Strong supports

theorem ConNF.Support.interferes_iff [ConNF.Params] (a : ConNF.Atom) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) : ConNF.Support.Interferes a N₁ N₂ ↔ N₁.fst = N₂.fst ∧ a ∈ symmDiff ↑N₁ ↑N₂ ∨ N₁.fst ≠ N₂.fst ∧ a ∈ ↑N₁ ∩ ↑N₂

inductive ConNF.Support.Interferes [ConNF.Params] (a : ConNF.Atom) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) : Prop

• symmDiff: ∀ [inst : ConNF.Params] {a : ConNF.Atom} {N₁ N₂ : ConNF.NearLitter}, N₁.fst = N₂.fst → a ∈ symmDiff ↑N₁ ↑N₂ → ConNF.Support.Interferes a N₁ N₂
• inter: ∀ [inst : ConNF.Params] {a : ConNF.Atom} {N₁ N₂ : ConNF.NearLitter}, N₁.fst ≠ N₂.fst → a ∈ ↑N₁ ∩ ↑N₂ → ConNF.Support.Interferes a N₁ N₂

theorem ConNF.Support.precedes_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ∀ (a a_1 : ConNF.Address ↑β), ConNF.Support.Precedes a a_1 ↔ (∃ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleCoe A N.fst), ∃ c ∈ h.t.support, a = { path := (h.path.B.cons ⋯).comp c.path, value := c.value } ∧ a_1 = { path := (h.path.B.cons ⋯).cons ⋯, value := Sum.inr N }) ∨ ∃ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleBot A N.fst), a = { path := h.path.B.cons ⋯, value := Sum.inl h.a } ∧ a_1 = { path := (h.path.B.cons ⋯).cons ⋯, value := Sum.inr N }

inductive ConNF.Support.Precedes [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ConNF.Address ↑β → ConNF.Address ↑β → Prop

• fuzz: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleCoe A N.fst), ∀ c ∈ h.t.support, ConNF.Support.Precedes { path := (h.path.B.cons ⋯).comp c.path, value := c.value } { path := (h.path.B.cons ⋯).cons ⋯, value := Sum.inr N }
• fuzzBot: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleBot A N.fst), ConNF.Support.Precedes { path := h.path.B.cons ⋯, value := Sum.inl h.a } { path := (h.path.B.cons ⋯).cons ⋯, value := Sum.inr N }

theorem ConNF.Support.strong_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) : S.Strong ↔ (∀ {i₁ i₂ : ConNF.κ} (hi₁ : i₁ < S.max) (hi₂ : i₂ < S.max) {A : ConNF.ExtendedIndex ↑β} {N₁ N₂ : ConNF.NearLitter}, S.f i₁ hi₁ = { path := A, value := Sum.inr N₁ } → S.f i₂ hi₂ = { path := A, value := Sum.inr N₂ } → ∀ {a : ConNF.Atom}, ConNF.Support.Interferes a N₁ N₂ → ∃ (j : ConNF.κ) (hj : j < S.max), S.f j hj = { path := A, value := Sum.inl a }) ∧ ∀ {i : ConNF.κ} (hi : i < S.max) (c : ConNF.Address ↑β), ConNF.Support.Precedes c (S.f i hi) → ∃ (j : ConNF.κ) (hj : j < S.max), j < i ∧ S.f j hj = c

structure ConNF.Support.Strong [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) : Prop

• interferes : ∀ {i₁ i₂ : ConNF.κ} (hi₁ : i₁ < S.max) (hi₂ : i₂ < S.max) {A : ConNF.ExtendedIndex ↑β} {N₁ N₂ : ConNF.NearLitter}, S.f i₁ hi₁ = { path := A, value := Sum.inr N₁ } → S.f i₂ hi₂ = { path := A, value := Sum.inr N₂ } → ∀ {a : ConNF.Atom}, ConNF.Support.Interferes a N₁ N₂ → ∃ (j : ConNF.κ) (hj : j < S.max), S.f j hj = { path := A, value := Sum.inl a }

  TODO: We can simplify this statement now that we've removed the extra inequalities.

