Supports

In this file, we define the notion of a support.

Main declarations

• ConNF.BaseSupport: The type of supports of atoms.
• ConNF.Support: The type of supports of objects of arbitrary type indices.

Base supports

structure ConNF.BaseSupport [ConNF.Params] : Type u

• atoms : ConNF.Enumeration ConNF.Atom
• nearLitters : ConNF.Enumeration ConNF.NearLitter

instance ConNF.BaseSupport.instSuperAEnumerationAtom [ConNF.Params] : ConNF.SuperA ConNF.BaseSupport (ConNF.Enumeration ConNF.Atom)

Equations

• ConNF.BaseSupport.instSuperAEnumerationAtom = { superA := ConNF.BaseSupport.atoms }

instance ConNF.BaseSupport.instSuperNEnumerationNearLitter [ConNF.Params] : ConNF.SuperN ConNF.BaseSupport (ConNF.Enumeration ConNF.NearLitter)

Equations

• ConNF.BaseSupport.instSuperNEnumerationNearLitter = { superN := ConNF.BaseSupport.nearLitters }

@[simp]

theorem ConNF.BaseSupport.mk_atoms [ConNF.Params] {a : ConNF.Enumeration ConNF.Atom} {N : ConNF.Enumeration ConNF.NearLitter} : { atoms := a, nearLitters := N }ᴬ = a

@[simp]

theorem ConNF.BaseSupport.mk_nearLitters [ConNF.Params] {a : ConNF.Enumeration ConNF.Atom} {N : ConNF.Enumeration ConNF.NearLitter} : { atoms := a, nearLitters := N }ᴺ = N

theorem ConNF.BaseSupport.atoms_congr [ConNF.Params] {S T : ConNF.BaseSupport} (h : S = T) : Sᴬ = Tᴬ

theorem ConNF.BaseSupport.nearLitters_congr [ConNF.Params] {S T : ConNF.BaseSupport} (h : S = T) : Sᴺ = Tᴺ

theorem ConNF.BaseSupport.ext [ConNF.Params] {S T : ConNF.BaseSupport} (h₁ : Sᴬ = Tᴬ) (h₂ : Sᴺ = Tᴺ) : S = T

instance ConNF.BaseSupport.instSMulBasePerm [ConNF.Params] : SMul ConNF.BasePerm ConNF.BaseSupport

Equations

• ConNF.BaseSupport.instSMulBasePerm = { smul := fun (π : ConNF.BasePerm) (S : ConNF.BaseSupport) => { atoms := π • Sᴬ, nearLitters := π • Sᴺ } }

@[simp]

theorem ConNF.BaseSupport.smul_atoms [ConNF.Params] (π : ConNF.BasePerm) (S : ConNF.BaseSupport) : (π • S)ᴬ = π • Sᴬ

@[simp]

theorem ConNF.BaseSupport.smul_nearLitters [ConNF.Params] (π : ConNF.BasePerm) (S : ConNF.BaseSupport) : (π • S)ᴺ = π • Sᴺ

@[simp]

theorem ConNF.BaseSupport.smul_atoms_eq_of_smul_eq [ConNF.Params] {π : ConNF.BasePerm} {S : ConNF.BaseSupport} (h : π • S = S) : π • Sᴬ = Sᴬ

@[simp]

theorem ConNF.BaseSupport.smul_nearLitters_eq_of_smul_eq [ConNF.Params] {π : ConNF.BasePerm} {S : ConNF.BaseSupport} (h : π • S = S) : π • Sᴺ = Sᴺ

instance ConNF.BaseSupport.instMulActionBasePerm [ConNF.Params] : MulAction ConNF.BasePerm ConNF.BaseSupport

Equations

• ConNF.BaseSupport.instMulActionBasePerm = MulAction.mk ⋯ ⋯

theorem ConNF.BaseSupport.smul_eq_smul_iff [ConNF.Params] (π₁ π₂ : ConNF.BasePerm) (S : ConNF.BaseSupport) : π₁ • S = π₂ • S ↔ (∀ a ∈ Sᴬ, π₁ • a = π₂ • a) ∧ ∀ N ∈ Sᴺ, π₁ • N = π₂ • N

theorem ConNF.BaseSupport.smul_eq_iff [ConNF.Params] (π : ConNF.BasePerm) (S : ConNF.BaseSupport) : π • S = S ↔ (∀ a ∈ Sᴬ, π • a = a) ∧ ∀ N ∈ Sᴺ, π • N = N

