Fin involutions

Some properties of involutions of Fin n.

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

def PhysLean.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 PhysLean.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 PhysLean.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 (Finset.filter (fun (i : Fin n) => ↑f i = i) Finset.univ).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 PhysLean.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 PhysLean.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 PhysLean.Fin.involutionAddEquiv_cast' {m : ℕ} {f1 f2 : { f : Fin m → Fin m // Function.Involutive f }} {N : ℕ} (hf : f1 = f2) (n : Option (Fin N)) (hn1 : N = (Finset.filter (fun (i : Fin m) => ↑f1 i = i) Finset.univ).card) (hn2 : N = (Finset.filter (fun (i : Fin m) => ↑f2 i = i) Finset.univ).card) : HEq ((involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn1)) n)) ((involutionAddEquiv f2).symm (Option.map (⇑(finCongr hn2)) n))

theorem PhysLean.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

theorem PhysLean.Fin.involutionAddEquiv_isSome_image_zero {n : ℕ} {f : { f : Fin n.succ → Fin n.succ // Function.Involutive f }} : ((involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd).isSome = true → ¬↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩

Equivalences of involutions with no fixed points.

The main aim of these equivalences is to define involutionNoFixedZeroEquivProd.

def PhysLean.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 PhysLean.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 PhysLean.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

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

def PhysLean.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

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

def PhysLean.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 PhysLean.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 PhysLean.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

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

def PhysLean.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

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

def PhysLean.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 PhysLean.Fin.instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean {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

• PhysLean.Fin.instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean = Subtype.fintype fun (x : Fin n → Fin n) => Function.Involutive x ∧ ∀ (i : Fin n), x i ≠ i

theorem PhysLean.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 PhysLean.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 PhysLean.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 PhysLean.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 PhysLean.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