• precedes : ∀ {i : ConNF.κ} (hi : i < S.max) (c : ConNF.Address ↑β), ConNF.Support.Precedes c (S.f i hi) → ∃ (j : ConNF.κ) (hj : j < S.max), j < i ∧ S.f j hj = c

theorem ConNF.Support.Strong.interferes [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} (self : S.Strong) {i₁ : ConNF.κ} {i₂ : ConNF.κ} (hi₁ : i₁ < S.max) (hi₂ : i₂ < S.max) {A : ConNF.ExtendedIndex ↑β} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h₁ : S.f i₁ hi₁ = { path := A, value := Sum.inr N₁ }) (h₂ : S.f i₂ hi₂ = { path := A, value := Sum.inr N₂ }) {a : ConNF.Atom} (ha : ConNF.Support.Interferes a N₁ N₂) : ∃ (j : ConNF.κ) (hj : j < S.max), S.f j hj = { path := A, value := Sum.inl a }

TODO: We can simplify this statement now that we've removed the extra inequalities.

theorem ConNF.Support.Strong.precedes [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} (self : S.Strong) {i : ConNF.κ} (hi : i < S.max) (c : ConNF.Address ↑β) (hc : ConNF.Support.Precedes c (S.f i hi)) : ∃ (j : ConNF.κ) (hj : j < S.max), j < i ∧ S.f j hj = c

theorem ConNF.Support.interferes_small [ConNF.Params] (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) : ConNF.Small {a : ConNF.Atom | ConNF.Support.Interferes a N₁ N₂}

@[simp]

theorem ConNF.Support.not_precedes_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} : ¬ConNF.Support.Precedes c { path := A, value := Sum.inl a }

theorem ConNF.Support.Precedes.lt [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} : ConNF.Support.Precedes c d → c < d

theorem ConNF.Support.Precedes.wellFounded [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : WellFounded ConNF.Support.Precedes

def ConNF.Support.precClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) : Set (ConNF.Address ↑β)

Equations

• ConNF.Support.precClosure s = {c : ConNF.Address ↑β | ∃ d ∈ s, Relation.ReflTransGen ConNF.Support.Precedes c d}

theorem ConNF.Support.precClosure_small [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (h : ConNF.Small s) : ConNF.Small (ConNF.Support.precClosure s)

def ConNF.Support.strongClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) : Set (ConNF.Address ↑β)

Equations

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

theorem ConNF.Support.interferesSet_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) : {c : ConNF.Address ↑β | ∃ (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter), { path := A, value := Sum.inr N₁ } ∈ ConNF.Support.precClosure s ∧ { path := A, value := Sum.inr N₂ } ∈ ConNF.Support.precClosure s ∧ ConNF.Support.Interferes a N₁ N₂ ∧ c = { path := A, value := Sum.inl a }} = ⋃ (A : ConNF.ExtendedIndex ↑β), ⋃ (N₁ : ConNF.NearLitter), ⋃ (_ : { path := A, value := Sum.inr N₁ } ∈ ConNF.Support.precClosure s), ⋃ (N₂ : ConNF.NearLitter), ⋃ (_ : { path := A, value := Sum.inr N₂ } ∈ ConNF.Support.precClosure s), ⋃ (a : ConNF.Atom), ⋃ (_ : ConNF.Support.Interferes a N₁ N₂), {{ path := A, value := Sum.inl a }}

theorem ConNF.Support.strongClosure_small [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (h : ConNF.Small s) : ConNF.Small (ConNF.Support.strongClosure s)

theorem ConNF.Support.subset_strongClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) : s ⊆ ConNF.Support.strongClosure s

theorem ConNF.Support.interferes_mem_strongClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) (h : ConNF.Support.Interferes a N₁ N₂) (hN₁ : { path := A, value := Sum.inr N₁ } ∈ ConNF.Support.strongClosure s) (hN₂ : { path := A, value := Sum.inr N₂ } ∈ ConNF.Support.strongClosure s) : { path := A, value := Sum.inl a } ∈ ConNF.Support.strongClosure s

