Model data

In this file, we define what model data at a type index means.

Main declarations

• ConNF.ModelData: The type of model data at a given type index.

class ConNF.PreModelData [Params] (α : TypeIndex) : Type (u + 1)

The same as ModelData but without the propositions.

• TSet : Type u
• AllPerm : Type u
• allPermGroup : Group (AllPerm α)
• allAction : MulAction (AllPerm α) (TSet α)
• tSetForget : TSet α → StrSet α
• allPermForget : AllPerm α → StrPerm α

instance ConNF.instSuperUTSetStrSet [Params] {α : TypeIndex} [PreModelData α] : SuperU (TSet α) (StrSet α)

Equations

• ConNF.instSuperUTSetStrSet = { superU := ConNF.PreModelData.tSetForget }

instance ConNF.instSuperUAllPermStrPerm [Params] {α : TypeIndex} [PreModelData α] : SuperU (AllPerm α) (StrPerm α)

Equations

• ConNF.instSuperUAllPermStrPerm = { superU := ConNF.PreModelData.allPermForget }

structure ConNF.Support.Supports [Params] {X : Type u_1} {α : TypeIndex} [PreModelData α] [MulAction (AllPerm α) X] (S : Support α) (x : X) : Prop

• supports (ρ : AllPerm α) : ρᵁ • S = S → ρ • x = x
• nearLitters_eq_empty_of_bot : α = ⊥ → Sᴺ = Enumeration.empty

theorem ConNF.Support.Supports.mono [Params] {X : Type u_1} {α : TypeIndex} [PreModelData α] [MulAction (AllPerm α) X] {S T : Support α} {x : X} (hS : S.Supports x) (h : S ≤ T) (hT : α = ⊥ → Tᴺ = Enumeration.empty) : T.Supports x

class ConNF.ModelData [Params] (α : TypeIndex) extends ConNF.PreModelData α : Type (u + 1)

• TSet : Type u
• AllPerm : Type u
• allPermGroup : Group (AllPerm α)
• allAction : MulAction (AllPerm α) (TSet α)
• tSetForget : TSet α → StrSet α
• allPermForget : AllPerm α → StrPerm α
• tSetForget_injective' : Function.Injective PreModelData.tSetForget
• tSetForget_surjective_of_bot' : α = ⊥ → Function.Surjective PreModelData.tSetForget
• allPermForget_injective' : Function.Injective PreModelData.allPermForget
• allPermForget_one : 1ᵁ = 1
• allPermForget_mul (ρ₁ ρ₂ : AllPerm α) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ
• smul_forget (ρ : AllPerm α) (x : TSet α) : (ρ • x)ᵁ = ρᵁ • xᵁ
• exists_support (x : TSet α) : ∃ (S : Support α), S.Supports x

theorem ConNF.tSetForget_injective [Params] {α : TypeIndex} [ModelData α] {x₁ x₂ : TSet α} (h : x₁ᵁ = x₂ᵁ) : x₁ = x₂

theorem ConNF.tSetForget_surjective [Params] [ModelData ⊥] (x : StrSet ⊥) : ∃ (y : TSet ⊥), yᵁ = x

theorem ConNF.allPermForget_injective [Params] {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} (h : ρ₁ᵁ = ρ₂ᵁ) : ρ₁ = ρ₂

@[simp]

theorem ConNF.allPermForget_inv [Params] {α : TypeIndex} [ModelData α] (ρ : AllPerm α) : ρ⁻¹ᵁ = ρᵁ⁻¹

@[simp]

theorem ConNF.allPermForget_npow [Params] {α : TypeIndex} [ModelData α] (ρ : AllPerm α) (n : ℕ) : (ρ ^ n)ᵁ = ρᵁ ^ n

@[simp]

theorem ConNF.allPermForget_zpow [Params] {α : TypeIndex} [ModelData α] (ρ : AllPerm α) (n : ℤ) : (ρ ^ n)ᵁ = ρᵁ ^ n

theorem ConNF.Support.Supports.smul_eq_smul [Params] {X : Type u_1} {α : TypeIndex} [ModelData α] [MulAction (AllPerm α) X] {S : Support α} {x : X} (h : S.Supports x) {ρ₁ ρ₂ : AllPerm α} (hρ : ρ₁ᵁ • S = ρ₂ᵁ • S) : ρ₁ • x = ρ₂ • x

theorem ConNF.Support.Supports.smul_eq_of_smul_eq [Params] {X : Type u_1} {α : TypeIndex} [ModelData α] [MulAction (AllPerm α) X] {S : Support α} {x : X} (h : S.Supports x) {ρ : AllPerm α} (hρ : ρᵁ • S = S) : ρ • x = x

theorem ConNF.Support.Supports.smul [Params] {X : Type u_1} {α : TypeIndex} [ModelData α] [MulAction (AllPerm α) X] {S : Support α} {x : X} (h : S.Supports x) (ρ : AllPerm α) : (ρᵁ • S).Supports (ρ • x)