noncomputable instance ConNF.BaseSupport.instAdd [ConNF.Params] : Add ConNF.BaseSupport

Equations

• ConNF.BaseSupport.instAdd = { add := fun (S T : ConNF.BaseSupport) => { atoms := Sᴬ + Tᴬ, nearLitters := Sᴺ + Tᴺ } }

@[simp]

theorem ConNF.BaseSupport.add_atoms [ConNF.Params] (S T : ConNF.BaseSupport) : (S + T)ᴬ = Sᴬ + Tᴬ

@[simp]

theorem ConNF.BaseSupport.add_nearLitters [ConNF.Params] (S T : ConNF.BaseSupport) : (S + T)ᴺ = Sᴺ + Tᴺ

def ConNF.baseSupportEquiv [ConNF.Params] : ConNF.BaseSupport ≃ ConNF.Enumeration ConNF.Atom × ConNF.Enumeration ConNF.NearLitter

Equations

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

theorem ConNF.card_baseSupport [ConNF.Params] : Cardinal.mk ConNF.BaseSupport = Cardinal.mk ConNF.μ

Structural supports

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

• atoms : ConNF.Enumeration (α ↝ ⊥ × ConNF.Atom)
• nearLitters : ConNF.Enumeration (α ↝ ⊥ × ConNF.NearLitter)