theorem ConNF.Support.precedes_mem_strongClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : ConNF.Support.Precedes c d) (hd : d ∈ ConNF.Support.strongClosure s) : c ∈ ConNF.Support.strongClosure s

inductive ConNF.Support.StrongSupportRel [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ConNF.Address ↑β → ConNF.Address ↑β → Prop

• atom: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A B : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) (N : ConNF.NearLitter), ConNF.Support.StrongSupportRel { path := A, value := Sum.inl a } { path := B, value := Sum.inr N }
• precedes: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (c d : ConNF.Address ↑β), ConNF.Support.Precedes c d → ConNF.Support.StrongSupportRel c d

theorem ConNF.Support.StrongSupportRel.wellFounded [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : WellFounded ConNF.Support.StrongSupportRel

noncomputable def ConNF.Support.StrongSupportOrder [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ConNF.Address ↑β → ConNF.Address ↑β → Prop

An arbitrary well-order on the type of β-addresses, formed in such a way that whenever c must appear before d in a support, c < d.

Equations

• ConNF.Support.StrongSupportOrder = LT.lt

noncomputable def ConNF.Support.StrongSupportOrderOn [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) : ↑s → ↑s → Prop

Equations

• ConNF.Support.StrongSupportOrderOn s c d = ConNF.Support.StrongSupportOrder ↑c ↑d

instance ConNF.Support.instIsWellOrderAddressSomeΛStrongSupportOrder [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : IsWellOrder (ConNF.Address ↑β) ConNF.Support.StrongSupportOrder

Equations

• ⋯ = ⋯

instance ConNF.Support.instIsWellOrderElemAddressSomeΛStrongSupportOrderOn [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (s : Set (ConNF.Address ↑β)) : IsWellOrder (↑s) (ConNF.Support.StrongSupportOrderOn s)

Equations

• ⋯ = ⋯

noncomputable def ConNF.Support.indexMax [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) : ConNF.κ

Equations

• ConNF.Support.indexMax hs = Ordinal.enum (fun (x x_1 : ConNF.κ) => x < x_1) (Ordinal.type (ConNF.Support.StrongSupportOrderOn s)) ⋯

theorem ConNF.Support.of_lt_indexMax [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) {i : ConNF.κ} (hi : i < ConNF.Support.indexMax hs) : Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i < Ordinal.type (ConNF.Support.StrongSupportOrderOn s)

noncomputable def ConNF.Support.indexed [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) (i : ConNF.κ) (hi : i < ConNF.Support.indexMax hs) : ConNF.Address ↑β

Equations

• ConNF.Support.indexed hs i hi = ↑(Ordinal.enum (ConNF.Support.StrongSupportOrderOn s) (Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i) ⋯)

noncomputable def ConNF.Support.strongSupport [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) : ConNF.Support ↑β

A strong support containing s.

Equations

• ConNF.Support.strongSupport hs = { max := ConNF.Support.indexMax ⋯, f := ConNF.Support.indexed ⋯ }

theorem ConNF.Support.strongSupport_f [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) {i : ConNF.κ} (hi : i < ConNF.Support.indexMax ⋯) : (ConNF.Support.strongSupport hs).f i hi = ConNF.Support.indexed ⋯ i hi

theorem ConNF.Support.strongSupport_index_lt_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) {i : ConNF.κ} {j : ConNF.κ} (hi : i < ConNF.Support.indexMax ⋯) (hj : j < ConNF.Support.indexMax ⋯) : ConNF.Support.StrongSupportOrder ((ConNF.Support.strongSupport hs).f i hi) ((ConNF.Support.strongSupport hs).f j hj) ↔ i < j

theorem ConNF.Support.lt_of_strongSupportRel [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) {i : ConNF.κ} {j : ConNF.κ} (hi : i < ConNF.Support.indexMax ⋯) (hj : j < ConNF.Support.indexMax ⋯) (h : ConNF.Support.StrongSupportRel ((ConNF.Support.strongSupport hs).f i hi) ((ConNF.Support.strongSupport hs).f j hj)) : i < j

theorem ConNF.Support.mem_of_strongSupport_f_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) {i : ConNF.κ} (hi : i < ConNF.Support.indexMax ⋯) : (ConNF.Support.strongSupport hs).f i hi ∈ ConNF.Support.strongClosure s

theorem ConNF.Support.exists_of_mem_strongClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) (c : ConNF.Address ↑β) (hc : c ∈ ConNF.Support.strongClosure s) : ∃ (j : ConNF.κ) (hj : j < ConNF.Support.indexMax ⋯), (ConNF.Support.strongSupport hs).f j hj = c

theorem ConNF.Support.subset_strongSupport [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) : s ⊆ ConNF.Enumeration.carrier (ConNF.Support.strongSupport hs)

theorem ConNF.Support.strongSupport_strong [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {s : Set (ConNF.Address ↑β)} (hs : ConNF.Small s) : (ConNF.Support.strongSupport hs).Strong

theorem ConNF.Support.Interferes.symm [ConNF.Params] {a : ConNF.Atom} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : ConNF.Support.Interferes a N₁ N₂) : ConNF.Support.Interferes a N₂ N₁

theorem ConNF.Support.Interferes.smul [ConNF.Params] {a : ConNF.Atom} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : ConNF.Support.Interferes a N₁ N₂) (π : ConNF.BasePerm) : ConNF.Support.Interferes (π • a) (π • N₁) (π • N₂)

