Fin involutions

Some properties of involutions of Fin n.

These involutions are used in e.g. proving results about Wick contractions.

def Physlib.Fin.involutionCons (n : ℕ) : { f : Fin n.succ → Fin n.succ // Function.Involutive f } ≃ (f : { f : Fin n → Fin n // Function.Involutive f }) × { i : Option (Fin n) // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }

There is an equivalence between involutions of Fin n.succ and involutions of Fin n and an optional valid choice of an element in Fin n (which is where 0 in Fin n.succ will be sent).

Equations

• One or more equations did not get rendered due to their size.

theorem Physlib.Fin.involutionCons_ext {n : ℕ} {f1 f2 : (f : { f : Fin n → Fin n // Function.Involutive f }) × { i : Option (Fin n) // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }} (h1 : f1.fst = f2.fst) (h2 : f1.snd = (Equiv.subtypeEquivRight ⋯) f2.snd) : f1 = f2

def Physlib.Fin.involutionAddEquiv {n : ℕ} (f : { f : Fin n → Fin n // Function.Involutive f }) : { i : Option (Fin n) // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i : Fin n | ↑f i = i}.card)

Given an involution of Fin n, the optional choice of an element in Fin n which maps to itself is equivalent to the optional choice of an element in Fin (Finset.univ.filter fun i => f.1 i = i).card.

Equations

• One or more equations did not get rendered due to their size.

theorem Physlib.Fin.involutionAddEquiv_none_image_zero {n : ℕ} {f : { f : Fin n.succ → Fin n.succ // Function.Involutive f }} : (involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none → ↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩

theorem Physlib.Fin.involutionAddEquiv_cast {n : ℕ} {f1 f2 : { f : Fin n → Fin n // Function.Involutive f }} (hf : f1 = f2) : involutionAddEquiv f1 = (Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f2).trans (finCongr ⋯).optionCongr)

theorem Physlib.Fin.involutionAddEquiv_cast' {m : ℕ} {f1 f2 : { f : Fin m → Fin m // Function.Involutive f }} {N : ℕ} (hf : f1 = f2) (n : Option (Fin N)) (hn1 : N = {i : Fin m | ↑f1 i = i}.card) (hn2 : N = {i : Fin m | ↑f2 i = i}.card) : (involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn1)) n) ≍ (involutionAddEquiv f2).symm (Option.map (⇑(finCongr hn2)) n)

theorem Physlib.Fin.involutionAddEquiv_none_succ {n : ℕ} {f : { f : Fin n.succ → Fin n.succ // Function.Involutive f }} (h : (involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none) (x : Fin n) : ↑f x.succ = x.succ ↔ ↑((involutionCons n) f).fst x = x

Equivalences of involutions with no fixed points.

The main aim of these equivalences is to define involutionNoFixedZeroEquivProd.

def Physlib.Fin.involutionNoFixedEquivSum {n : ℕ} : { f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ ∀ (i : Fin n.succ), f i ≠ i } ≃ (k : Fin n) × { f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }

Fixed point free involutions of Fin n.succ can be separated based on where they sent 0.

Equations

• One or more equations did not get rendered due to their size.

def Physlib.Fin.involutionNoFixedZeroSetEquivEquiv {n : ℕ} (k : Fin n) (e : Fin n.succ ≃ Fin n.succ) : { f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ } ≃ { f : Fin n.succ → Fin n.succ // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }

The condition on fixed point free involutions of Fin n.succ for a fixed value of f 0, can be modified by conjugation with an equivalence.

Equations

• One or more equations did not get rendered due to their size.

def Physlib.Fin.involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin n) (e : Fin n.succ ≃ Fin n.succ) : { f : Fin n.succ → Fin n.succ // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ } ≃ { f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }

The condition on fixed point free involutions of Fin n.succ for a fixed value of f 0 given an equivalence e, can be modified so that only the condition on f 0 is up-to the equivalence e.

Equations

• Physlib.Fin.involutionNoFixedZeroSetEquivSetEquiv k e = Equiv.subtypeEquivRight ⋯

def Physlib.Fin.involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin n) (e : Fin n.succ ≃ Fin n.succ) : { f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ } ≃ { f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f (e 0) = e k.succ }

Fixed point free involutions of Fin n.succ fixing (e.symm ∘ f ∘ e) = k.succ for a given e are equivalent to fixing f (e 0) = e k.succ.

Equations

• Physlib.Fin.involutionNoFixedZeroSetEquivEquiv' k e = Equiv.subtypeEquivRight ⋯

def Physlib.Fin.involutionNoFixedZeroSetEquivSetOne {n : ℕ} (k : Fin n.succ) : { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = k.succ } ≃ { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }

Fixed point involutions of Fin n.succ.succ with f 0 = k.succ are equivalent to fixed point involutions with f 0 = 1.

Equations

• One or more equations did not get rendered due to their size.

def Physlib.Fin.involutionNoFixedSetOne {n : ℕ} : { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 } ≃ { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

Fixed point involutions of Fin n.succ.succ fixing f 0 = 1 are equivalent to fixed point involutions of Fin n.

Equations

• One or more equations did not get rendered due to their size.

def Physlib.Fin.involutionNoFixedZeroSetEquiv {n : ℕ} (k : Fin n.succ) : { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = k.succ } ≃ { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

Fixed point involutions of Fin n.succ.succ for fixed f 0 = k.succ are equivalent to fixed point involutions of Fin n.

Equations

• Physlib.Fin.involutionNoFixedZeroSetEquiv k = (Physlib.Fin.involutionNoFixedZeroSetEquivSetOne k).trans Physlib.Fin.involutionNoFixedSetOne

def Physlib.Fin.involutionNoFixedEquivSumSame {n : ℕ} : { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ ∀ (i : Fin n.succ.succ), f i ≠ i } ≃ (_ : Fin n.succ) × { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

The type of fixed point free involutions of Fin n.succ.succ is equivalent to the sum of Fin n.succ copies of fixed point involutions of Fin n.

Equations

• Physlib.Fin.involutionNoFixedEquivSumSame = Physlib.Fin.involutionNoFixedEquivSum.trans (Equiv.sigmaCongrRight Physlib.Fin.involutionNoFixedZeroSetEquiv)

def Physlib.Fin.involutionNoFixedZeroEquivProd {n : ℕ} : { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ ∀ (i : Fin n.succ.succ), f i ≠ i } ≃ Fin n.succ × { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

Ever fixed-point free involutions of Fin n.succ.succ can be decomposed into a element of Fin n.succ (where 0 is sent) and a fixed-point free involution of Fin n.

Equations

• One or more equations did not get rendered due to their size.

Cardinality

instance Physlib.Fin.instFintypeSubtypeForallFinAndInvolutiveForallNe_physlib {n : ℕ} : Fintype { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

The type of fixed-point free involutions of Fin n is finite.

Equations

• Physlib.Fin.instFintypeSubtypeForallFinAndInvolutiveForallNe_physlib = Subtype.fintype fun (f : Fin n → Fin n) => Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i

theorem Physlib.Fin.involutionNoFixed_card_succ {n : ℕ} : Fintype.card { f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ ∀ (i : Fin n.succ.succ), f i ≠ i } = n.succ * Fintype.card { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

theorem Physlib.Fin.involutionNoFixed_card_mul_two (n : ℕ) : Fintype.card { f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ ∀ (i : Fin (2 * n)), f i ≠ i } = (2 * n - 1).doubleFactorial

theorem Physlib.Fin.involutionNoFixed_card_mul_two_plus_one (n : ℕ) : Fintype.card { f : Fin (2 * n + 1) → Fin (2 * n + 1) // Function.Involutive f ∧ ∀ (i : Fin (2 * n + 1)), f i ≠ i } = 0

theorem Physlib.Fin.involutionNoFixed_card_even (n : ℕ) (he : Even n) : Fintype.card { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1).doubleFactorial

theorem Physlib.Fin.involutionNoFixed_card_odd (n : ℕ) (ho : Odd n) : Fintype.card { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0