From 812d86213abb792132ec954432af5fbeb9260d2b Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Mon, 4 Nov 2024 00:05:09 +0000 Subject: [PATCH] WIP Signed-off-by: zeramorphic --- ConNF.lean | 1 + ConNF/Construction/Code.lean | 12 ++ ConNF/Construction/NewModelData.lean | 167 +++++++++++++++++++++++++++ ConNF/Setup/Tree.lean | 31 +++-- 4 files changed, 203 insertions(+), 8 deletions(-) create mode 100644 ConNF/Construction/NewModelData.lean diff --git a/ConNF.lean b/ConNF.lean index 7708e543c7..fdeb3aec64 100644 --- a/ConNF.lean +++ b/ConNF.lean @@ -7,6 +7,7 @@ import ConNF.Aux.Set import ConNF.Aux.Transfer import ConNF.Aux.WellOrder import ConNF.Construction.Code +import ConNF.Construction.NewModelData import ConNF.Counting.BaseCoding import ConNF.Counting.BaseCounting import ConNF.Counting.CodingFunction diff --git a/ConNF/Construction/Code.lean b/ConNF/Construction/Code.lean index a15a4b7f1a..7c5474a6d1 100644 --- a/ConNF/Construction/Code.lean +++ b/ConNF/Construction/Code.lean @@ -23,6 +23,7 @@ class TypedNearLitters (α : Λ) [ModelData α] [Position (Tangle α)] where typed : NearLitter → TSet α typed_injective : Function.Injective typed pos_le_pos_of_typed (N : NearLitter) (t : Tangle α) : t.set = typed N → pos N ≤ pos t + smul_typed (ρ : AllPerm α) (N : NearLitter) : ρ • typed N = typed (ρᵁ ↘. • N) export TypedNearLitters (typed) @@ -194,6 +195,17 @@ theorem even_or_odd (c : Code) : c.Even ∨ c.Odd := by · exact .mk c d hd₁ hd · cases hd₂ hd +@[simp] +theorem not_even (c : Code) : ¬c.Even ↔ c.Odd := by + have := even_or_odd c + have := not_even_and_odd c + tauto + +@[simp] +theorem not_odd (c : Code) : ¬c.Odd ↔ c.Even := by + have := not_even c + tauto + inductive Represents : Rel Code Code | refl (c : Code) : c.Even → Represents c c | cloud (c d : Code) : c.Even → Cloud c d → Represents c d diff --git a/ConNF/Construction/NewModelData.lean b/ConNF/Construction/NewModelData.lean new file mode 100644 index 0000000000..89624a56fd --- /dev/null +++ b/ConNF/Construction/NewModelData.lean @@ -0,0 +1,167 @@ +import ConNF.Construction.Code + +/-! +# Construction of model data + +In this file, we construct model data at type `α`, given that it is defined at all types below `α`. + +## Main declarations + +* `ConNF.foo`: Something new. +-/ + +noncomputable section +universe u + +open Cardinal Ordinal +open scoped Pointwise + +namespace ConNF + +variable [Params.{u}] [Level] [LtData] + +@[ext] +structure NewPerm : Type u where + sderiv : (β : TypeIndex) → [LtLevel β] → AllPerm β + smul_fuzz {β : TypeIndex} {γ : Λ} [LtLevel β] [LtLevel γ] (hβγ : β ≠ γ) (t : Tangle β) : + (sderiv γ)ᵁ ↘. • fuzz hβγ t = fuzz hβγ (sderiv β • t) + +instance : Mul NewPerm where + mul ρ₁ ρ₂ := ⟨λ β _ ↦ ρ₁.sderiv β * ρ₂.sderiv β, by + intro β γ _ _ hβγ t + simp only [allPermForget_mul, mul_smul, Tree.mul_sderivBot, NewPerm.smul_fuzz]⟩ + +instance : One NewPerm where + one := ⟨λ _ _ ↦ 1, by + intro β γ _ _ hβγ t + simp only [allPermForget_one, one_smul, Tree.one_sderivBot]⟩ + +instance : Inv NewPerm where + inv ρ := ⟨λ β _ ↦ (ρ.sderiv β)⁻¹, by + intro β γ _ _ hβγ t + simp only [allPermForget_inv, Tree.inv_sderivBot, inv_smul_eq_iff, NewPerm.smul_fuzz, + smul_inv_smul]⟩ + +@[simp] +theorem mul_sderiv (ρ₁ ρ₂ : NewPerm) (β : TypeIndex) [LtLevel β] : + (ρ₁ * ρ₂).sderiv β = ρ₁.sderiv β * ρ₂.sderiv β := + rfl + +@[simp] +theorem one_sderiv (β : TypeIndex) [LtLevel β] : + (1 : NewPerm).sderiv β = 1 := + rfl + +@[simp] +theorem inv_sderiv (ρ : NewPerm) (β : TypeIndex) [LtLevel β] : + ρ⁻¹.sderiv β = (ρ.sderiv β)⁻¹ := + rfl + +instance : Group NewPerm where + mul_assoc ρ₁ ρ₂ ρ₃ := by + ext β : 3 + simp only [mul_sderiv, mul_assoc] + one_mul ρ := by + ext β : 3 + simp only [mul_sderiv, one_mul, one_sderiv] + mul_one ρ := by + ext β : 3 + simp only [mul_sderiv, mul_one, one_sderiv] + inv_mul_cancel ρ := by + ext β : 3 + simp only [mul_sderiv, inv_sderiv, inv_mul_cancel, one_sderiv] + +instance : SMul NewPerm Code where + smul ρ c := ⟨c.β, ρ.sderiv c.β • c.s, Set.smul_set_nonempty.mpr c.hs⟩ + +@[simp] +theorem NewPerm.smul_mk (ρ : NewPerm) (β : TypeIndex) [LtLevel β] + (s : Set (TSet β)) (hs : s.Nonempty) : + ρ • Code.mk β s hs = ⟨β, ρ.sderiv β • s, Set.smul_set_nonempty.mpr hs⟩ := + rfl + +instance : MulAction NewPerm Code where + one_smul := by + rintro ⟨β, s, hs⟩ + simp only [NewPerm.smul_mk, one_sderiv, one_smul] + mul_smul := by + rintro ρ₁ ρ₂ ⟨β, s, hs⟩ + simp only [NewPerm.smul_mk, mul_sderiv, mul_smul] + +theorem Cloud.smul {c d : Code} (h : Cloud c d) (ρ : NewPerm) : + Cloud (ρ • c) (ρ • d) := by + obtain ⟨β, γ, hβγ, s, hs⟩ := h + convert Cloud.mk β γ hβγ (ρ.sderiv β • s) (Set.smul_set_nonempty.mpr hs) using 1 + rw [NewPerm.smul_mk, Code.mk.injEq, heq_eq_eq] + use rfl + ext x + constructor + · rintro ⟨y, ⟨N, ⟨t, ht, hN⟩, rfl⟩, rfl⟩ + refine ⟨(ρ.sderiv γ)ᵁ ↘. • N, ⟨ρ.sderiv β • t, ?_, ?_⟩, ?_⟩ + · rwa [Tangle.smul_set, Set.smul_mem_smul_set_iff] + · rw [BasePerm.smul_nearLitter_litter, hN, NewPerm.smul_fuzz] + · rw [← TypedNearLitters.smul_typed] + · rintro ⟨N, ⟨t, ⟨x, hxs, hxt⟩, hN⟩, rfl⟩ + refine ⟨(ρ.sderiv γ)⁻¹ • typed N, + ⟨(ρ.sderiv γ)ᵁ⁻¹ ↘. • N, ⟨(ρ.sderiv β)⁻¹ • t, ?_, ?_⟩, ?_⟩, ?_⟩ + · rwa [Tangle.smul_set, ← hxt, inv_smul_smul] + · rw [Tree.inv_sderivBot, BasePerm.smul_nearLitter_litter, inv_smul_eq_iff, + NewPerm.smul_fuzz, smul_inv_smul, hN] + · rw [Tree.inv_sderivBot, TypedNearLitters.smul_typed, allPermForget_inv, Tree.inv_sderivBot] + · simp only [smul_inv_smul] + +@[simp] +theorem Code.smul_even {c : Code} (ρ : NewPerm) : + (ρ • c).Even ↔ c.Even := by + induction c using cloud_wf.induction + case h c ih => + constructor + · rintro ⟨_, hc⟩ + constructor + intro d hd + have := hc (ρ • d) (hd.smul ρ) + by_contra hd' + rw [not_odd, ← ih d hd] at hd' + exact not_even_and_odd _ ⟨hd', this⟩ + · rintro ⟨_, hc⟩ + constructor + intro d hd + have hc' := hc (ρ⁻¹ • d) ?_ + · have ih' := ih (ρ⁻¹ • d) ?_ + · rw [smul_inv_smul] at ih' + by_contra hd' + rw [not_odd, ih'] at hd' + exact not_even_and_odd _ ⟨hd', hc'⟩ + · have := hd.smul ρ⁻¹ + rwa [inv_smul_smul] at this + · have := hd.smul ρ⁻¹ + rwa [inv_smul_smul] at this + +theorem Represents.smul {c d : Code} (h : Represents c d) (ρ : NewPerm) : + Represents (ρ • c) (ρ • d) := by + obtain (⟨_, h⟩ | ⟨_, _, hc, hcd⟩) := h + · refine .refl _ ?_ + rwa [Code.smul_even] + · refine .cloud _ _ ?_ ?_ + · rwa [Code.smul_even] + · exact hcd.smul ρ + +def Path.untop {β γ : TypeIndex} (A : β ↝ γ) (h : β ≠ γ) : + ((δ : {δ : TypeIndex // δ < β}) × δ ↝ γ) := + A.recScoderiv (motive := λ ε _ ↦ ε ≠ γ → ((δ : {δ : TypeIndex // δ < ε}) × δ ↝ γ)) + (λ h ↦ (h rfl).elim) (λ ε ζ B hζ _ h ↦ ⟨⟨ζ, hζ⟩, B⟩) h + +def Path.recTop {β δ : TypeIndex} (hβδ : δ < β) {motive : Sort _} + (scoderiv : ∀ γ (h : γ < β), γ ↝ δ → motive) + {γ : TypeIndex} (A : β ↝ δ) : motive := + sorry + +-- instance : SuperU NewPerm (StrPerm α) where +-- superU ρ := λ A ↦ A.recScoderiv (motive := λ β _ ↦ BasePerm) _ (λ β γ B hγβ _ ↦ _) + +structure NewSet : Type u where + c : Code + hc : c.Even + hS : ∃ S : Support α, ∀ ρ : NewPerm, ρᵁ • S = S → ρ • c = c + +end ConNF diff --git a/ConNF/Setup/Tree.lean b/ConNF/Setup/Tree.lean index 2d681a8834..7c7a757e3e 100644 --- a/ConNF/Setup/Tree.lean +++ b/ConNF/Setup/Tree.lean @@ -84,6 +84,11 @@ theorem one_sderiv [Group X] (h : β < α) : (1 : Tree X α) ↘ h = 1 := rfl +@[simp] +theorem one_sderivBot [Group X] : + (1 : Tree X α) ↘. = 1 := + rfl + @[simp] theorem mul_apply [Group X] (T₁ T₂ : Tree X α) (A : α ↝ ⊥) : (T₁ * T₂) A = T₁ A * T₂ A := @@ -94,29 +99,39 @@ theorem mul_sderiv [Group X] (T₁ T₂ : Tree X α) (h : β < α) : (T₁ * T₂) ↘ h = T₁ ↘ h * T₂ ↘ h := rfl +@[simp] +theorem mul_sderivBot [Group X] (T₁ T₂ : Tree X α) : + (T₁ * T₂) ↘. = T₁ ↘. * T₂ ↘. := + rfl + @[simp] theorem inv_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) : T⁻¹ A = (T A)⁻¹ := rfl @[simp] -theorem npow_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℕ) : - (T ^ n) A = (T A) ^ n := +theorem inv_deriv [Group X] (T : Tree X α) (A : α ↝ β) : + T⁻¹ ⇘ A = (T ⇘ A)⁻¹ := rfl @[simp] -theorem zpow_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℤ) : - (T ^ n) A = (T A) ^ n := +theorem inv_sderiv [Group X] (T : Tree X α) (h : β < α) : + T⁻¹ ↘ h = (T ↘ h)⁻¹ := rfl @[simp] -theorem inv_deriv [Group X] (T : Tree X α) (A : α ↝ β) : - T⁻¹ ⇘ A = (T ⇘ A)⁻¹ := +theorem inv_sderivBot [Group X] (T : Tree X α) : + T⁻¹ ↘. = (T ↘.)⁻¹ := rfl @[simp] -theorem inv_sderiv [Group X] (T : Tree X α) (h : β < α) : - T⁻¹ ↘ h = (T ↘ h)⁻¹ := +theorem npow_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℕ) : + (T ^ n) A = (T A) ^ n := + rfl + +@[simp] +theorem zpow_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℤ) : + (T ^ n) A = (T A) ^ n := rfl /-- The partial order on the type of `α`-trees of `X` is given by "branchwise" comparison. -/