New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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