theorem ConNF.Support.Precedes.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (h : ConNF.Support.Precedes c d) (ρ : ConNF.Allowable ↑β) : ConNF.Support.Precedes (ρ • c) (ρ • d)

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

def ConNF.Support.before [ConNF.Params] {β : ConNF.Λ} (S : ConNF.Support ↑β) (i : ConNF.κ) (hi : i < S.max) : ConNF.Support ↑β

TODO: We can probably do without this.

Equations

• S.before i hi = { max := i, f := fun (j : ConNF.κ) (hj : j < i) => S.f j ⋯ }

@[simp]

theorem ConNF.Support.before_f [ConNF.Params] {β : ConNF.Λ} (S : ConNF.Support ↑β) (i : ConNF.κ) (hi : i < S.max) (j : ConNF.κ) (hj : j < i) : (S.before i hi).f j hj = S.f j ⋯

@[simp]

theorem ConNF.Support.before_carrier [ConNF.Params] {β : ConNF.Λ} (S : ConNF.Support ↑β) (i : ConNF.κ) (hi : i < S.max) : ConNF.Enumeration.carrier (S.before i hi) = {c : ConNF.Address ↑β | ∃ (j : ConNF.κ) (hj : j < S.max), j < i ∧ S.f j hj = c}

@[simp]

theorem ConNF.Support.before_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (S : ConNF.Support ↑β) (i : ConNF.κ) (hi : i < S.max) (ρ : ConNF.Allowable ↑β) : (ρ • S).before i hi = ρ • S.before i hi

def ConNF.Support.CanComp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} (S : ConNF.Support ↑β) (A : Quiver.Path ↑β ↑γ) : Prop

Equations

• S.CanComp A = {i : ConNF.κ | ∃ (hi : i < S.max) (c : ConNF.Address ↑γ), S.f i hi = { path := A.comp c.path, value := c.value }}.Nonempty

noncomputable def ConNF.Support.leastCompIndex [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) : ConNF.κ

Equations

• ConNF.Support.leastCompIndex hS = ⋯.min {i : ConNF.κ | ∃ (hi : i < S.max) (c : ConNF.Address ↑γ), S.f i hi = { path := A.comp c.path, value := c.value }} hS