instance ConNF.instTypedMemTSet [Params] {β α : TypeIndex} [ModelData β] [ModelData α] : TypedMem (TSet β) (TSet α) β α

Equations

• ConNF.instTypedMemTSet = { typedMem := fun (h : β < α) (y : ConNF.TSet β) (x : ConNF.TSet α) => yᵁ ∈[h] xᵁ }

theorem ConNF.TSet.forget_mem_forget [Params] {β α : TypeIndex} [ModelData β] [ModelData α] (h : β < α) {x : TSet β} {y : TSet α} : xᵁ ∈[h] yᵁ ↔ x ∈[h] y

structure ConNF.Tangle [Params] (α : TypeIndex) [ModelData α] : Type u

• set : TSet α
• support : Support α
• support_supports : self.support.Supports self.set

theorem ConNF.Tangle.ext {inst✝ : Params} {α : TypeIndex} {inst✝¹ : ModelData α} {x y : Tangle α} (set : x.set = y.set) (support : x.support = y.support) : x = y

instance ConNF.instSMulAllPermTangle [Params] {α : TypeIndex} [ModelData α] : SMul (AllPerm α) (Tangle α)

Equations

• ConNF.instSMulAllPermTangle = { smul := fun (ρ : ConNF.AllPerm α) (t : ConNF.Tangle α) => { set := ρ • t.set, support := ρᵁ • t.support, support_supports := ⋯ } }

@[simp]

theorem ConNF.Tangle.smul_set [Params] {α : TypeIndex} [ModelData α] (ρ : AllPerm α) (t : Tangle α) : (ρ • t).set = ρ • t.set

@[simp]

theorem ConNF.Tangle.smul_support [Params] {α : TypeIndex} [ModelData α] (ρ : AllPerm α) (t : Tangle α) : (ρ • t).support = ρᵁ • t.support

theorem ConNF.Tangle.smul_eq_smul [Params] {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ᵁ • t.support = ρ₂ᵁ • t.support) : ρ₁ • t = ρ₂ • t

instance ConNF.instMulActionAllPermTangle [Params] {α : TypeIndex} [ModelData α] : MulAction (AllPerm α) (Tangle α)

Equations

• ConNF.instMulActionAllPermTangle = MulAction.mk ⋯ ⋯

theorem ConNF.Tangle.smul_eq [Params] {α : TypeIndex} [ModelData α] {ρ : AllPerm α} {t : Tangle α} (h : ρᵁ • t.support = t.support) : ρ • t = t

theorem ConNF.Tangle.smul_atom_eq_of_mem_support [Params] {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ • t = ρ₂ • t) {a : Atom} {A : α ↝ ⊥} (ha : a ∈ (t.support ⇘. A)ᴬ) : ρ₁ᵁ A • a = ρ₂ᵁ A • a

theorem ConNF.Tangle.smul_nearLitter_eq_of_mem_support [Params] {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ • t = ρ₂ • t) {N : NearLitter} {A : α ↝ ⊥} (hN : N ∈ (t.support ⇘. A)ᴺ) : ρ₁ᵁ A • N = ρ₂ᵁ A • N

theorem ConNF.card_tangle_le_of_card_tSet [Params] {α : TypeIndex} [ModelData α] (h : Cardinal.mk (TSet α) ≤ Cardinal.mk μ) : Cardinal.mk (Tangle α) ≤ Cardinal.mk μ

Criteria for supports

theorem ConNF.Support.supports_coe [Params] {α : Λ} {X : Type u_1} [PreModelData ↑α] [MulAction (AllPerm ↑α) X] (S : Support ↑α) (x : X) (h : ∀ (ρ : AllPerm ↑α), (∀ (A : ↑α ↝ ⊥), ∀ a ∈ (S ⇘. A)ᴬ, ρᵁ A • a = a) → (∀ (A : ↑α ↝ ⊥), ∀ N ∈ (S ⇘. A)ᴺ, ρᵁ A • N = N) → ρ • x = x) : S.Supports x

theorem ConNF.Support.supports_bot [Params] {X : Type u_1} [PreModelData ⊥] [MulAction (AllPerm ⊥) X] (E : Enumeration (⊥ ↝ ⊥ × Atom)) (x : X) (h : ∀ (ρ : AllPerm ⊥), (∀ (A : ⊥ ↝ ⊥) (x : Atom), (A, x) ∈ E → ρᵁ A • x = x) → ρ • x = x) : { atoms := E, nearLitters := Enumeration.empty }.Supports x

Model data at level ⊥

def ConNF.botPreModelData [Params] : PreModelData ⊥

Equations

• ConNF.botPreModelData = ConNF.PreModelData.mk ConNF.Atom ConNF.BasePerm ⇑ConNF.StrSet.botEquiv.symm fun (ρ : ConNF.BasePerm) (x : ⊥ ↝ ⊥) => ρ

def ConNF.botModelData [Params] : ModelData ⊥

Equations

• ConNF.botModelData = ConNF.ModelData.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