feat: equivalence between involutions and contractions
This commit is contained in:
jstoobysmith
parent
7d1f15e18a
commit
eadb354477
2 changed files with 416 additions and 67 deletions
|
|
@ -124,6 +124,14 @@ def consEquiv {φ : 𝓕} {φs : List 𝓕} :
|
|||
| ContractionsAux.cons (φsᵤₙ := aux') i c => rfl
|
||||
right_inv ci := by rfl
|
||||
|
||||
lemma consEquiv_ext {φs : List 𝓕} {c1 c2 : Contractions φs}
|
||||
{n1 : Option (Fin c1.normalize.length)} {n2 : Option (Fin c2.normalize.length)}
|
||||
(hc : c1 = c2) (hn : Option.map (finCongr (by rw [hc])) n1 = n2) :
|
||||
(⟨c1, n1⟩ : (c : Contractions φs) × Option (Fin c.normalize.length)) = ⟨c2, n2⟩ := by
|
||||
subst hc
|
||||
subst hn
|
||||
simp
|
||||
|
||||
/-- The type of contractions is decidable. -/
|
||||
instance decidable : (φs : List 𝓕) → DecidableEq (Contractions φs)
|
||||
| [] => fun a b =>
|
||||
|
|
@ -574,44 +582,24 @@ def involutionCons (n : ℕ):
|
|||
subst hs
|
||||
exact ne_of_beq_false rfl
|
||||
|
||||
def uncontractedFromInduction : {l : List 𝓕} → (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
|
||||
List 𝓕
|
||||
| [], _ => []
|
||||
| φ :: φs, f =>
|
||||
let f' := involutionCons φs.length f
|
||||
let c' := uncontractedFromInduction f'.1
|
||||
if f'.2.1.isSome then
|
||||
c'
|
||||
else
|
||||
φ :: c'
|
||||
lemma involutionCons_ext {n : ℕ} {f1 f2 : (f : {f : Fin n → Fin n // Function.Involutive f}) × {i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}}
|
||||
(h1 : f1.1 = f2.1) (h2 : f1.2 = Equiv.subtypeEquivRight (by rw [h1]; simp) f2.2) : f1 = f2 := by
|
||||
cases f1
|
||||
cases f2
|
||||
simp at h1 h2
|
||||
subst h1
|
||||
rename_i fst snd snd_1
|
||||
simp_all only [Sigma.mk.inj_iff, heq_eq_eq, true_and]
|
||||
obtain ⟨val, property⟩ := fst
|
||||
obtain ⟨val_1, property_1⟩ := snd
|
||||
obtain ⟨val_2, property_2⟩ := snd_1
|
||||
simp_all only
|
||||
rfl
|
||||
|
||||
lemma uncontractedFromInduction_length : {l : List 𝓕} → (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
|
||||
(uncontractedFromInduction f).length = ∑ i, if f.1 i = i then 1 else 0
|
||||
| [] => by
|
||||
intro f
|
||||
rfl
|
||||
| φ :: φs => by
|
||||
intro f
|
||||
let f' := involutionCons φs.length f
|
||||
let c' := uncontractedFromInduction f'.1
|
||||
by_cases h : f'.2.1.isSome
|
||||
· dsimp [uncontractedFromInduction]
|
||||
rw [if_pos h]
|
||||
rw [uncontractedFromInduction_length f'.1]
|
||||
rw [Fin.sum_univ_succ]
|
||||
simp [f', involutionCons] at h
|
||||
rw [if_neg h]
|
||||
simp
|
||||
sorry
|
||||
· sorry
|
||||
|
||||
|
||||
|
||||
|
||||
def uncontractedEquiv {l : List 𝓕} (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) :
|
||||
def uncontractedEquiv' {l : List 𝓕} (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) :
|
||||
{i : Option (Fin l.length) //
|
||||
∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)} ≃
|
||||
Option (Fin (uncontractedFromInduction f).length) := by
|
||||
Option (Fin (Finset.univ.filter fun i => f.1 i = i).card) := by
|
||||
let e1 : {i : Option (Fin l.length) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}
|
||||
≃ Option {i : Fin l.length // f.1 i = i} :=
|
||||
{ toFun := fun i => match i with
|
||||
|
|
@ -637,44 +625,395 @@ def uncontractedEquiv {l : List 𝓕} (f : {f : Fin l.length → Fin l.length //
|
|||
let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by
|
||||
refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
|
||||
simp [s]
|
||||
have hcard : (uncontractedFromInduction f).length = Finset.card s := by
|
||||
simp [s]
|
||||
rw [Finset.card_filter]
|
||||
rw [uncontractedFromInduction_length]
|
||||
sorry
|
||||
refine e1.trans (Equiv.optionCongr (e2'.trans (e2)))
|
||||
|
||||
|
||||
lemma uncontractedEquiv'_none_image_zero {φs : List 𝓕} {φ : 𝓕} :
|
||||
{f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}}
|
||||
→ uncontractedEquiv' (involutionCons φs.length f).1 (involutionCons φs.length f).2 = none
|
||||
→ f.1 ⟨0, Nat.zero_lt_succ φs.length⟩ = ⟨0, Nat.zero_lt_succ φs.length⟩ := by
|
||||
intro f h
|
||||
simp only [Nat.succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, uncontractedEquiv',
|
||||
Option.isSome_some, Option.get_some, Option.isSome_none, Equiv.trans_apply,
|
||||
Equiv.optionCongr_apply, Equiv.coe_trans, RelIso.coe_fn_toEquiv, Option.map_eq_none'] at h
|
||||
simp_all only [List.length_cons, Fin.zero_eta]
|
||||
obtain ⟨val, property⟩ := f
|
||||
simp_all only [List.length_cons]
|
||||
split at h
|
||||
next i i_1 h_1 heq =>
|
||||
split at heq
|
||||
next h_2 => simp_all only [reduceCtorEq]
|
||||
next h_2 => simp_all only [reduceCtorEq]
|
||||
next i h_1 heq =>
|
||||
split at heq
|
||||
next h_2 => simp_all only
|
||||
next h_2 => simp_all only [Subtype.mk.injEq, reduceCtorEq]
|
||||
|
||||
lemma uncontractedEquiv'_cast {l : List 𝓕} {f1 f2 : {f : Fin l.length → Fin l.length // Function.Involutive f}}
|
||||
(hf : f1 = f2):
|
||||
uncontractedEquiv' f1 = (Equiv.subtypeEquivRight (by rw [hf]; simp)).trans
|
||||
((uncontractedEquiv' f2).trans (Equiv.optionCongr (finCongr (by rw [hf])))):= by
|
||||
subst hf
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma uncontractedEquiv'_none_succ {φs : List 𝓕} {φ : 𝓕} :
|
||||
{f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}}
|
||||
→ uncontractedEquiv' (involutionCons φs.length f).1 (involutionCons φs.length f).2 = none
|
||||
→ ∀ (x : Fin φs.length), f.1 x.succ = x.succ ↔ (involutionCons φs.length f).1.1 x = x := by
|
||||
intro f h x
|
||||
simp [involutionCons]
|
||||
have hn' := uncontractedEquiv'_none_image_zero h
|
||||
have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ φs.length⟩:= by
|
||||
rw [← hn']
|
||||
exact fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
|
||||
apply Iff.intro
|
||||
· intro h2 h3
|
||||
rw [Fin.ext_iff]
|
||||
simp [h2]
|
||||
· intro h2
|
||||
have h2' := h2 hx
|
||||
conv_rhs => rw [← h2']
|
||||
simp
|
||||
|
||||
|
||||
lemma uncontractedEquiv'_isSome_image_zero {φs : List 𝓕} {φ : 𝓕} :
|
||||
{f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}}
|
||||
→ (uncontractedEquiv' (involutionCons φs.length f).1 (involutionCons φs.length f).2).isSome
|
||||
→ ¬ f.1 ⟨0, Nat.zero_lt_succ φs.length⟩ = ⟨0, Nat.zero_lt_succ φs.length⟩ := by
|
||||
intro f hf
|
||||
simp [uncontractedEquiv', involutionCons] at hf
|
||||
simp_all only [List.length_cons, Fin.zero_eta]
|
||||
obtain ⟨val, property⟩ := f
|
||||
simp_all only [List.length_cons]
|
||||
apply Aesop.BuiltinRules.not_intro
|
||||
intro a
|
||||
simp_all only [↓reduceDIte, Option.isSome_none, Bool.false_eq_true]
|
||||
|
||||
|
||||
|
||||
def uncontractedFromInvolution: {φs : List 𝓕} →
|
||||
(f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) →
|
||||
{l : List 𝓕 // l.length = (Finset.univ.filter fun i => f.1 i = i).card}
|
||||
| [], _ => ⟨[], by simp⟩
|
||||
| φ :: φs, f =>
|
||||
let luc := uncontractedFromInvolution (involutionCons φs.length f).fst
|
||||
let n' := uncontractedEquiv' (involutionCons φs.length f).1 (involutionCons φs.length f).2
|
||||
if hn : n' = none then
|
||||
have hn' := uncontractedEquiv'_none_image_zero (φs := φs) (φ := φ) (f := f) hn
|
||||
⟨optionEraseZ luc φ none, by
|
||||
simp [optionEraseZ]
|
||||
rw [← luc.2]
|
||||
conv_rhs => rw [Finset.card_filter]
|
||||
rw [Fin.sum_univ_succ]
|
||||
conv_rhs => erw [if_pos hn']
|
||||
ring_nf
|
||||
simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, Nat.cast_id,
|
||||
add_right_inj]
|
||||
rw [Finset.card_filter]
|
||||
apply congrArg
|
||||
funext i
|
||||
refine ite_congr ?h.h.h₁ (congrFun rfl) (congrFun rfl)
|
||||
rw [uncontractedEquiv'_none_succ hn]⟩
|
||||
else
|
||||
let n := n'.get (Option.isSome_iff_ne_none.mpr hn)
|
||||
let np : Fin luc.1.length := ⟨n.1, by
|
||||
rw [luc.2]
|
||||
exact n.prop⟩
|
||||
⟨optionEraseZ luc φ (some np), by
|
||||
let k' := (involutionCons φs.length f).2
|
||||
have hkIsSome : (k'.1).isSome := by
|
||||
simp [n', uncontractedEquiv' ] at hn
|
||||
split at hn
|
||||
· simp_all only [reduceCtorEq, not_false_eq_true, Nat.succ_eq_add_one, Option.isSome_some, k']
|
||||
· simp_all only [not_true_eq_false]
|
||||
let k := k'.1.get hkIsSome
|
||||
rw [optionEraseZ_some_length]
|
||||
have hksucc : k.succ = f.1 ⟨0, Nat.zero_lt_succ φs.length⟩ := by
|
||||
simp [k, k', involutionCons]
|
||||
have hzero : ⟨0, Nat.zero_lt_succ φs.length⟩ = f.1 k.succ := by
|
||||
rw [hksucc]
|
||||
rw [f.2]
|
||||
have hkcons : ((involutionCons φs.length) f).1.1 k = k := by
|
||||
exact k'.2 hkIsSome
|
||||
have hksuccNe : f.1 k.succ ≠ k.succ := by
|
||||
conv_rhs => rw [hksucc]
|
||||
exact fun hn => Fin.succ_ne_zero k (Function.Involutive.injective f.2 hn )
|
||||
have hluc : 1 ≤ luc.1.length := by
|
||||
simp
|
||||
use k
|
||||
simp [involutionCons]
|
||||
rw [hksucc, f.2]
|
||||
simp
|
||||
rw [propext (Nat.sub_eq_iff_eq_add' hluc)]
|
||||
have h0 : ¬ f.1 ⟨0, Nat.zero_lt_succ φs.length⟩ = ⟨0, Nat.zero_lt_succ φs.length⟩ := by
|
||||
exact Option.isSome_dite'.mp hkIsSome
|
||||
conv_rhs =>
|
||||
rw [Finset.card_filter]
|
||||
erw [Fin.sum_univ_succ]
|
||||
erw [if_neg h0]
|
||||
simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, List.length_cons,
|
||||
Nat.cast_id, zero_add]
|
||||
conv_rhs => lhs; rw [Eq.symm (Fintype.sum_ite_eq' k fun j => 1)]
|
||||
rw [← Finset.sum_add_distrib]
|
||||
rw [Finset.card_filter]
|
||||
apply congrArg
|
||||
funext i
|
||||
by_cases hik : i = k
|
||||
· subst hik
|
||||
simp [hkcons, hksuccNe]
|
||||
· simp [hik]
|
||||
refine ite_congr ?_ (congrFun rfl) (congrFun rfl)
|
||||
simp [involutionCons]
|
||||
have hfi : f.1 i.succ ≠ ⟨0, Nat.zero_lt_succ φs.length⟩ := by
|
||||
rw [hzero]
|
||||
by_contra hn
|
||||
have hik' := (Function.Involutive.injective f.2 hn)
|
||||
simp only [List.length_cons, Fin.succ_inj] at hik'
|
||||
exact hik hik'
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
have h' := h hfi
|
||||
conv_rhs => rw [← h']
|
||||
simp
|
||||
· intro h hfi
|
||||
simp [Fin.ext_iff]
|
||||
rw [h]
|
||||
simp⟩
|
||||
|
||||
def involutionEquiv : (l : List 𝓕) → Contractions l ≃
|
||||
{f : Fin l.length → Fin l.length // Function.Involutive f}
|
||||
| [] => {
|
||||
toFun := fun c => ⟨fun i => i, fun i => rfl⟩,
|
||||
invFun := fun f => ⟨[], ContractionsAux.nil⟩,
|
||||
left_inv := by
|
||||
intro a
|
||||
cases a
|
||||
rename_i aux c
|
||||
cases c
|
||||
lemma uncontractedFromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
|
||||
(f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}) :
|
||||
uncontractedFromInvolution f =
|
||||
optionEraseZ (uncontractedFromInvolution (involutionCons φs.length f).fst) φ
|
||||
(Option.map (finCongr ((uncontractedFromInvolution (involutionCons φs.length f).fst).2.symm))
|
||||
(uncontractedEquiv' (involutionCons φs.length f).1 (involutionCons φs.length f).2)) := by
|
||||
let luc := uncontractedFromInvolution (involutionCons φs.length f).fst
|
||||
let n' := uncontractedEquiv' (involutionCons φs.length f).1 (involutionCons φs.length f).2
|
||||
change _ = optionEraseZ luc φ
|
||||
(Option.map (finCongr ((uncontractedFromInvolution (involutionCons φs.length f).fst).2.symm)) n')
|
||||
dsimp [uncontractedFromInvolution]
|
||||
by_cases hn : n' = none
|
||||
· have hn' := hn
|
||||
simp [n'] at hn'
|
||||
simp [hn']
|
||||
rw [hn]
|
||||
rfl
|
||||
· have hn' := hn
|
||||
simp [n'] at hn'
|
||||
simp [hn']
|
||||
congr
|
||||
simp [n']
|
||||
simp_all only [Nat.succ_eq_add_one, not_false_eq_true, n', luc]
|
||||
obtain ⟨val, property⟩ := f
|
||||
obtain ⟨val_1, property_1⟩ := luc
|
||||
simp_all only [Nat.succ_eq_add_one, List.length_cons]
|
||||
ext a : 1
|
||||
simp_all only [Option.mem_def, Option.some.injEq, Option.map_eq_some', finCongr_apply]
|
||||
apply Iff.intro
|
||||
· intro a_1
|
||||
subst a_1
|
||||
apply Exists.intro
|
||||
· apply And.intro
|
||||
on_goal 2 => {rfl
|
||||
}
|
||||
· simp_all only [Option.some_get]
|
||||
· intro a_1
|
||||
obtain ⟨w, h⟩ := a_1
|
||||
obtain ⟨left, right⟩ := h
|
||||
subst right
|
||||
simp_all only [Option.get_some]
|
||||
rfl
|
||||
right_inv := by
|
||||
intro f
|
||||
ext i
|
||||
exact Fin.elim0 i}
|
||||
| φ :: φs => by
|
||||
refine Equiv.trans consEquiv ?_
|
||||
refine Equiv.trans ?_ (involutionCons φs.length).symm
|
||||
refine Equiv.sigmaCongr (involutionEquiv φs) (fun c => ?_)
|
||||
exact {
|
||||
toFun := fun i? => ⟨Option.map c.embedUncontracted i?, by
|
||||
intro h
|
||||
|
||||
sorry⟩
|
||||
invFun := fun i => sorry
|
||||
left_inv := by
|
||||
sorry
|
||||
right_inv := by sorry
|
||||
}
|
||||
def auxCongr : {φs: List 𝓕} → {φsᵤₙ φsᵤₙ' : List 𝓕} → (h : φsᵤₙ = φsᵤₙ') →
|
||||
ContractionsAux φs φsᵤₙ ≃ ContractionsAux φs φsᵤₙ'
|
||||
| _, _, _, Eq.refl _ => Equiv.refl _
|
||||
|
||||
lemma auxCongr_ext {φs: List 𝓕} {c c2 : Contractions φs} (h : c.1 = c2.1)
|
||||
(hx : c.2 = auxCongr h.symm c2.2) : c = c2 := by
|
||||
cases c
|
||||
cases c2
|
||||
simp at h
|
||||
subst h
|
||||
simp [auxCongr] at hx
|
||||
subst hx
|
||||
rfl
|
||||
|
||||
|
||||
lemma uncontractedEquiv'_cast' {l : List 𝓕} {f1 f2 : {f : Fin l.length → Fin l.length // 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 ((uncontractedEquiv' f1).symm (Option.map (finCongr hn1) n)) ((uncontractedEquiv' f2).symm (Option.map (finCongr hn2) n)) := by
|
||||
subst hf
|
||||
rfl
|
||||
|
||||
def toInvolution' : {φs : List 𝓕} → (c : Contractions φs) →
|
||||
{f : {f : Fin φs.length → Fin φs.length // Function.Involutive f} //
|
||||
uncontractedFromInvolution f = c.1}
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => ⟨⟨fun i => i, by
|
||||
intro i
|
||||
simp⟩, by rfl⟩
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) n c⟩ => by
|
||||
let ⟨⟨f', hf1⟩, hf2⟩ := toInvolution' ⟨aux, c⟩
|
||||
let n' : Option (Fin (uncontractedFromInvolution ⟨f', hf1⟩).1.length) :=
|
||||
Option.map (finCongr (by rw [hf2])) n
|
||||
let F := (involutionCons φs.length).symm ⟨⟨f', hf1⟩,
|
||||
(uncontractedEquiv' ⟨f', hf1⟩).symm
|
||||
(Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩
|
||||
refine ⟨F, ?_⟩
|
||||
have hF0 : ((involutionCons φs.length) F) = ⟨⟨f', hf1⟩,
|
||||
(uncontractedEquiv' ⟨f', hf1⟩).symm
|
||||
(Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩ := by
|
||||
simp [F]
|
||||
have hF1 : ((involutionCons φs.length) F).fst = ⟨f', hf1⟩ := by
|
||||
rw [hF0]
|
||||
have hF2L : ((uncontractedFromInvolution ⟨f', hf1⟩)).1.length =
|
||||
(Finset.filter (fun i => ((involutionCons φs.length) F).1.1 i = i) Finset.univ).card := by
|
||||
apply Eq.trans ((uncontractedFromInvolution ⟨f', hf1⟩)).2
|
||||
congr
|
||||
rw [hF1]
|
||||
have hF2 : ((involutionCons φs.length) F).snd = (uncontractedEquiv' ((involutionCons φs.length) F).fst).symm
|
||||
(Option.map (finCongr hF2L) n') := by
|
||||
rw [@Sigma.subtype_ext_iff] at hF0
|
||||
ext1
|
||||
rw [hF0.2]
|
||||
simp
|
||||
congr 1
|
||||
· rw [hF1]
|
||||
· refine uncontractedEquiv'_cast' ?_ n' _ _
|
||||
rw [hF1]
|
||||
rw [uncontractedFromInvolution_cons]
|
||||
have hx := (toInvolution' ⟨aux, c⟩).2
|
||||
simp at hx
|
||||
simp
|
||||
refine optionEraseZ_ext ?_ ?_ ?_
|
||||
· dsimp [F]
|
||||
rw [Equiv.apply_symm_apply]
|
||||
simp
|
||||
rw [← hx]
|
||||
simp_all only
|
||||
· rfl
|
||||
· simp [hF2]
|
||||
dsimp [n']
|
||||
simp [finCongr]
|
||||
simp only [Nat.succ_eq_add_one, id_eq, eq_mpr_eq_cast, F, n']
|
||||
ext a : 1
|
||||
simp only [Option.mem_def, Option.map_eq_some', Function.comp_apply, Fin.cast_trans,
|
||||
Fin.cast_eq_self, exists_eq_right]
|
||||
|
||||
lemma toInvolution'_length {φs φsᵤₙ : List 𝓕} {c : ContractionsAux φs φsᵤₙ} :
|
||||
φsᵤₙ.length = (Finset.filter (fun i => (toInvolution' ⟨φsᵤₙ, c⟩).1.1 i = i) Finset.univ).card
|
||||
:= by
|
||||
have h2 := (toInvolution' ⟨φsᵤₙ, c⟩).2
|
||||
simp at h2
|
||||
conv_lhs => rw [← h2]
|
||||
exact Mathlib.Vector.length_val (uncontractedFromInvolution (toInvolution' ⟨φsᵤₙ, c⟩).1)
|
||||
|
||||
lemma toInvolution'_cons {φs φsᵤₙ : List 𝓕} {φ : 𝓕}
|
||||
(c : ContractionsAux φs φsᵤₙ) (n : Option (Fin (φsᵤₙ.length))) :
|
||||
(toInvolution' ⟨optionEraseZ φsᵤₙ φ n, ContractionsAux.cons n c⟩).1
|
||||
= (involutionCons φs.length).symm ⟨(toInvolution' ⟨φsᵤₙ, c⟩).1,
|
||||
(uncontractedEquiv' (toInvolution' ⟨φsᵤₙ, c⟩).1).symm
|
||||
(Option.map (finCongr (toInvolution'_length)) n)⟩ := by
|
||||
dsimp [toInvolution']
|
||||
congr 3
|
||||
rw [Option.map_map]
|
||||
simp [finCongr]
|
||||
rfl
|
||||
|
||||
lemma toInvolution_consEquiv {φs : List 𝓕} {φ : 𝓕}
|
||||
(c : Contractions φs) (n : Option (Fin (c.normalize.length))) :
|
||||
(toInvolution' ((consEquiv (φ := φ)).symm ⟨c, n⟩)).1 =
|
||||
(involutionCons φs.length).symm ⟨(toInvolution' c).1,
|
||||
(uncontractedEquiv' (toInvolution' c).1).symm
|
||||
(Option.map (finCongr (toInvolution'_length)) n)⟩ := by
|
||||
erw [toInvolution'_cons]
|
||||
rfl
|
||||
|
||||
def fromInvolutionAux : {l : List 𝓕} →
|
||||
(f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
|
||||
ContractionsAux l (uncontractedFromInvolution f)
|
||||
| [] => fun _ => ContractionsAux.nil
|
||||
| _ :: φs => fun f =>
|
||||
let f' := involutionCons φs.length f
|
||||
let c' := fromInvolutionAux f'.1
|
||||
let n' := Option.map (finCongr ((uncontractedFromInvolution f'.fst).2.symm))
|
||||
(uncontractedEquiv' f'.1 f'.2)
|
||||
auxCongr (uncontractedFromInvolution_cons f).symm (ContractionsAux.cons n' c')
|
||||
|
||||
def fromInvolution {φs : List 𝓕} (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) :
|
||||
Contractions φs := ⟨uncontractedFromInvolution f, fromInvolutionAux f⟩
|
||||
|
||||
lemma fromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
|
||||
(f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}) :
|
||||
let f' := involutionCons φs.length f
|
||||
fromInvolution f = consEquiv.symm
|
||||
⟨fromInvolution f'.1, Option.map (finCongr ((uncontractedFromInvolution f'.fst).2.symm))
|
||||
(uncontractedEquiv' f'.1 f'.2)⟩ := by
|
||||
refine auxCongr_ext ?_ ?_
|
||||
· dsimp [fromInvolution]
|
||||
rw [uncontractedFromInvolution_cons]
|
||||
rfl
|
||||
· dsimp [fromInvolution, fromInvolutionAux]
|
||||
rfl
|
||||
|
||||
lemma fromInvolution_of_involutionCons
|
||||
{φs : List 𝓕} {φ : 𝓕}
|
||||
(f : {f : Fin (φs ).length → Fin (φs).length // Function.Involutive f})
|
||||
(n : { i : Option (Fin φs.length) // ∀ (h : i.isSome = true), f.1 (i.get h) = i.get h }):
|
||||
fromInvolution (φs := φ :: φs) ((involutionCons φs.length).symm ⟨f, n⟩) =
|
||||
consEquiv.symm
|
||||
⟨fromInvolution f, Option.map (finCongr ((uncontractedFromInvolution f).2.symm))
|
||||
(uncontractedEquiv' f n)⟩ := by
|
||||
rw [fromInvolution_cons]
|
||||
congr 1
|
||||
simp
|
||||
rw [Equiv.apply_symm_apply]
|
||||
|
||||
|
||||
|
||||
|
||||
lemma toInvolution_fromInvolution : {φs : List 𝓕} → (c : Contractions φs) →
|
||||
fromInvolution (toInvolution' c) = c
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => rfl
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := φsᵤₙ) n c⟩ => by
|
||||
rw [toInvolution'_cons]
|
||||
rw [fromInvolution_of_involutionCons]
|
||||
rw [Equiv.symm_apply_eq]
|
||||
dsimp [consEquiv]
|
||||
refine consEquiv_ext ?_ ?_
|
||||
· exact toInvolution_fromInvolution ⟨φsᵤₙ, c⟩
|
||||
· simp [finCongr]
|
||||
ext a : 1
|
||||
simp only [Option.mem_def, Option.map_eq_some', Function.comp_apply, Fin.cast_trans,
|
||||
Fin.cast_eq_self, exists_eq_right]
|
||||
|
||||
lemma fromInvolution_toInvolution : {φs : List 𝓕} → (f : {f : Fin (φs ).length → Fin (φs).length // Function.Involutive f})
|
||||
→ toInvolution' (fromInvolution f) = f
|
||||
| [], _ => by
|
||||
ext x
|
||||
exact Fin.elim0 x
|
||||
| φ :: φs, f => by
|
||||
rw [fromInvolution_cons]
|
||||
rw [toInvolution_consEquiv]
|
||||
erw [Equiv.symm_apply_eq]
|
||||
have hx := fromInvolution_toInvolution ((involutionCons φs.length) f).fst
|
||||
apply involutionCons_ext ?_ ?_
|
||||
· simp only [Nat.succ_eq_add_one, List.length_cons]
|
||||
exact hx
|
||||
· simp only [Nat.succ_eq_add_one, Option.map_map, List.length_cons]
|
||||
rw [Equiv.symm_apply_eq]
|
||||
conv_rhs =>
|
||||
lhs
|
||||
rw [uncontractedEquiv'_cast hx]
|
||||
simp [Nat.succ_eq_add_one,- eq_mpr_eq_cast, Equiv.trans_apply, -Equiv.optionCongr_apply]
|
||||
rfl
|
||||
|
||||
def equivInvolutions {φs : List 𝓕} :
|
||||
Contractions φs ≃ {f : Fin φs.length → Fin φs.length // Function.Involutive f} where
|
||||
toFun := fun c => toInvolution' c
|
||||
invFun := fromInvolution
|
||||
left_inv := toInvolution_fromInvolution
|
||||
right_inv := fromInvolution_toInvolution
|
||||
|
||||
/-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
|
||||
the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue