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 [Params] : Type u

• atoms : Enumeration Atom
• nearLitters : Enumeration NearLitter

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

theorem ConNF.BaseSupport.ext_iff [Params] {S T : BaseSupport} : S = T ↔ Sᴬ = Tᴬ ∧ Sᴺ = Tᴺ

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ConNF.BaseSupport.instMulActionBasePerm = { toSMul := ConNF.BaseSupport.instSMulBasePerm, one_smul := ⋯, mul_smul := ⋯ }

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Structural supports

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• ConNF.Support.instMulActionStrPerm = { toSMul := ConNF.Support.instSMulStrPerm, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

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

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

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

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

Orders on supports

instance ConNF.instLEBaseSupport [Params] : LE BaseSupport

Equations

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

instance ConNF.instPreorderBaseSupport [Params] : Preorder BaseSupport

Equations

• ConNF.instPreorderBaseSupport = { toLE := ConNF.instLEBaseSupport, lt := fun (a b : ConNF.BaseSupport) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

Equations

• ConNF.instPreorderSupport = { toLE := ConNF.instLESupport, lt := fun (a b : ConNF.Support α) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

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

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

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

Equations

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

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

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

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

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

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

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

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