theorem ConNF.Support.leastCompIndex_mem [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) : ConNF.Support.leastCompIndex hS ∈ {i : ConNF.κ | ∃ (hi : i < S.max) (c : ConNF.Address ↑γ), S.f i hi = { path := A.comp c.path, value := c.value }}

theorem ConNF.Support.not_lt_leastCompIndex [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) (i : ConNF.κ) (hi : ∃ (hi : i < S.max) (c : ConNF.Address ↑γ), S.f i hi = { path := A.comp c.path, value := c.value }) : ¬i < ConNF.Support.leastCompIndex hS

noncomputable def ConNF.Support.compIndex [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) : ConNF.κ

Equations

• ConNF.Support.compIndex hS hi = if ∃ (d : ConNF.Address ↑γ), S.f i hi = { path := A.comp d.path, value := d.value } then i else ConNF.Support.leastCompIndex hS

theorem ConNF.Support.compIndex_lt_max [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) : ConNF.Support.compIndex hS hi < S.max

theorem ConNF.Support.compIndex_eq_comp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) : ∃ (d : ConNF.Address ↑γ), S.f (ConNF.Support.compIndex hS hi) ⋯ = { path := A.comp d.path, value := d.value }

theorem ConNF.Support.compIndex_eq_of_comp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) {c : ConNF.Address ↑γ} (hc : S.f i hi = { path := A.comp c.path, value := c.value }) : ConNF.Support.compIndex hS hi = i

theorem ConNF.Support.compIndex_eq_of_comp' [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) (hc : ¬∃ (c : ConNF.Address ↑γ), S.f i hi = { path := A.comp c.path, value := c.value }) : ConNF.Support.compIndex hS hi = ConNF.Support.leastCompIndex hS

noncomputable def ConNF.Support.decomp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) : ConNF.Address ↑γ

Equations

• ConNF.Support.decomp hS hi = ⋯.choose

theorem ConNF.Support.decomp_spec [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) : S.f (ConNF.Support.compIndex hS hi) ⋯ = { path := A.comp (ConNF.Support.decomp hS hi).path, value := (ConNF.Support.decomp hS hi).value }

noncomputable def ConNF.Support.comp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} (S : ConNF.Support ↑β) (A : Quiver.Path ↑β ↑γ) : ConNF.Support ↑γ

Equations

• S.comp A = if hS : S.CanComp A then { max := S.max, f := fun (x : ConNF.κ) (hi : x < S.max) => ConNF.Support.decomp hS hi } else { max := 0, f := fun (x : ConNF.κ) (h : x < 0) => ⋯.elim }

theorem ConNF.Support.comp_eq_of_canComp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) : S.comp A = { max := S.max, f := fun (x : ConNF.κ) (hi : x < S.max) => ConNF.Support.decomp hS hi }

theorem ConNF.Support.comp_eq_of_not_canComp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : ¬S.CanComp A) : S.comp A = { max := 0, f := fun (x : ConNF.κ) (h : x < 0) => ⋯.elim }

theorem ConNF.Support.comp_max_eq_of_canComp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) : (S.comp A).max = S.max

theorem ConNF.Support.comp_max_eq_of_not_canComp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : ¬S.CanComp A) : (S.comp A).max = 0

theorem ConNF.Support.canComp_of_lt_comp_max [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} {i : ConNF.κ} (hi : i < (S.comp A).max) : S.CanComp A

theorem ConNF.Support.lt_max_of_lt_comp_max [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} {i : ConNF.κ} (hi : i < (S.comp A).max) : i < S.max

@[simp]

theorem ConNF.Support.comp_f_eq [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} {i : ConNF.κ} (hi : i < (S.comp A).max) : (S.comp A).f i hi = ConNF.Support.decomp ⋯ ⋯

theorem ConNF.Support.comp_decomp_mem [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) : { path := A.comp (ConNF.Support.decomp hS hi).path, value := (ConNF.Support.decomp hS hi).value } ∈ S

