Grace/Cumulus/Cardinal/PermutationExchange.g17

Open in Workbench Download source

Imports

Permutations · Set.Transposition

Declarations

Source

1-- Exchanging two inputs of a permutation as a function graph (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.PermutationExchange8import Permutations9import Set.Transposition1011defgraph permutationExchange (I a b : Set) (p ∈ permutations(I)) : permutations(I) :=12  compose(p, transposition(I, a, b), I, I, I)13requires ha : a ∈ I14requires hb : b ∈ I15proof16  have permutation := permutations.mem_iff.forward at I, p with *17  have swap := transposition.bijective at I, a, b with *18  have composed := compose.bijective at p, transposition(I, a, b), I, I, I with *19  exact permutations.mem_iff.backward at I, compose(p, transposition(I, a, b), I, I, I) with composed2021section Exchanges22variable (I a b : Set)23hypothesis ha : a ∈ I24hypothesis hb : b ∈ I2526theorem permutationExchange.apply (p i : Set)27  requires permutation : p ∈ permutations(I)28  requires index : i ∈ I29  shows permutationExchange(I, a, b)(p)(i) = p(transposition(I, a, b)(i))30proof31  have bijective := permutations.mem_iff.forward with permutation32  have injective := Bijective.injective with bijective33  have function := Injective.function with injective34  have swap := transposition.function at I, a, b with *35  have graph := permutationExchange.value at I, a, b, p with *36  rw graph37  exact compose.apply with *3839theorem permutationExchange.involution40  shows InvolutionOn(permutationExchange(I, a, b), permutations(I))41proof42  have function := permutationExchange.function at I, a, b with *43  have swap := transposition.function at I, a, b with *44  have inverse := transposition.involution at I, a, b with *45  unfold InvolutionOn46  refine ⟨function, ?_⟩47  intros p member48  have paired := FunctionBetween.apply_closed with function, member49  have doubled := FunctionBetween.apply_closed with function, paired50  have originalBijective := permutations.mem_iff.forward with member51  have doubleBijective := permutations.mem_iff.forward with doubled52  have originalInjective := Bijective.injective with originalBijective53  have doubleInjective := Bijective.injective with doubleBijective54  have originalFunction := Injective.function with originalInjective55  have doubleFunction := Injective.function with doubleInjective56  apply FunctionBetween.ext with doubleFunction, originalFunction57  intros i index58  have image := FunctionBetween.apply_closed with swap, index59  have outer := permutationExchange.apply at I, a, b, permutationExchange(I, a, b)(p), i with *60  have inner := permutationExchange.apply at I, a, b, p, transposition(I, a, b)(i) with *61  have restored := InvolutionOn.apply with inverse, index62  cc6364theorem permutationExchange.free (p : Set)65  requires distinct : a ≠ b66  requires permutation : p ∈ permutations(I)67  shows permutationExchange(I, a, b)(p) ≠ p68proof69  intro same70  have bijective := permutations.mem_iff.forward with permutation71  have injective := Bijective.injective with bijective72  have function := Injective.function with injective73  have atFirst := permutationExchange.apply at I, a, b, p, a with *74  have swapped := transposition.first at I, a, b with *75  have equal : p(a) = p(b) by cc76  have value := FunctionBetween.apply_closed at p, I, I, b with *77  have edgeA := FunctionBetween.relates_apply at p, I, I, a with *78  have edgeB := FunctionBetween.relates_apply at p, I, I, b with *79  rw equal at edgeA80  have impossible := Injective.cancel at p, I, I, a, b, p(b) with *81  exact distinct with impossible8283theorem permutationExchange.symmetric (p : Set)84  requires permutation : p ∈ permutations(I)85  shows permutationExchange(I, a, b)(p) = permutationExchange(I, b, a)(p)86proof87  simp [permutationExchange.value, transposition.symmetric]8889end Exchanges90theorem permutationExchange.conjugate (I a b c p : Set)91  requires ha : a ∈ I92  requires hb : b ∈ I93  requires hc : c ∈ I94  requires ab : a ≠ b95  requires ac : a ≠ c96  requires bc : b ≠ c97  requires permutation : p ∈ permutations(I)98  shows permutationExchange(I, b, c)(permutationExchange(I, a, b)(permutationExchange(I, b, c)(p))) = permutationExchange(I, a, c)(p)99proof100  have fBC := permutationExchange.function at I, b, c with *101  have fAB := permutationExchange.function at I, a, b with *102  have fAC := permutationExchange.function at I, a, c with *103  have p1 := FunctionBetween.apply_closed with fBC, permutation104  have p2 := FunctionBetween.apply_closed with fAB, p1105  have p3 := FunctionBetween.apply_closed with fBC, p2106  have direct := FunctionBetween.apply_closed with fAC, permutation107  have b3 := permutations.mem_iff.forward with p3108  have bd := permutations.mem_iff.forward with direct109  have i3 := Bijective.injective with b3110  have id := Bijective.injective with bd111  have fn3 := Injective.function with i3112  have fnd := Injective.function with id113  have swapBC := transposition.function at I, b, c with *114  have swapAB := transposition.function at I, a, b with *115  apply FunctionBetween.ext with fn3, fnd116  intros i hi117  have jIn := FunctionBetween.apply_closed with swapBC, hi118  have kIn := FunctionBetween.apply_closed with swapAB, jIn119  have first := permutationExchange.apply at I, b, c, permutationExchange(I, a, b)(permutationExchange(I, b, c)(p)), i with *120  have second := permutationExchange.apply at I, a, b, permutationExchange(I, b, c)(p), transposition(I, b, c)(i) with *121  have third := permutationExchange.apply at I, b, c, p, transposition(I, a, b)(transposition(I, b, c)(i)) with *122  have directValue := permutationExchange.apply at I, a, c, p, i with *123  have conjugate := transposition.conjugate at I, a, b, c, i with *124  cc125