Grace/Cumulus/Algebra/Ring/PermutationSignCompose.g17

Open in Workbench Download source

Imports

PermutationSign · DeterminantIdentity · Combinatorics.Permutations

Declarations

Source

1-- The sign of a composite permutation is the product of the signs: a2-- permutation with no inversions is the identity, an inversion yields an3-- adjacent descent, exchanging at a descent removes exactly one inversion,4-- and induction on the number of inversions does the rest5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.PermutationSignCompose11import PermutationSign12import DeterminantIdentity13import Combinatorics.Permutations1415-- The points a function moves.16def movedPoints (n q : Set) : Set := { i ∈ n | q(i) ≠ i }1718-- A least moved point i is sent upward, and the point sent onto i lies19-- beyond i: together they form an inversion.20theorem permutations.least_moved (n : Nat) (q i : Set)21  requires permutation : q ∈ permutations(n)22  requires iIn : i ∈ n23  requires moved : q(i) ≠ i24  requires least : ∀ j ∈ n, j < i → q(j) = j25  shows Nonempty(inversions(n, q))26proof27  have positions := natural.member at n28  have iNat := positions with i, iIn29  have vIn := permutations.apply_closed with permutation, iIn30  have vNat := positions with q(i), vIn31  have order := Less.trichotomy at q(i), i with vNat, iNat32  rcases order with below | rest33  . have fixedV := least with q(i), vIn, below34    have cancel := permutations.apply_cancel at n, q, q(i), i35      with permutation, vIn, iIn, fixedV36    exfalso37    exact moved with cancel38  . rcases rest with same | above39    . exfalso40      exact moved with same41    . obtain ⟨j, jIn, hit⟩ := permutations.apply_surjective at n, q, i42        with permutation, iIn43      have jNat := positions with j, jIn44      have orderJ := Less.trichotomy at j, i with jNat, iNat45      rcases orderJ with jBelow | restJ46      . have fixedJ := least with j, jIn, jBelow47        rw fixedJ at hit48        rw hit at jBelow49        have irreflexive := Less.irreflexive at i50        exfalso51        exact irreflexive with jBelow52      . rcases restJ with jSame | jAbove53        . rw jSame at hit54          exfalso55          exact moved with hit56        . have ruleIJ := membership.of_Less at i, j with iNat, jNat57          have iInJ := ruleIJ with jAbove58          have ruleIV := membership.of_Less at i, q(i) with iNat, vNat59          have iInV := ruleIV with above60          have reversed : q(j) ∈ q(i)61            rw hit62            exact iInV63          have pair := inversions.pair.backward at n, q, i, j64            with ⟨iIn, jIn, iInJ, reversed⟩65          witness (i, j)66          exact pair6768-- A permutation with no inversions is the identity.69theorem permutations.identity_of_no_inversions (n : Nat) (q : Set)70  requires permutation : q ∈ permutations(n)71  requires empty : inversions(n, q) = ∅72  shows q = identity(n)73proof74  have function := permutations.function with permutation75  have idFunction := identity.function at n76  have positions := natural.member at n77  have naturals : movedPoints(n, q) ⊆ ℕ78    intros i hi79    have parts := movedPoints.membership.forward with hi80    have iNat := positions with i, parts.left81    exact nat.omega.forward with iNat82  have noMoved : ¬Nonempty(movedPoints(n, q))83    intro inhabited84    have member := leastNatural.member at movedPoints(n, q) with inhabited, naturals85    obtain ⟨iIn, moved⟩ := movedPoints.membership.forward with member86    have least : ∀ j ∈ n, j < leastNatural(movedPoints(n, q)) → q(j) = j87      intros j jIn below88      have jNat := positions with j, jIn89      by_contra90      have jMoved : j ∈ movedPoints(n, q) :=91        movedPoints.membership.backward with ⟨jIn, this⟩92      have bound := leastNatural.least at movedPoints(n, q), j93        with inhabited, naturals, jMoved94      have separation := Less.iff_not_LessEqual at j, leastNatural(movedPoints(n, q))95      have notBound := separation.forward with below96      exact notBound with bound97    have inversionsInhabited := permutations.least_moved at n, q,98      leastNatural(movedPoints(n, q)) with permutation, iIn, moved, least99    rw empty at inversionsInhabited100    obtain ⟨x, hx⟩ := inversionsInhabited101    exact set.empty with hx102  have same : ∀ x ∈ n, q(x) = identity(n)(x)103    intros x hx104    have idValue := identity.apply at x, n with hx105    rw idValue106    by_contra107    have xMoved : x ∈ movedPoints(n, q) :=108      movedPoints.membership.backward with ⟨hx, this⟩109    exact noMoved with ⟨x, xMoved⟩110  exact FunctionBetween.ext with function, idFunction, same111112-- Between the ends of an inversion lies an adjacent descent.113theorem inversions.descent_within (n : Nat) (q : Set) (d : Nat)114  requires permutation : q ∈ permutations(n)115  shows ∀ i, Nat(i) → ∀ j, Nat(j) → i ∈ n → j ∈ n → j = i + 1 + d →116    q(j) ∈ q(i) → ∃ a, Nat(a) ∧ a ∈ n ∧ succ(a) ∈ n ∧ q(succ(a)) ∈ q(a)117proof118  induction d119  | zero =>120    intros i iNat j jNat iIn jIn gap reversed121    have plusOne : i + 1 = succ(i) := add.right_one at i122    have jSucc : j = succ(i)123      rw [← plusOne, gap]124      arith125    rw jSucc at jIn126    rw jSucc at reversed127    refine ⟨i, iNat, iIn, jIn, reversed⟩128  | succ(k) using ih =>129    intros i iNat j jNat iIn jIn gap reversed130    have positions := natural.member at n131    have mNat : Nat(succ(i)) by typecheck132    have plusOne : i + 1 = succ(i) := add.right_one at i133    have plusOneK : k + 1 = succ(k) := add.right_one at k134    have shifted : j = succ(i) + 1 + k135      rw ← plusOneK at gap136      rw [← plusOne, gap]137      ring138    have mBelowJ : succ(i) < j139      rw shifted140      arith141    have ruleJN := Less.of_membership at j, n142    have jBelowN := ruleJN with jIn143    have mBelowN := Less.transitive at succ(i), j, n with mBelowJ, jBelowN144    have ruleMN := membership.of_Less at succ(i), n with mNat, assumption145    have mIn := ruleMN with mBelowN146    have qmIn := permutations.apply_closed with permutation, mIn147    have qiIn := permutations.apply_closed with permutation, iIn148    have qjIn := permutations.apply_closed with permutation, jIn149    have qmNat := positions with q(succ(i)), qmIn150    have qiNat := positions with q(i), qiIn151    have qjNat := positions with q(j), qjIn152    have order := Less.trichotomy at q(succ(i)), q(i) with qmNat, qiNat153    rcases order with descent | rest154    . have rule := membership.of_Less at q(succ(i)), q(i) with qmNat, qiNat155      have mem := rule with descent156      refine ⟨i, iNat, iIn, mIn, mem⟩157    . rcases rest with same | ascent158      . have cancel := permutations.apply_cancel at n, q, succ(i), i159          with permutation, mIn, iIn, same160        rw ← plusOne at cancel161        exfalso162        arith163      . have ruleJI := Less.of_membership at q(j), q(i)164        have below := ruleJI with reversed165        have chain := Less.transitive at q(j), q(i), q(succ(i)) with below, ascent166        have ruleJM := membership.of_Less at q(j), q(succ(i)) with qjNat, qmNat167        have mem := ruleJM with chain168        exact ih with succ(i), mNat, j, jNat, mIn, jIn, shifted, mem169170-- A permutation with an inversion has an adjacent descent.171theorem inversions.adjacent_descent (n : Nat) (q : Set)172  requires permutation : q ∈ permutations(n)173  requires inhabited : Nonempty(inversions(n, q))174  shows ∃ a, Nat(a) ∧ a ∈ n ∧ succ(a) ∈ n ∧ q(succ(a)) ∈ q(a)175proof176  obtain ⟨pair, member⟩ := inhabited177  obtain ⟨bound, i, iIn, j, jIn, shape, ordered, reversed⟩ :=178    inversions.membership.forward with member179  have positions := natural.member at n180  have iNat := positions with i, iIn181  have jNat := positions with j, jIn182  have rule := Less.of_membership at i, j183  have below := rule with ordered184  have gapRule := Less.gap at i, j185  have atLeast := gapRule.forward with below186  obtain ⟨d, dNat, gap⟩ := LessEqual.exists_add at i + 1, j with atLeast187  exact inversions.descent_within at n, q, d188    with permutation, i, iNat, j, jNat, iIn, jIn, gap, reversed189190-- Exchanging at an adjacent descent removes exactly one inversion.191theorem inversions.descent_count (n a : Nat) (q : Set)192  requires ha : a ∈ n193  requires hb : succ(a) ∈ n194  requires permutation : q ∈ permutations(n)195  requires descent : (a, succ(a)) ∈ inversions(n, q)196  shows cardinality(inversions(n, q)) =197    succ(cardinality(inversions(n, permutationExchange(n, a, succ(a))(q))))198proof199  have finite := inversions.finite at n, q with (Finite.natural at n)200  have remove := cardinality.remove at inversions(n, q), (a, succ(a)) with finite, descent201  have off := inversions.adjacent_count_off_pair at n, a, q with ha, hb, permutation202  have self := bootstrap.succ.self at a203  have rule := Less.of_membership at a, succ(a)204  have ordered := rule with self205  have distinguished := inversions.exchange_distinguished at n, a, succ(a), q206    with ha, hb, ordered, permutation207  have absent : ¬((a, succ(a)) ∈ inversions(n, permutationExchange(n, a, succ(a))(q)))208    intro present209    have contradiction := distinguished.forward with present210    exact contradiction with descent211  have disjoint : inversions(n, permutationExchange(n, a, succ(a))(q)) ∩ {(a, succ(a))} = ∅212    ext x213    constructor214    . intro hx215      have parts := intersection.membership.forward with hx216      have equal := singleton.membership.forward with parts.right217      rw equal at parts218      exfalso219      exact absent with parts.left220    . intro hx221      exfalso222      exact set.empty with hx223  have same := difference.eq_self_iff_disjoint at224    inversions(n, permutationExchange(n, a, succ(a))(q)), {(a, succ(a))}225  have unchanged := same.backward with disjoint226  rw [remove, off, unchanged]227  rfl228229-- The sign of a composite, by induction on the number of inversions of230-- the right factor.231theorem permutationSign.compose_induction (A add zero neg mul one : Set) (n k : Nat)232  requires ring : IsCommRing(A, add, zero, neg, mul, one)233  shows ∀ q ∈ permutations(n), cardinality(inversions(n, q)) = k →234    ∀ p ∈ permutations(n),235      permutationSign(n, A, add, zero, neg, mul, one, compose(p, q, n, n, n)) =236        call2(mul, permutationSign(n, A, add, zero, neg, mul, one, p),237          permutationSign(n, A, add, zero, neg, mul, one, q))238proof239  induction k240  | zero =>241    intros q hq count p hp242    have finiteN := Finite.natural at n243    have finite := inversions.finite at n, q with finiteN244    have criterion := cardinality.eq_zero_iff at inversions(n, q) with finite245    have empty := criterion.forward with count246    have isIdentity := permutations.identity_of_no_inversions at n, q with hq, empty247    have composed := permutations.compose_identity_right at n, p with hp248    have signOne := permutationSign.identity at A, add, zero, neg, mul, one, n with ring249    have signP := permutationSign.closed at A, add, zero, neg, mul, one, n, p250      with ring, finiteN251    have ordinary := IsCommRing.ring with ring252    have multiplicative := IsRing.multiplicative with ordinary253    have unit := IsMonoid.right_identity at A, mul, one,254      permutationSign(n, A, add, zero, neg, mul, one, p) with multiplicative, signP255    rw [isIdentity, composed, signOne, unit]256    rfl257  | succ(m) using ih =>258    intros q hq count p hp259    have finiteN := Finite.natural at n260    have finite := inversions.finite at n, q with finiteN261    have inhabited : Nonempty(inversions(n, q))262      have criterion := Nonempty.iff_ne_empty at inversions(n, q)263      apply criterion.backward264      intro empty265      have zeroCount := cardinality.eq_zero_iff at inversions(n, q) with finite266      have isZero := zeroCount.backward with empty267      rw isZero at count268      arith269    obtain ⟨a, aNat, ha, hb, descentValue⟩ :=270      inversions.adjacent_descent at n, q with hq, inhabited271    have self := bootstrap.succ.self at a272    have descent := inversions.pair.backward at n, q, a, succ(a)273      with ⟨ha, hb, self, descentValue⟩274    have exchangeFunction := permutationExchange.function at n, a, succ(a) with ha, hb275    have hqExchanged := FunctionBetween.apply_closed with exchangeFunction, hq276    have countRule := inversions.descent_count at n, a, q with ha, hb, hq, descent277    rw countRule at count278    have countExchanged := Naturals.injective.succ with count279    have composedIn := permutations.compose at n, permutationExchange(n, a, succ(a))(q), p280      with hqExchanged, hp281    have inner := ih with permutationExchange(n, a, succ(a))(q), hqExchanged, countExchanged, p, hp282    have involution := permutationExchange.involution at n, a, succ(a) with ha, hb283    have restore := involution.right with q, hq284    have value := permutationExchange.value at n, a, succ(a),285      permutationExchange(n, a, succ(a))(q) with ha, hb, hqExchanged286    have associative := permutations.compose_associative at n, transposition(n, a, succ(a)),287      permutationExchange(n, a, succ(a))(q), p288    have composedValue := permutationExchange.value at n, a, succ(a),289      compose(p, permutationExchange(n, a, succ(a))(q), n, n, n) with ha, hb, composedIn290    have distinct : a ≠ succ(a)291      intro equal292      have plusOne : a + 1 = succ(a) := add.right_one at a293      rw ← plusOne at equal294      arith295    have signExchange := permutationSign.exchange at A, add, zero, neg, mul, one, n, a, succ(a),296      compose(p, permutationExchange(n, a, succ(a))(q), n, n, n)297      with ring, ha, hb, distinct, composedIn298    have signQ := permutationSign.exchange at A, add, zero, neg, mul, one, n, a, succ(a),299      permutationExchange(n, a, succ(a))(q) with ring, ha, hb, distinct, hqExchanged300    have signP := permutationSign.closed at A, add, zero, neg, mul, one, n, p301      with ring, finiteN302    have signExchanged := permutationSign.closed at A, add, zero, neg, mul, one, n,303      permutationExchange(n, a, succ(a))(q) with ring, finiteN304    have ordinary := IsCommRing.ring with ring305    have negClosed := IsRing.neg_closed at A, add, zero, neg, mul, one,306      permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(q))307      with ordinary, signExchanged308    have commutative := IsCommRing.commutative with ring309    unfold Commutative at commutative310    have swapNeg := commutative with311      permutationSign(n, A, add, zero, neg, mul, one, p), signP,312      neg(permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(q))),313      negClosed314    have swap := commutative with315      permutationSign(n, A, add, zero, neg, mul, one, p), signP,316      permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(q)),317      signExchanged318    have negLeft := IsRing.neg_mul at A, add, zero, neg, mul, one,319      permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(q)),320      permutationSign(n, A, add, zero, neg, mul, one, p) with ordinary, signExchanged, signP321    have negation : call2(mul, permutationSign(n, A, add, zero, neg, mul, one, p),322        neg(permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(q)))) =323        neg(call2(mul, permutationSign(n, A, add, zero, neg, mul, one, p),324          permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(q))))325      rw [swapNeg, negLeft, swap]326      rfl327    rw restore at signQ328    rw restore at value329    rw [signQ, negation, ← inner, ← signExchange, composedValue, ← associative, ← value]330    rfl331332-- The sign of a composite permutation is the product of the signs.333theorem permutationSign.compose (A add zero neg mul one : Set) (n : Nat) (p q : Set)334  requires ring : IsCommRing(A, add, zero, neg, mul, one)335  requires hp : p ∈ permutations(n)336  requires hq : q ∈ permutations(n)337  shows permutationSign(n, A, add, zero, neg, mul, one, compose(p, q, n, n, n)) =338    call2(mul, permutationSign(n, A, add, zero, neg, mul, one, p),339      permutationSign(n, A, add, zero, neg, mul, one, q))340proof341  have finite := inversions.finite at n, q with (Finite.natural at n)342  have countNat := cardinality.nat at inversions(n, q) with finite343  have rule := permutationSign.compose_induction at A, add, zero, neg, mul, one, n,344    cardinality(inversions(n, q)) with ring345  have same : cardinality(inversions(n, q)) = cardinality(inversions(n, q)) by rfl346  exact rule with q, hq, same, p, hp347