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 [ConNF.Params] (α : ConNF.TypeIndex) : Type (u + 1)

The same as ModelData but without the propositions.

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

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

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

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

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

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

instance ConNF.instSMulAllPermTangle [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] : SMul (ConNF.AllPerm α) (ConNF.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 [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (ρ : ConNF.AllPerm α) (t : ConNF.Tangle α) : (ρ • t).set = ρ • t.set

@[simp]

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

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

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

Equations

• ConNF.instMulActionAllPermTangle = MulAction.mk ⋯ ⋯

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

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

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

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

Criteria for supports

theorem ConNF.Support.supports_coe [ConNF.Params] {α : ConNF.Λ} {X : Type u_1} [ConNF.PreModelData ↑α] [MulAction (ConNF.AllPerm ↑α) X] (S : ConNF.Support ↑α) (x : X) (h : ∀ (ρ : ConNF.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 [ConNF.Params] {X : Type u_1} [ConNF.PreModelData ⊥] [MulAction (ConNF.AllPerm ⊥) X] (E : ConNF.Enumeration (⊥ ↝ ⊥ × ConNF.Atom)) (x : X) (h : ∀ (ρ : ConNF.AllPerm ⊥), (∀ (A : ⊥ ↝ ⊥) (x : ConNF.Atom), (A, x) ∈ E → ρᵁ A • x = x) → ρ • x = x) : { atoms := E, nearLitters := ConNF.Enumeration.empty }.Supports x

Model data at level ⊥

def ConNF.botPreModelData [ConNF.Params] : ConNF.PreModelData ⊥

Equations

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

def ConNF.botModelData [ConNF.Params] : ConNF.ModelData ⊥

Equations

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