New file

In this file...

Main declarations

• ConNF.foo: Something new.

class ConNF.BaseActionClass [ConNF.Params] (X : Type u_1) : Type (max u u_1)

• atoms : X → Rel ConNF.Atom ConNF.Atom
• atoms_oneOne : ∀ (ξ : X), (ConNF.BaseActionClass.atoms ξ).OneOne
• nearLitters : X → Rel ConNF.NearLitter ConNF.NearLitter
• nearLitters_oneOne : ∀ (ξ : X), (ConNF.BaseActionClass.nearLitters ξ).OneOne

instance ConNF.instSuperARelAtomOfBaseActionClass [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] : ConNF.SuperA X (Rel ConNF.Atom ConNF.Atom)

Equations

• ConNF.instSuperARelAtomOfBaseActionClass = { superA := ConNF.BaseActionClass.atoms }

instance ConNF.instSuperNRelNearLitterOfBaseActionClass [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] : ConNF.SuperN X (Rel ConNF.NearLitter ConNF.NearLitter)

Equations

• ConNF.instSuperNRelNearLitterOfBaseActionClass = { superN := ConNF.BaseActionClass.nearLitters }

instance ConNF.instSMulBaseSupportOfBaseActionClass [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] : SMul X ConNF.BaseSupport

Equations

• ConNF.instSMulBaseSupportOfBaseActionClass = { smul := fun (ξ : X) (S : ConNF.BaseSupport) => { atoms := Sᴬ.comp ξᴬ ⋯, nearLitters := Sᴺ.comp ξᴺ ⋯ } }

instance ConNF.instSMulTreeSupportOfBaseActionClass [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] {β : ConNF.TypeIndex} : SMul (ConNF.Tree X β) (ConNF.Support β)

Equations

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

theorem ConNF.smul_atoms [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] (ξ : X) (S : ConNF.BaseSupport) : (ξ • S)ᴬ = Sᴬ.comp ξᴬ ⋯

theorem ConNF.smul_nearLitters [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] (ξ : X) (S : ConNF.BaseSupport) : (ξ • S)ᴺ = Sᴺ.comp ξᴺ ⋯

theorem ConNF.smul_baseSupport_eq_smul_iff [ConNF.Params] {X : Type u_1} [ConNF.BaseActionClass X] (ξ : X) (S : ConNF.BaseSupport) (π : ConNF.BasePerm) : ξ • S = π • S ↔ (∀ a ∈ Sᴬ, ξᴬ a (π • a)) ∧ ∀ N ∈ Sᴺ, ξᴺ N (π • N)

@[simp]

theorem ConNF.smul_support_derivBot [ConNF.Params] {β : ConNF.TypeIndex} {X : Type u_1} [ConNF.BaseActionClass X] (ξ : ConNF.Tree X β) (S : ConNF.Support β) (A : β ↝ ⊥) : (ξ • S) ⇘. A = ξ A • S ⇘. A

theorem ConNF.smul_support_eq_smul_iff [ConNF.Params] {β : ConNF.TypeIndex} {X : Type u_1} [ConNF.BaseActionClass X] (ξ : ConNF.Tree X β) (S : ConNF.Support β) (π : ConNF.StrPerm β) : ξ • S = π • S ↔ ∀ (A : β ↝ ⊥), (∀ a ∈ (S ⇘. A)ᴬ, (ξ A)ᴬ a (π A • a)) ∧ ∀ N ∈ (S ⇘. A)ᴺ, (ξ A)ᴺ N (π A • N)

theorem ConNF.smul_support_smul_eq_iff [ConNF.Params] {β : ConNF.TypeIndex} {X : Type u_1} [ConNF.BaseActionClass X] (ξ : ConNF.Tree X β) (S : ConNF.Support β) (π : ConNF.StrPerm β) : ξ • π • S = S ↔ ∀ (A : β ↝ ⊥), (∀ a ∈ ((π • S) ⇘. A)ᴬ, (ξ A)ᴬ a (π⁻¹ A • a)) ∧ ∀ N ∈ ((π • S) ⇘. A)ᴺ, (ξ A)ᴺ N (π⁻¹ A • N)