theorem ConNF.Support.comp_decomp_eq [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) {c : ConNF.Address ↑γ} (h : S.f i hi = { path := A.comp c.path, value := c.value }) : ConNF.Support.decomp hS hi = c

noncomputable def ConNF.Support.leastComp [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) : ConNF.Address ↑γ

Equations

• ConNF.Support.leastComp hS = ⋯.choose

theorem ConNF.Support.leastComp_spec [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) : S.f (ConNF.Support.leastCompIndex hS) ⋯ = { path := A.comp (ConNF.Support.leastComp hS).path, value := (ConNF.Support.leastComp hS).value }

theorem ConNF.Support.comp_decomp_eq' [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) {i : ConNF.κ} (hi : i < S.max) (h : ¬∃ (c : ConNF.Address ↑γ), S.f i hi = { path := A.comp c.path, value := c.value }) : ConNF.Support.decomp hS hi = ConNF.Support.leastComp hS

@[simp]

theorem ConNF.Support.comp_carrier [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} (S : ConNF.Support ↑β) (A : Quiver.Path ↑β ↑γ) : ConNF.Enumeration.carrier (S.comp A) = (fun (c : ConNF.Address ↑γ) => { path := A.comp c.path, value := c.value }) ⁻¹' ConNF.Enumeration.carrier S

theorem ConNF.Support.comp_f_eq' [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} {i : ConNF.κ} {hi : i < (S.comp A).max} {c : ConNF.Address ↑γ} (hiS : (S.comp A).f i hi = c) : ∃ (j : ConNF.κ) (hj : j < S.max), S.f j hj = { path := A.comp c.path, value := c.value }

theorem ConNF.Support.Precedes.comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {c : ConNF.Address ↑γ} {d : ConNF.Address ↑γ} (h : ConNF.Support.Precedes c d) (A : Quiver.Path ↑β ↑γ) : ConNF.Support.Precedes { path := A.comp c.path, value := c.value } { path := A.comp d.path, value := d.value }

theorem ConNF.Support.comp_strong [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} (S : ConNF.Support ↑β) (A : Quiver.Path ↑β ↑γ) (hS : S.Strong) : (S.comp A).Strong

theorem ConNF.Support.CanComp.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (h : S.CanComp A) (ρ : ConNF.Allowable ↑β) : (ρ • S).CanComp A

theorem ConNF.Support.leastCompIndex_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) (ρ : ConNF.Allowable ↑β) : ConNF.Support.leastCompIndex ⋯ = ConNF.Support.leastCompIndex hS

theorem ConNF.Support.leastComp_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] {S : ConNF.Support ↑β} {A : Quiver.Path ↑β ↑γ} (hS : S.CanComp A) (ρ : ConNF.Allowable ↑β) : ConNF.Support.leastComp ⋯ = (ConNF.Allowable.comp A) ρ • ConNF.Support.leastComp hS

@[simp]

theorem ConNF.Support.comp_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (S : ConNF.Support ↑β) (A : Quiver.Path ↑β ↑γ) (ρ : ConNF.Allowable ↑β) : (ρ • S).comp A = (ConNF.Allowable.comp A) ρ • S.comp A

theorem ConNF.Support.smul_comp_ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (A : Quiver.Path ↑β ↑γ) (ρ : ConNF.Allowable ↑γ) (h₁ : S.max = T.max) (h₂ : ∀ (i : ConNF.κ) (hiS : i < S.max) (hiT : i < T.max) (c : ConNF.Address ↑γ), S.f i hiS = { path := A.comp c.path, value := c.value } → T.f i hiT = { path := A.comp c.path, value := ConNF.Allowable.toStructPerm ρ c.path • c.value }) (h₃ : ∀ (i : ConNF.κ) (hiT : i < T.max) (hiS : i < S.max) (c : ConNF.Address ↑γ), T.f i hiT = { path := A.comp c.path, value := c.value } → S.f i hiS = { path := A.comp c.path, value := ConNF.Allowable.toStructPerm ρ⁻¹ c.path • c.value }) : ρ • S.comp A = T.comp A