instance ConNF.Support.instSuperAEnumerationProdPathBotTypeIndexAtom [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.SuperA (ConNF.Support α) (ConNF.Enumeration (α ↝ ⊥ × ConNF.Atom))

Equations

• ConNF.Support.instSuperAEnumerationProdPathBotTypeIndexAtom = { superA := ConNF.Support.atoms }

instance ConNF.Support.instSuperNEnumerationProdPathBotTypeIndexNearLitter [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.SuperN (ConNF.Support α) (ConNF.Enumeration (α ↝ ⊥ × ConNF.NearLitter))

Equations

• ConNF.Support.instSuperNEnumerationProdPathBotTypeIndexNearLitter = { superN := ConNF.Support.nearLitters }

@[simp]

theorem ConNF.Support.mk_atoms [ConNF.Params] {α : ConNF.TypeIndex} (E : ConNF.Enumeration (α ↝ ⊥ × ConNF.Atom)) (F : ConNF.Enumeration (α ↝ ⊥ × ConNF.NearLitter)) : { atoms := E, nearLitters := F }ᴬ = E

@[simp]

theorem ConNF.Support.mk_nearLitters [ConNF.Params] {α : ConNF.TypeIndex} (E : ConNF.Enumeration (α ↝ ⊥ × ConNF.Atom)) (F : ConNF.Enumeration (α ↝ ⊥ × ConNF.NearLitter)) : { atoms := E, nearLitters := F }ᴺ = F

instance ConNF.Support.instDerivative [ConNF.Params] {α β : ConNF.TypeIndex} : ConNF.Derivative (ConNF.Support α) (ConNF.Support β) α β

Equations

• ConNF.Support.instDerivative = ConNF.Derivative.mk (fun (S : ConNF.Support α) (A : α ↝ β) => { atoms := Sᴬ ⇘ A, nearLitters := Sᴺ ⇘ A }) ⋯

instance ConNF.Support.instCoderivative [ConNF.Params] {α β : ConNF.TypeIndex} : ConNF.Coderivative (ConNF.Support β) (ConNF.Support α) α β

Equations

• ConNF.Support.instCoderivative = ConNF.Coderivative.mk (fun (S : ConNF.Support β) (A : α ↝ β) => { atoms := Sᴬ ⇗ A, nearLitters := Sᴺ ⇗ A }) ⋯

instance ConNF.Support.instBotDerivativeBaseSupport [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.BotDerivative (ConNF.Support α) ConNF.BaseSupport α

Equations

• ConNF.Support.instBotDerivativeBaseSupport = ConNF.BotDerivative.mk (fun (S : ConNF.Support α) (A : α ↝ ⊥) => { atoms := Sᴬ ⇘. A, nearLitters := Sᴺ ⇘. A }) ⋯

@[simp]

theorem ConNF.Support.deriv_atoms [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support α) (A : α ↝ β) : Sᴬ ⇘ A = (S ⇘ A)ᴬ

@[simp]

theorem ConNF.Support.deriv_nearLitters [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support α) (A : α ↝ β) : Sᴺ ⇘ A = (S ⇘ A)ᴺ

@[simp]

theorem ConNF.Support.sderiv_atoms [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support α) (h : β < α) : Sᴬ ↘ h = (S ↘ h)ᴬ

@[simp]

theorem ConNF.Support.sderiv_nearLitters [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support α) (h : β < α) : Sᴺ ↘ h = (S ↘ h)ᴺ

@[simp]

theorem ConNF.Support.coderiv_atoms [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support β) (A : α ↝ β) : Sᴬ ⇗ A = (S ⇗ A)ᴬ

@[simp]

theorem ConNF.Support.coderiv_nearLitters [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support β) (A : α ↝ β) : Sᴺ ⇗ A = (S ⇗ A)ᴺ

@[simp]

theorem ConNF.Support.scoderiv_atoms [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support β) (h : β < α) : Sᴬ ↗ h = (S ↗ h)ᴬ

@[simp]

theorem ConNF.Support.scoderiv_nearLitters [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support β) (h : β < α) : Sᴺ ↗ h = (S ↗ h)ᴺ

@[simp]

theorem ConNF.Support.derivBot_atoms [ConNF.Params] {α : ConNF.TypeIndex} (S : ConNF.Support α) (A : α ↝ ⊥) : Sᴬ ⇘. A = (S ⇘. A)ᴬ

@[simp]

theorem ConNF.Support.derivBot_nearLitters [ConNF.Params] {α : ConNF.TypeIndex} (S : ConNF.Support α) (A : α ↝ ⊥) : Sᴺ ⇘. A = (S ⇘. A)ᴺ

theorem ConNF.Support.ext' [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} (h₁ : Sᴬ = Tᴬ) (h₂ : Sᴺ = Tᴺ) : S = T

theorem ConNF.Support.ext [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} (h : ∀ (A : α ↝ ⊥), S ⇘. A = T ⇘. A) : S = T

@[simp]

theorem ConNF.Support.deriv_derivBot [ConNF.Params] {β α : ConNF.TypeIndex} (S : ConNF.Support α) (A : α ↝ β) (B : β ↝ ⊥) : S ⇘ A ⇘. B = S ⇘. (A ⇘ B)

@[simp]

theorem ConNF.Support.coderiv_deriv_eq [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support β) (A : α ↝ β) : S ⇗ A ⇘ A = S

theorem ConNF.Support.eq_of_atom_mem_scoderiv_botDeriv [ConNF.Params] {α β : ConNF.TypeIndex} {S : ConNF.Support β} {A : α ↝ ⊥} {h : β < α} {a : ConNF.Atom} (ha : a ∈ (S ↗ h ⇘. A)ᴬ) : ∃ (B : β ↝ ⊥), A = B ↗ h

theorem ConNF.Support.eq_of_nearLitter_mem_scoderiv_botDeriv [ConNF.Params] {α β : ConNF.TypeIndex} {S : ConNF.Support β} {A : α ↝ ⊥} {h : β < α} {N : ConNF.NearLitter} (hN : N ∈ (S ↗ h ⇘. A)ᴺ) : ∃ (B : β ↝ ⊥), A = B ↗ h

@[simp]

theorem ConNF.Support.scoderiv_botDeriv_eq [ConNF.Params] {α β : ConNF.TypeIndex} (S : ConNF.Support β) (A : β ↝ ⊥) (h : β < α) : S ↗ h ⇘. (A ↗ h) = S ⇘. A

@[simp]

theorem ConNF.Support.scoderiv_deriv_eq [ConNF.Params] {α β γ : ConNF.TypeIndex} (S : ConNF.Support β) (A : β ↝ γ) (h : β < α) : S ↗ h ⇘ (A ↗ h) = S ⇘ A

@[simp]

theorem ConNF.Support.coderiv_inj [ConNF.Params] {α β : ConNF.TypeIndex} (S T : ConNF.Support β) (A : α ↝ β) : S ⇗ A = T ⇗ A ↔ S = T

@[simp]

theorem ConNF.Support.scoderiv_inj [ConNF.Params] {α β : ConNF.TypeIndex} (S T : ConNF.Support β) (h : β < α) : S ↗ h = T ↗ h ↔ S = T

instance ConNF.Support.instSMulStrPerm [ConNF.Params] {α : ConNF.TypeIndex} : SMul (ConNF.StrPerm α) (ConNF.Support α)

Equations

• ConNF.Support.instSMulStrPerm = { smul := fun (π : ConNF.StrPerm α) (S : ConNF.Support α) => { atoms := π • Sᴬ, nearLitters := π • Sᴺ } }

@[simp]

theorem ConNF.Support.smul_atoms [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StrPerm α) (S : ConNF.Support α) : (π • S)ᴬ = π • Sᴬ

@[simp]

theorem ConNF.Support.smul_nearLitters [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StrPerm α) (S : ConNF.Support α) : (π • S)ᴺ = π • Sᴺ

theorem ConNF.Support.smul_atoms_eq_of_smul_eq [ConNF.Params] {α : ConNF.TypeIndex} {π : ConNF.StrPerm α} {S : ConNF.Support α} (h : π • S = S) : π • Sᴬ = Sᴬ

theorem ConNF.Support.smul_nearLitters_eq_of_smul_eq [ConNF.Params] {α : ConNF.TypeIndex} {π : ConNF.StrPerm α} {S : ConNF.Support α} (h : π • S = S) : π • Sᴺ = Sᴺ

instance ConNF.Support.instMulActionStrPerm [ConNF.Params] {α : ConNF.TypeIndex} : MulAction (ConNF.StrPerm α) (ConNF.Support α)

Equations

• ConNF.Support.instMulActionStrPerm = MulAction.mk ⋯ ⋯

@[simp]

theorem ConNF.Support.smul_derivBot [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StrPerm α) (S : ConNF.Support α) (A : α ↝ ⊥) : (π • S) ⇘. A = π A • S ⇘. A

theorem ConNF.Support.smul_coderiv [ConNF.Params] {β α : ConNF.TypeIndex} (π : ConNF.StrPerm α) (S : ConNF.Support β) (A : α ↝ β) : π • S ⇗ A = (π ⇘ A • S) ⇗ A

theorem ConNF.Support.smul_scoderiv [ConNF.Params] {β α : ConNF.TypeIndex} (π : ConNF.StrPerm α) (S : ConNF.Support β) (h : β < α) : π • S ↗ h = (π ↘ h • S) ↗ h

theorem ConNF.Support.smul_eq_smul_iff [ConNF.Params] {β : ConNF.TypeIndex} (π₁ π₂ : ConNF.StrPerm β) (S : ConNF.Support β) : π₁ • S = π₂ • S ↔ ∀ (A : β ↝ ⊥), (∀ a ∈ (S ⇘. A)ᴬ, π₁ A • a = π₂ A • a) ∧ ∀ N ∈ (S ⇘. A)ᴺ, π₁ A • N = π₂ A • N

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

noncomputable instance ConNF.Support.instAdd [ConNF.Params] {α : ConNF.TypeIndex} : Add (ConNF.Support α)

Equations

• ConNF.Support.instAdd = { add := fun (S T : ConNF.Support α) => { atoms := Sᴬ + Tᴬ, nearLitters := Sᴺ + Tᴺ } }

@[simp]

theorem ConNF.Support.add_derivBot [ConNF.Params] {α : ConNF.TypeIndex} (S T : ConNF.Support α) (A : α ↝ ⊥) : (S + T) ⇘. A = S ⇘. A + T ⇘. A

theorem ConNF.Support.smul_add [ConNF.Params] {α : ConNF.TypeIndex} (S T : ConNF.Support α) (π : ConNF.StrPerm α) : π • (S + T) = π • S + π • T

theorem ConNF.Support.add_inj_of_bound_eq_bound [ConNF.Params] {α : ConNF.TypeIndex} {S T U V : ConNF.Support α} (ha : Sᴬ.bound = Tᴬ.bound) (hN : Sᴺ.bound = Tᴺ.bound) (h' : S + U = T + V) : S = T ∧ U = V

def ConNF.supportEquiv [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.Support α ≃ ConNF.Enumeration (α ↝ ⊥ × ConNF.Atom) × ConNF.Enumeration (α ↝ ⊥ × ConNF.NearLitter)

Equations

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

theorem ConNF.card_support [ConNF.Params] {α : ConNF.TypeIndex} : Cardinal.mk (ConNF.Support α) = Cardinal.mk ConNF.μ

Orders on supports

instance ConNF.instLEBaseSupport [ConNF.Params] : LE ConNF.BaseSupport

Equations

• ConNF.instLEBaseSupport = { le := fun (S T : ConNF.BaseSupport) => (∀ a ∈ Sᴬ, a ∈ Tᴬ) ∧ ∀ N ∈ Sᴺ, N ∈ Tᴺ }

instance ConNF.instPreorderBaseSupport [ConNF.Params] : Preorder ConNF.BaseSupport

Equations

• ConNF.instPreorderBaseSupport = Preorder.mk ⋯ ⋯ ⋯

theorem ConNF.BaseSupport.smul_le_smul [ConNF.Params] {S T : ConNF.BaseSupport} (h : S ≤ T) (π : ConNF.BasePerm) : π • S ≤ π • T

theorem ConNF.BaseSupport.le_add_right [ConNF.Params] {S T : ConNF.BaseSupport} : S ≤ S + T

theorem ConNF.BaseSupport.le_add_left [ConNF.Params] {S T : ConNF.BaseSupport} : S ≤ T + S

def ConNF.BaseSupport.Subsupport [ConNF.Params] (S T : ConNF.BaseSupport) : Prop

Equations

• S.Subsupport T = (Sᴬ.rel ≤ Tᴬ.rel ∧ Sᴺ.rel ≤ Tᴺ.rel)

theorem ConNF.BaseSupport.Subsupport.le [ConNF.Params] {S T : ConNF.BaseSupport} (h : S.Subsupport T) : S ≤ T

theorem ConNF.BaseSupport.Subsupport.trans [ConNF.Params] {S T U : ConNF.BaseSupport} (h₁ : S.Subsupport T) (h₂ : T.Subsupport U) : S.Subsupport U

theorem ConNF.BaseSupport.smul_subsupport_smul [ConNF.Params] {S T : ConNF.BaseSupport} (h : S.Subsupport T) (π : ConNF.BasePerm) : (π • S).Subsupport (π • T)

instance ConNF.instLESupport [ConNF.Params] {α : ConNF.TypeIndex} : LE (ConNF.Support α)

Equations

• ConNF.instLESupport = { le := fun (S T : ConNF.Support α) => ∀ (A : α ↝ ⊥), S ⇘. A ≤ T ⇘. A }

instance ConNF.instPreorderSupport [ConNF.Params] {α : ConNF.TypeIndex} : Preorder (ConNF.Support α)

Equations

• ConNF.instPreorderSupport = Preorder.mk ⋯ ⋯ ⋯

theorem ConNF.Support.smul_le_smul [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} (h : S ≤ T) (π : ConNF.StrPerm α) : π • S ≤ π • T

theorem ConNF.Support.le_add_right [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} : S ≤ S + T

theorem ConNF.Support.le_add_left [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} : S ≤ T + S

def ConNF.Support.Subsupport [ConNF.Params] {α : ConNF.TypeIndex} (S T : ConNF.Support α) : Prop

Equations

• S.Subsupport T = ∀ (A : α ↝ ⊥), (S ⇘. A).Subsupport (T ⇘. A)

theorem ConNF.Support.Subsupport.le [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} (h : S.Subsupport T) : S ≤ T

theorem ConNF.Support.Subsupport.trans [ConNF.Params] {α : ConNF.TypeIndex} {S T U : ConNF.Support α} (h₁ : S.Subsupport T) (h₂ : T.Subsupport U) : S.Subsupport U

theorem ConNF.Support.smul_subsupport_smul [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} (h : S.Subsupport T) (π : ConNF.StrPerm α) : (π • S).Subsupport (π • T)

theorem ConNF.subsupport_add [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} : S.Subsupport (S + T)

theorem ConNF.smul_eq_of_subsupport [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} {π : ConNF.StrPerm α} (h₁ : S.Subsupport T) (h₂ : S.Subsupport (π • T)) : π • S = S

theorem ConNF.smul_eq_smul_of_le [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} {π₁ π₂ : ConNF.StrPerm α} (h : S ≤ T) (h₂ : π₁ • T = π₂ • T) : π₁ • S = π₂ • S

theorem ConNF.smul_eq_of_le [ConNF.Params] {α : ConNF.TypeIndex} {S T : ConNF.Support α} {π : ConNF.StrPerm α} (h : S ≤ T) (h₂ : π • T = T) : π • S = S