structure ConNF.CoherentAt [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {X : Type u_1} [ConNF.BaseActionClass X] (ξ : ConNF.Tree X β) (A : β ↝ ⊥) (L₁ L₂ : ConNF.Litter) : Prop

ξ is defined coherently at (A, L₁, L₂) (or could be defined coherently at this triple).

• inflexible : ∀ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → L₁ = ConNF.fuzz ⋯ t → ∃ (ρ : ConNF.AllPerm P.δ), ξ ⇘ P.A ↘ ⋯ • t.support = ρᵁ • t.support ∧ L₂ = ConNF.fuzz ⋯ (ρ • t)
• flexible : ¬ConNF.Inflexible A L₁ → ¬ConNF.Inflexible A L₂

theorem ConNF.coherentAt_inflexible [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {X : Type u_1} [ConNF.BaseActionClass X] {ξ : ConNF.Tree X β} {A : β ↝ ⊥} {L₁ L₂ : ConNF.Litter} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (ht : L₁ = ConNF.fuzz ⋯ t) : ConNF.CoherentAt ξ A L₁ L₂ ↔ ∃ (ρ : ConNF.AllPerm P.δ), ξ ⇘ P.A ↘ ⋯ • t.support = ρᵁ • t.support ∧ L₂ = ConNF.fuzz ⋯ (ρ • t)

theorem ConNF.smul_eq_of_coherentAt_inflexible [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {X : Type u_1} [ConNF.BaseActionClass X] {ξ : ConNF.Tree X β} {A : β ↝ ⊥} {L₁ L₂ : ConNF.Litter} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (ht : L₁ = ConNF.fuzz ⋯ t) (h : ConNF.CoherentAt ξ A L₁ L₂) (ρ : ConNF.AllPerm P.δ) : ξ ⇘ P.A ↘ ⋯ • t.support = ρᵁ • t.support → L₂ = ConNF.fuzz ⋯ (ρ • t)

theorem ConNF.coherentAt_flexible [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {X : Type u_1} [ConNF.BaseActionClass X] {ξ : ConNF.Tree X β} {A : β ↝ ⊥} {L₁ L₂ : ConNF.Litter} (hL : ¬ConNF.Inflexible A L₁) : ConNF.CoherentAt ξ A L₁ L₂ ↔ ¬ConNF.Inflexible A L₂

theorem ConNF.coherentAt_inflexible' [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {X : Type u_1} [ConNF.BaseActionClass X] {ξ : ConNF.Tree X β} {A : β ↝ ⊥} {L₁ L₂ : ConNF.Litter} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (ht : L₂ = ConNF.fuzz ⋯ t) : ConNF.CoherentAt ξ A L₁ L₂ ↔ ∃ (ρ : ConNF.AllPerm P.δ), ξ ⇘ P.A ↘ ⋯ • ρᵁ • t.support = t.support ∧ L₁ = ConNF.fuzz ⋯ (ρ • t)

theorem ConNF.smul_eq_of_coherentAt_inflexible' [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {X : Type u_1} [ConNF.BaseActionClass X] {ξ : ConNF.Tree X β} {A : β ↝ ⊥} {L₁ L₂ : ConNF.Litter} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (ht : L₂ = ConNF.fuzz ⋯ t) (h : ConNF.CoherentAt ξ A L₁ L₂) (ρ : ConNF.AllPerm P.δ) : ξ ⇘ P.A ↘ ⋯ • ρᵁ • t.support = t.support → L₁ = ConNF.fuzz ⋯ (ρ • t)

theorem ConNF.CoherentAt.deriv [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {γ : ConNF.TypeIndex} [ConNF.LeLevel γ] {X : Type u_1} [ConNF.BaseActionClass X] {ξ : ConNF.Tree X β} {L₁ L₂ : ConNF.Litter} (A : β ↝ γ) (B : γ ↝ ⊥) (h : ConNF.CoherentAt ξ (A ⇘ B) L₁ L₂) : ConNF.CoherentAt (ξ ⇘ A) B L₁ L₂