structure ConNF.SupportHom [ConNF.Params] {β : ConNF.Λ} (S : ConNF.Support ↑β) (T : ConNF.Support ↑β) : Type u

A morphism of supports S → T.

• f : ConNF.κ → ConNF.κ
• hf : ∀ i < S.max, self.f i < T.max
• f_eq : ∀ (i : ConNF.κ) (hi : i < S.max), S.f i hi = T.f (self.f i) ⋯

theorem ConNF.SupportHom.hf [ConNF.Params] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (self : ConNF.SupportHom S T) (i : ConNF.κ) (hi : i < S.max) : self.f i < T.max

theorem ConNF.SupportHom.f_eq [ConNF.Params] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (self : ConNF.SupportHom S T) (i : ConNF.κ) (hi : i < S.max) : S.f i hi = T.f (self.f i) ⋯

theorem ConNF.Support.exists_hom_strongSupport [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) : Nonempty (ConNF.SupportHom S (ConNF.Support.strongSupport ⋯))

theorem ConNF.SupportHom.ext [ConNF.Params] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {F : ConNF.SupportHom S T} {G : ConNF.SupportHom S T} (h : F.f = G.f) : F = G

def ConNF.SupportHom.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (F : ConNF.SupportHom S T) (ρ : ConNF.Allowable ↑β) : ConNF.SupportHom (ρ • S) (ρ • T)

Equations

• F.smul ρ = { f := F.f, hf := ⋯, f_eq := ⋯ }

@[simp]

theorem ConNF.SupportHom.smul_f [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (F : ConNF.SupportHom S T) (ρ : ConNF.Allowable ↑β) : (F.smul ρ).f = F.f

theorem ConNF.SupportHom.smul_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S₁ : ConNF.Support ↑β} {S₂ : ConNF.Support ↑β} {T₁ : ConNF.Support ↑β} {T₂ : ConNF.Support ↑β} {ρ : ConNF.Allowable ↑β} {F₁ : ConNF.SupportHom S₁ T₁} {F₂ : ConNF.SupportHom S₂ T₂} (hF : F₁.f = F₂.f) (h : ρ • T₁ = T₂) (h' : S₁.max = S₂.max) : ρ • S₁ = S₂

structure ConNF.WeakSpec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) : Type u

A specification for a not-necessarily-strong support.

• max : ConNF.κ
• f : ConNF.κ → ConNF.κ
• σ : ConNF.Spec β

def ConNF.WeakSpec.Specifies [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (W : ConNF.WeakSpec β) (S : ConNF.Support ↑β) : Prop

Equations

• W.Specifies S = ∃ (T : ConNF.Support ↑β) (hT : T.Strong) (F : ConNF.SupportHom S T), W.max = S.max ∧ W.f = F.f ∧ W.σ.Specifies T hT

theorem ConNF.Support.hasWeakSpec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) : ∃ (W : ConNF.WeakSpec β), W.Specifies S

theorem ConNF.WeakSpec.Specifies.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {W : ConNF.WeakSpec β} {S : ConNF.Support ↑β} (h : W.Specifies S) (ρ : ConNF.Allowable ↑β) : W.Specifies (ρ • S)

theorem ConNF.SupportOrbit.hasWeakSpec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.SupportOrbit β) : ∃ (W : ConNF.WeakSpec β), ∀ S ∈ o, W.Specifies S

noncomputable def ConNF.SupportOrbit.weakSpec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.SupportOrbit β) : ConNF.WeakSpec β

Equations

• o.weakSpec = ⋯.choose

theorem ConNF.SupportOrbit.weakSpec_specifies [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.SupportOrbit β) (S : ConNF.Support ↑β) (hS : S ∈ o) : o.weakSpec.Specifies S

theorem ConNF.SupportOrbit.spec_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o₁ : ConNF.SupportOrbit β) (o₂ : ConNF.SupportOrbit β) (h : o₁.weakSpec = o₂.weakSpec) : o₁ = o₂

theorem ConNF.mk_supportOrbit_le_mk_weakSpec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] : Cardinal.mk (ConNF.SupportOrbit β) ≤ Cardinal.mk (ConNF.WeakSpec β)

def ConNF.WeakSpec.decompose [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (W : ConNF.WeakSpec β) : ConNF.κ × (ConNF.κ → ConNF.κ) × ConNF.Spec β

Equations

• W.decompose = (W.max, W.f, W.σ)

theorem ConNF.WeakSpec.decompose_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : Function.Injective ConNF.WeakSpec.decompose

theorem ConNF.mk_supportOrbit_le [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] : Cardinal.mk (ConNF.SupportOrbit β) ≤ 2 ^ Cardinal.mk ConNF.κ * Cardinal.mk (ConNF.Spec β)