Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Mathlib.Data.Finset.Sort public import Mathlib.Data.Fintype.Pi public import Mathlib.Data.Fintype.Prod public import Mathlib.Data.Nat.Factorial.DoubleFactorial

Fin involutions

Some properties of involutions of Fin n.

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

@[expose] public section

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).

n:f✝:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f:Fin n Fin nhf:Function.Involutive ff0:Option (Fin n)hf0: (h : f0.isSome = true), f, hf (f0.get h) = f0.get hi:Fin nhs:f0.isSome = truehx:¬(f0.get hs).succ = 0f0.get = i (h : f0.isSome = true), f0.get h = i All goals completed! 🐙 n:f✝:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f:Fin n Fin nhf:Function.Involutive ff0:Option (Fin n)hf0: (h : f0.isSome = true), f, hf (f0.get h) = f0.get hi:Fin nhs:¬f0.isSome = true(∃ (h : ¬(if h : f0.isSome = true then Fin.cons (f0.get ).succ (Function.update (Fin.succ f) (f0.get ) 0) else Fin.cons 0 (Fin.succ f)) 0 = 0), ((if h : f0.isSome = true then Fin.cons (f0.get ).succ (Function.update (Fin.succ f) (f0.get ) 0) else Fin.cons 0 (Fin.succ f)) 0).pred = i) f0 = some i n:f✝:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f:Fin n Fin nhf:Function.Involutive ff0:Option (Fin n)hf0: (h : f0.isSome = true), f, hf (f0.get h) = f0.get hi:Fin nhs:¬f0.isSome = true¬f0 = some i n:f✝:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f:Fin n Fin nhf:Function.Involutive ff0:Option (Fin n)hf0: (h : f0.isSome = true), f, hf (f0.get h) = f0.get hi:Fin nhs:f0 = none¬f0 = some i n:f✝:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f:Fin n Fin nhf:Function.Involutive fi:Fin nhf0: (h : none.isSome = true), f, hf (none.get h) = none.get h¬none = some i All goals completed! 🐙
n:f1:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f2:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }h1:f1.fst = f2.fst (x : Option (Fin n)), (∀ (h : x.isSome = true), f2.fst (x.get h) = x.get h) (h : x.isSome = true), f2.fst (x.get h) = x.get h; All goals completed! 🐙) f2.2) : f1 = f2 := n:f1:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }f2:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }h1:f1.fst = f2.fsth2:f1.snd = (Equiv.subtypeEquivRight ) f2.sndf1 = f2 n:f2:(f : { f // Function.Involutive f }) × { i // (h : i.isSome = true), f (i.get h) = i.get h }fst✝:{ f // Function.Involutive f }snd✝:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }h1:fst✝, snd✝.fst = f2.fsth2:fst✝, snd✝.snd = (Equiv.subtypeEquivRight ) f2.sndfst✝, snd✝ = f2 n:fst✝¹:{ f // Function.Involutive f }snd✝¹:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }fst✝:{ f // Function.Involutive f }snd✝:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }h1:fst✝¹, snd✝¹.fst = fst✝, snd✝.fsth2:fst✝¹, snd✝¹.snd = (Equiv.subtypeEquivRight ) fst✝, snd✝.sndfst✝¹, snd✝¹ = fst✝, snd✝ n:fst✝¹:{ f // Function.Involutive f }snd✝¹:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }fst✝:{ f // Function.Involutive f }snd✝:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }h1:fst✝¹ = fst✝h2:snd✝¹ = (Equiv.subtypeEquivRight ) snd✝fst✝¹, snd✝¹ = fst✝, snd✝ n:fst✝:{ f // Function.Involutive f }snd✝¹:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }snd✝:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }h2:snd✝¹ = (Equiv.subtypeEquivRight ) snd✝fst✝, snd✝¹ = fst✝, snd✝ n:fst:{ f // Function.Involutive f }snd:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }snd_1:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }h2:snd✝¹ = (Equiv.subtypeEquivRight ) snd✝fst✝, snd✝¹ = fst✝, snd✝ n:fst:{ f // Function.Involutive f }snd:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }snd_1:{ i // (h : i.isSome = true), fst✝ (i.get h) = i.get h }h2:snd✝¹ = (Equiv.subtypeEquivRight ) snd✝(Equiv.subtypeEquivRight ) snd_1 = snd_1 n:val:Fin n Fin nproperty:Function.Involutive valsnd:{ i // (h : i.isSome = true), val, property (i.get h) = i.get h }snd_1:{ i // (h : i.isSome = true), val, property (i.get h) = i.get h }h2:snd = (Equiv.subtypeEquivRight ) snd_1(Equiv.subtypeEquivRight ) snd_1 = snd_1 n:val:Fin n Fin nproperty:Function.Involutive valsnd_1:{ i // (h : i.isSome = true), val, property (i.get h) = i.get h }val_1:Option (Fin n)property_1: (h : val_1.isSome = true), val, property (val_1.get h) = val_1.get hh2:val_1, property_1 = (Equiv.subtypeEquivRight ) snd_1(Equiv.subtypeEquivRight ) snd_1 = snd_1 n:val:Fin n Fin nproperty:Function.Involutive valval_1:Option (Fin n)property_1: (h : val_1.isSome = true), val, property (val_1.get h) = val_1.get hval_2:Option (Fin n)property_2: (h : val_2.isSome = true), val, property (val_2.get h) = val_2.get hh2:val_1, property_1 = (Equiv.subtypeEquivRight ) val_2, property_2(Equiv.subtypeEquivRight ) val_2, property_2 = val_2, property_2 n:val:Fin n Fin nproperty:Function.Involutive valval_1:Option (Fin n)property_1: (h : val_1.isSome = true), val, property (val_1.get h) = val_1.get hval_2:Option (Fin n)property_2: (h : val_2.isSome = true), val, property (val_2.get h) = val_2.get hh2:val_1, property_1 = (Equiv.subtypeEquivRight ) val_2, property_2(Equiv.subtypeEquivRight ) val_2, property_2 = val_2, property_2 All goals completed! 🐙

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.

n:f:{ f // Function.Involutive f }e1:{ i // (h : i.isSome = true), f (i.get h) = i.get h } Option { i // f i = i } := { toFun := fun i => match i with | some i, h => some i, | none, h => none, invFun := fun i => match i with | some i, h => some i, | none => none, , left_inv := , right_inv := }s:Finset (Fin n) := {i | f i = i}e2':{ i // f i = i } s := Equiv.subtypeEquivProp e2:s Fin s.card := (s.orderIsoOfFin ).symm.toEquiv{ i // (h : i.isSome = true), f (i.get h) = i.get h } Option (Fin {i | f i = i}.card) All goals completed! 🐙
lemma involutionAddEquiv_none_image_zero {n : } : {f : {f : Fin n.succ Fin n.succ // Function.Involutive f}} involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none f.1 0, Nat.zero_lt_succ n = 0, Nat.zero_lt_succ n := n: {f : { f // Function.Involutive f }}, (involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none f 0, = 0, n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonef 0, = 0, n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonehf0:¬f 0, = 0, False n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonehf0:¬f 0 = 0False n:f:{ f // Function.Involutive f }hf0:¬f 0 = 0h:({ toFun := fun i => match i with | some i, h => some i, | none, h => none, invFun := fun i => match i with | some i, h => some i, | none => none, , left_inv := , right_inv := }.trans ((Equiv.subtypeEquivProp ).trans ({i | (if h : f i.succ = 0 then i else (f i.succ).pred h) = i}.orderIsoOfFin ).symm.toEquiv).optionCongr) some ((f 0).pred hf0), = noneFalse All goals completed! 🐙n:f1:{ f // Function.Involutive f }involutionAddEquiv f1 = (Equiv.subtypeEquivRight ).trans ((involutionAddEquiv f1).trans (Equiv.refl (Option (Fin {i | f1 i = i}.card)))) All goals completed! 🐙lemma 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 => f1.1 i = i) Finset.univ).card) (hn2 : N = (Finset.filter (fun i => f2.1 i = i) Finset.univ).card) : HEq ((involutionAddEquiv f1).symm (Option.map (finCongr hn1) n)) ((involutionAddEquiv f2).symm (Option.map (finCongr hn2) n)) := m:f1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }N:hf:f1 = f2n:Option (Fin N)hn1:N = {i | f1 i = i}.cardhn2:N = {i | f2 i = i}.card(involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn1)) n) (involutionAddEquiv f2).symm (Option.map (⇑(finCongr hn2)) n) m:f1:{ f // Function.Involutive f }N:n:Option (Fin N)hn1:N = {i | f1 i = i}.cardhn2:N = {i | f1 i = i}.card(involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn1)) n) (involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn2)) n) All goals completed! 🐙lemma involutionAddEquiv_none_succ {n : } {f : {f : Fin n.succ Fin n.succ // Function.Involutive f}} (h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none) (x : Fin n) : f.1 x.succ = x.succ (involutionCons n f).1.1 x = x := n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin nf x.succ = x.succ ((involutionCons n) f).fst x = x n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin nf x.succ = x.succ (h : ¬f x.succ = 0), (f x.succ).pred h = x n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin nhx:¬f x.succ = 0, f x.succ = x.succ (h : ¬f x.succ = 0), (f x.succ).pred h = x exact Iff.intro (fun h2 n:f:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin nhx:¬f x.succ = 0, h2:f x.succ = x.succ (h : ¬f x.succ = 0), (f x.succ).pred h = x All goals completed! 🐙) (fun h2 (Fin.pred_eq_iff_eq_succ hx).mp (h2 hx))

Equivalences of involutions with no fixed points.

The main aim of these equivalences is to define involutionNoFixedZeroEquivProd.

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

def involutionNoFixedEquivSum {n : } : {f : Fin n.succ Fin n.succ // Function.Involutive f i, f i i} Σ (k : Fin n), {f : Fin n.succ Fin n.succ // Function.Involutive f ( i, f i i) f 0 = k.succ} where toFun f := (f.1 0).pred (f.2.2 0), f.1, f.2.1, n:f:{ f // Function.Involutive f (i : Fin n.succ), f i i }(∀ (i : Fin n.succ), f i i) f 0 = ((f 0).pred ).succ All goals completed! 🐙 invFun f := f.2.1, f.2.2.1, f.2.2.2.1 left_inv f := rfl right_inv f := n:f:(k : Fin n) × { f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }(fun f => (f 0).pred , f, ) ((fun f => f.snd, ) f) = f n:f:(k : Fin n) × { f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }((fun f => (f 0).pred , f, ) ((fun f => f.snd, ) f)).fst = f.fstn:f:(k : Fin n) × { f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }x✝:Fin n.succ(((fun f => (f 0).pred , f, ) ((fun f => f.snd, ) f)).snd x✝) = (f.snd x✝) n:f:(k : Fin n) × { f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }((fun f => (f 0).pred , f, ) ((fun f => f.snd, ) f)).fst = f.fstn:f:(k : Fin n) × { f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }x✝:Fin n.succ(((fun f => (f 0).pred , f, ) ((fun f => f.snd, ) f)).snd x✝) = (f.snd x✝) try All goals completed! 🐙

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.

All goals completed! 🐙, n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ } (i : Fin n.succ), (e.symm (e f e.symm) e) i i All goals completed! 🐙, n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }(e.symm (e f e.symm) e) 0 = k.succ All goals completed! 🐙 invFun f := e.symm f.1 e, n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive (e.symm f e) (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ }Function.Involutive (e.symm f e) n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive (e.symm f e) (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ }i:Fin n.succ(e.symm f e) ((e.symm f e) i) = i All goals completed! 🐙, n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive (e.symm f e) (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ } (i : Fin n.succ), (e.symm f e) i i All goals completed! 🐙, n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive (e.symm f e) (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ }(e.symm f e) 0 = k.succ All goals completed! 🐙 left_inv f := n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }(fun f => e.symm f e, ) ((fun f => e f e.symm, ) f) = f n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f 0 = k.succ }i:Fin n.succ(((fun f => e.symm f e, ) ((fun f => e f e.symm, ) f)) i) = (f i); All goals completed! 🐙 right_inv f := n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive (e.symm f e) (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ }(fun f => e f e.symm, ) ((fun f => e.symm f e, ) f) = f n:k:Fin ne:Fin n.succ Fin n.succf:{ f // Function.Involutive (e.symm f e) (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ }i:Fin n.succ(((fun f => e f e.symm, ) ((fun f => e.symm f e, ) f)) i) = (f i); All goals completed! 🐙

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.

n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1:Function.Involutive (e.symm f e) Function.Involutive fFunction.Involutive f (∀ (i : Fin n.succ), (e.symm f e) i i) (e.symm f e) 0 = k.succ Function.Involutive f (∀ (i : Fin n.succ), f i i) (e.symm f e) 0 = k.succ n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1:Function.Involutive (e.symm f e) Function.Involutive fFunction.Involutive f e.symm (f (e 0)) = k.succ ((∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) (i : Fin (n + 1)), ¬f i = i) n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ(∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) (i : Fin (n + 1)), ¬f i = i n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ(∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) (i : Fin (n + 1)), ¬f i = in:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ(∀ (i : Fin (n + 1)), ¬f i = i) (i : Fin (n + 1)), ¬e.symm (f (e i)) = i n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ(∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) (i : Fin (n + 1)), ¬f i = i n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh: (i : Fin (n + 1)), ¬e.symm (f (e i)) = ii:Fin (n + 1)¬f i = i All goals completed! 🐙 n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ(∀ (i : Fin (n + 1)), ¬f i = i) (i : Fin (n + 1)), ¬e.symm (f (e i)) = i n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh: (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)¬e.symm (f (e i)) = i n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh: (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)hi:¬f (e i) = e i¬e.symm (f (e i)) = i n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh: (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)hi:¬f (e i) = e ihn:e.symm (f (e i)) = iFalse n:k:Fin ne:Fin n.succ Fin n.succf:Fin n.succ Fin n.succh1✝:Function.Involutive (e.symm f e) Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh: (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)hi:¬f (e i) = e (e.symm (f (e i)))hn:e.symm (f (e i)) = iFalse All goals completed! 🐙

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.

def involutionNoFixedZeroSetEquivEquiv' {n : } (k : Fin n) (e : Fin n.succ Fin n.succ) : {f : Fin n.succ Fin n.succ // Function.Involutive f ( i, f i i) (e.symm f e) 0 = k.succ} {f : Fin n.succ Fin n.succ // Function.Involutive f ( i, f i i) f (e 0) = e k.succ} := n:k:Fin ne:Fin n.succ Fin n.succ{ f // Function.Involutive f (∀ (i : Fin n.succ), f i i) (e.symm f e) 0 = k.succ } { f // Function.Involutive f (∀ (i : Fin n.succ), f i i) f (e 0) = e k.succ } n:k:Fin ne:Fin n.succ Fin n.succ (x : Fin n.succ Fin n.succ), Function.Involutive x (∀ (i : Fin n.succ), x i i) (e.symm x e) 0 = k.succ Function.Involutive x (∀ (i : Fin n.succ), x i i) x (e 0) = e k.succ n:k:Fin ne:Fin n.succ Fin n.succ (x : Fin (n + 1) Fin (n + 1)), Function.Involutive x (∀ (i : Fin (n + 1)), ¬x i = i) (e.symm (x (e 0)) = k.succ x (e 0) = e k.succ) n:k:Fin ne:Fin n.succ Fin n.succf:Fin (n + 1) Fin (n + 1)hi:Function.Involutive fh1: (i : Fin (n + 1)), ¬f i = ie.symm (f (e 0)) = k.succ f (e 0) = e k.succ All goals completed! 🐙

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

n:k:Fin n.succf:Fin (n + 1 + 1) Fin (n + 1 + 1)hi:Function.Involutive fh1: (i : Fin (n + 1 + 1)), ¬f i = i0 k.succn:k:Fin n.succf:Fin (n + 1 + 1) Fin (n + 1 + 1)hi:Function.Involutive fh1: (i : Fin (n + 1 + 1)), ¬f i = i0 1 n:k:Fin n.succf:Fin (n + 1 + 1) Fin (n + 1 + 1)hi:Function.Involutive fh1: (i : Fin (n + 1 + 1)), ¬f i = i0 k.succ All goals completed! 🐙 n:k:Fin n.succf:Fin (n + 1 + 1) Fin (n + 1 + 1)hi:Function.Involutive fh1: (i : Fin (n + 1 + 1)), ¬f i = i0 1 All goals completed! 🐙

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

n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0(fun f => let f' := fun i => match i with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => (f n_1, ).succ.succ; f', ) ((fun f => have f_succ_succ_ne_zero_one := ; let f' := f Fin.succ Fin.succ; have hf' := ; let f'' := fun i => (f' i).pred ; have hf'' := ; let f''' := fun i => (f'' i).pred ; f''', ) f) = f n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0fun i => match i with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => f n_1 + 1 + 1, , = f n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i:Fin (n + 1 + 1)(fun i => match i with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => f n_1 + 1 + 1, , i) = (f i) n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i:Fin (n + 1 + 1)(match i with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => f n_1 + 1 + 1, ) = (f i) n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i✝:Fin n✝.succ.succh✝:0 < n.succ.succ1 = (f 0, h✝)n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i✝:Fin n✝.succ.succh✝:1 < n.succ.succ0 = (f 1, h✝)n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succ(f n✝ + 1 + 1, ) = (f n✝.succ.succ, h✝) n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i✝:Fin n✝.succ.succh✝:0 < n.succ.succ1 = (f 0, h✝) All goals completed! 🐙 n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i✝:Fin n✝.succ.succh✝:1 < n.succ.succ0 = (f 1, h✝) All goals completed! 🐙 n:f:{ f // Function.Involutive f (∀ (i : Fin n.succ.succ), f i i) f 0 = 1 }hf1:f 1 = 0i✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succ(f n✝ + 1 + 1, ) = (f n✝.succ.succ, h✝) All goals completed! 🐙 right_inv f := n:f:{ f // Function.Involutive f (i : Fin n), f i i }(fun f => have f_succ_succ_ne_zero_one := ; let f' := f Fin.succ Fin.succ; have hf' := ; let f'' := fun i => (f' i).pred ; have hf'' := ; let f''' := fun i => (f'' i).pred ; f''', ) ((fun f => let f' := fun i => match i with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => (f n_1, ).succ.succ; f', ) f) = f n:f:{ f // Function.Involutive f (i : Fin n), f i i }fun i => ((match i.succ.succ with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => (f n_1, ).succ.succ).pred ).pred , = f n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin n(fun i => ((match i.succ.succ with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => (f n_1, ).succ.succ).pred ).pred , i) = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin n(match i.succ.succ with | 0, h => 1 | 1, h => 0 | n_1.succ.succ, h => (f n_1, ).succ.succ) - 1 - 1 = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:i.succ.succ = 0, h✝1 - 1 - 1 = (f i)n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:i.succ.succ = 1, h✝0 - 1 - 1 = (f i)n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = n✝.succ.succ, h✝(f n✝, ).succ.succ - 1 - 1 = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:i.succ.succ = 0, h✝1 - 1 - 1 = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succh✝:0 < n.succ.succh:i.succ.succ = 0, h✝1 - 1 - 1 = (f i) All goals completed! 🐙 n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:i.succ.succ = 1, h✝0 - 1 - 1 = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succh✝:1 < n.succ.succh:i.succ.succ = 1, h✝0 - 1 - 1 = (f i) All goals completed! 🐙 n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = n✝.succ.succ, h✝(f n✝, ).succ.succ - 1 - 1 = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = n✝.succ.succ, h✝(f n✝, ) = (f i) n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = n✝.succ.succ, h✝f n✝, = f i n:f:{ f // Function.Involutive f (i : Fin n), f i i }i:Fin ni✝:Fin n✝.succ.succn✝:h✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = n✝.succ.succ, h✝n✝, = i All goals completed! 🐙

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

def involutionNoFixedZeroSetEquiv {n : } (k : Fin n.succ) : {f : Fin n.succ.succ Fin n.succ.succ // Function.Involutive f ( i, f i i) f 0 = k.succ} {f : Fin n Fin n // Function.Involutive f ( i, f i i)} := (involutionNoFixedZeroSetEquivSetOne k).trans involutionNoFixedSetOne

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.

def involutionNoFixedEquivSumSame {n : } : {f : Fin n.succ.succ Fin n.succ.succ // Function.Involutive f ( i, f i i)} Σ (_ : Fin n.succ), {f : Fin n Fin n // Function.Involutive f ( i, f i i)} := involutionNoFixedEquivSum.trans <| .sigmaCongrRight involutionNoFixedZeroSetEquiv

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.

def involutionNoFixedZeroEquivProd {n : } : {f : Fin n.succ.succ Fin n.succ.succ // Function.Involutive f ( i, f i i)} Fin n.succ × {f : Fin n Fin n // Function.Involutive f ( i, f i i)} := involutionNoFixedEquivSumSame.trans <| .sigmaEquivProd ..

Cardinality

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

instance {n : } : Fintype { f // Function.Involutive f (i : Fin n), f i i } := n:Fintype { f // Function.Involutive f (i : Fin n), f i i } n:this:DecidablePred fun x => Function.Involutive xFintype { f // Function.Involutive f (i : Fin n), f i i } All goals completed! 🐙
lemma involutionNoFixed_card_succ {n : } : Fintype.card {f : Fin n.succ.succ Fin n.succ.succ // Function.Involutive f ( i, f i i)} = n.succ * Fintype.card {f : Fin n Fin n // Function.Involutive f ( i, f i i)} := n:Fintype.card { f // Function.Involutive f (i : Fin n.succ.succ), f i i } = n.succ * Fintype.card { f // Function.Involutive f (i : Fin n), f i i } All goals completed! 🐙lemma involutionNoFixed_card_mul_two : (n : ) Fintype.card {f : Fin (2 * n) Fin (2 * n) // Function.Involutive f ( i, f i i)} = (2 * n - 1) | 0 => rfl n:Fintype.card { f // Function.Involutive f (i : Fin (2 * n.succ)), f i i } = (2 * n.succ - 1) n:Fintype.card { f // Function.Involutive f (i : Fin (2 * n.succ)), f i i } = (2 * n.succ - 1) erw [n:(Nat.mul 2 n).succ * Fintype.card { f // Function.Involutive f (i : Fin (Nat.mul 2 n)), f i i } = (2 * n.succ - 1) n:(Nat.mul 2 n).succ * (2 * n - 1) = (2 * n.succ - 1)n:(Nat.mul 2 n).succ * (2 * n - 1) = (2 * n.succ - 1) All goals completed! 🐙lemma involutionNoFixed_card_mul_two_plus_one : (n : ) Fintype.card {f : Fin (2 * n + 1) Fin (2 * n + 1) // Function.Involutive f ( i, f i i)} = 0 | 0 => rfl n:Fintype.card { f // Function.Involutive f (i : Fin (2 * n.succ + 1)), f i i } = 0 n:Fintype.card { f // Function.Involutive f (i : Fin (2 * n.succ + 1)), f i i } = 0 erw [n:(Nat.mul 2 n + 1).succ * Fintype.card { f // Function.Involutive f (i : Fin (Nat.mul 2 n + 1)), f i i } = 0 n:(Nat.mul 2 n + 1).succ * 0 = 0n:(Nat.mul 2 n + 1).succ * 0 = 0 All goals completed! 🐙n:r:hr:n = r + rhr':n = 2 * rFintype.card { f // Function.Involutive f (i : Fin n), f i i } = (n - 1) r:hr:2 * r = r + rFintype.card { f // Function.Involutive f (i : Fin (2 * r)), f i i } = (2 * r - 1) All goals completed! 🐙lemma involutionNoFixed_card_odd : (n : ) (ho : Odd n) Fintype.card {f : Fin n Fin n // Function.Involutive f ( i, f i i)} = 0 := (n : ), Odd n Fintype.card { f // Function.Involutive f (i : Fin n), f i i } = 0 n:ho:Odd nFintype.card { f // Function.Involutive f (i : Fin n), f i i } = 0 n:r:hr:n = 2 * r + 1Fintype.card { f // Function.Involutive f (i : Fin n), f i i } = 0 r:Fintype.card { f // Function.Involutive f (i : Fin (2 * r + 1)), f i i } = 0 All goals completed! 🐙