-- Exchanging two inputs of a permutation as a function graph (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Cardinal.PermutationExchange
import Permutations
import Set.Transposition

defgraph permutationExchange (I a b : Set) (p ∈ permutations(I)) : permutations(I) :=
  compose(p, transposition(I, a, b), I, I, I)
requires ha : a ∈ I
requires hb : b ∈ I
proof
  have permutation := permutations.mem_iff.forward at I, p with *
  have swap := transposition.bijective at I, a, b with *
  have composed := compose.bijective at p, transposition(I, a, b), I, I, I with *
  exact permutations.mem_iff.backward at I, compose(p, transposition(I, a, b), I, I, I) with composed

section Exchanges
variable (I a b : Set)
hypothesis ha : a ∈ I
hypothesis hb : b ∈ I

theorem permutationExchange.apply (p i : Set)
  requires permutation : p ∈ permutations(I)
  requires index : i ∈ I
  shows permutationExchange(I, a, b)(p)(i) = p(transposition(I, a, b)(i))
proof
  have bijective := permutations.mem_iff.forward with permutation
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have swap := transposition.function at I, a, b with *
  have graph := permutationExchange.value at I, a, b, p with *
  rw graph
  exact compose.apply with *

theorem permutationExchange.involution
  shows InvolutionOn(permutationExchange(I, a, b), permutations(I))
proof
  have function := permutationExchange.function at I, a, b with *
  have swap := transposition.function at I, a, b with *
  have inverse := transposition.involution at I, a, b with *
  unfold InvolutionOn
  refine ⟨function, ?_⟩
  intros p member
  have paired := FunctionBetween.apply_closed with function, member
  have doubled := FunctionBetween.apply_closed with function, paired
  have originalBijective := permutations.mem_iff.forward with member
  have doubleBijective := permutations.mem_iff.forward with doubled
  have originalInjective := Bijective.injective with originalBijective
  have doubleInjective := Bijective.injective with doubleBijective
  have originalFunction := Injective.function with originalInjective
  have doubleFunction := Injective.function with doubleInjective
  apply FunctionBetween.ext with doubleFunction, originalFunction
  intros i index
  have image := FunctionBetween.apply_closed with swap, index
  have outer := permutationExchange.apply at I, a, b, permutationExchange(I, a, b)(p), i with *
  have inner := permutationExchange.apply at I, a, b, p, transposition(I, a, b)(i) with *
  have restored := InvolutionOn.apply with inverse, index
  cc

theorem permutationExchange.free (p : Set)
  requires distinct : a ≠ b
  requires permutation : p ∈ permutations(I)
  shows permutationExchange(I, a, b)(p) ≠ p
proof
  intro same
  have bijective := permutations.mem_iff.forward with permutation
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have atFirst := permutationExchange.apply at I, a, b, p, a with *
  have swapped := transposition.first at I, a, b with *
  have equal : p(a) = p(b) by cc
  have value := FunctionBetween.apply_closed at p, I, I, b with *
  have edgeA := FunctionBetween.relates_apply at p, I, I, a with *
  have edgeB := FunctionBetween.relates_apply at p, I, I, b with *
  rw equal at edgeA
  have impossible := Injective.cancel at p, I, I, a, b, p(b) with *
  exact distinct with impossible

theorem permutationExchange.symmetric (p : Set)
  requires permutation : p ∈ permutations(I)
  shows permutationExchange(I, a, b)(p) = permutationExchange(I, b, a)(p)
proof
  simp [permutationExchange.value, transposition.symmetric]

end Exchanges
theorem permutationExchange.conjugate (I a b c p : Set)
  requires ha : a ∈ I
  requires hb : b ∈ I
  requires hc : c ∈ I
  requires ab : a ≠ b
  requires ac : a ≠ c
  requires bc : b ≠ c
  requires permutation : p ∈ permutations(I)
  shows permutationExchange(I, b, c)(permutationExchange(I, a, b)(permutationExchange(I, b, c)(p))) = permutationExchange(I, a, c)(p)
proof
  have fBC := permutationExchange.function at I, b, c with *
  have fAB := permutationExchange.function at I, a, b with *
  have fAC := permutationExchange.function at I, a, c with *
  have p1 := FunctionBetween.apply_closed with fBC, permutation
  have p2 := FunctionBetween.apply_closed with fAB, p1
  have p3 := FunctionBetween.apply_closed with fBC, p2
  have direct := FunctionBetween.apply_closed with fAC, permutation
  have b3 := permutations.mem_iff.forward with p3
  have bd := permutations.mem_iff.forward with direct
  have i3 := Bijective.injective with b3
  have id := Bijective.injective with bd
  have fn3 := Injective.function with i3
  have fnd := Injective.function with id
  have swapBC := transposition.function at I, b, c with *
  have swapAB := transposition.function at I, a, b with *
  apply FunctionBetween.ext with fn3, fnd
  intros i hi
  have jIn := FunctionBetween.apply_closed with swapBC, hi
  have kIn := FunctionBetween.apply_closed with swapAB, jIn
  have first := permutationExchange.apply at I, b, c, permutationExchange(I, a, b)(permutationExchange(I, b, c)(p)), i with *
  have second := permutationExchange.apply at I, a, b, permutationExchange(I, b, c)(p), transposition(I, b, c)(i) with *
  have third := permutationExchange.apply at I, b, c, p, transposition(I, a, b)(transposition(I, b, c)(i)) with *
  have directValue := permutationExchange.apply at I, a, c, p, i with *
  have conjugate := transposition.conjugate at I, a, b, c, i with *
  cc