Coordinate subcomodules

A subset of a finite basis spans a subcomodule exactly when the corresponding columns of the coefficient matrix have no entries outside that subset. This is a scheme-level criterion: it uses the universal coaction and requires no separation hypothesis on algebra-valued points.

Main declarations

• Module.Basis.coordinateSpanIsStable: the coefficient-vanishing condition for a basis subset.
• Module.Basis.coordinateSpanSubcomodule: the coordinate span as a subcomodule.
• Module.Basis.exists_subcomodule_toSubmodule_eq_span_iff_coordinateSpanIsStable: the coefficient criterion is also necessary.
• Module.Basis.weightCoordinateSpanIsStable_iff_blockTriangular: every upper weight filtration step is stable exactly when the coefficient matrix is block triangular by weight.

def Module.Basis.coordinateSpanIsStable {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (b : Basis ι R M) (s : Set ι) : Prop

The coefficient-matrix condition saying that the span of the basis vectors indexed by s is stable under the coaction. A column indexed by j ∈ s has no entry in a row outside s.

Equations

• b.coordinateSpanIsStable s = ∀ i ∉ s, ∀ j ∈ s, TauCeti.Comodule.coefficientMatrix b i j = 0

@[simp]

theorem Module.Basis.coordinateSpanIsStable_iff {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (b : Basis ι R M) (s : Set ι) : b.coordinateSpanIsStable s ↔ ∀ i ∉ s, ∀ j ∈ s, TauCeti.Comodule.coefficientMatrix b i j = 0

The coordinate-span stability predicate is exactly coefficient vanishing from selected columns to rows outside the selected subset.

def Module.Basis.coordinateSpanSubcomodule {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (b : Basis ι R M) (s : Set ι) [Finite ι] (h : b.coordinateSpanIsStable s) : TauCeti.Subcomodule R C M

A basis subset whose coefficient columns have no entries outside the subset spans a subcomodule.

Equations

• b.coordinateSpanSubcomodule s h = TauCeti.Subcomodule.ofSubmodule (Submodule.span R (⇑b '' s)) ⋯

@[simp]

theorem Module.Basis.coordinateSpanSubcomodule_toSubmodule {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (b : Basis ι R M) (s : Set ι) [Finite ι] (h : b.coordinateSpanIsStable s) : (b.coordinateSpanSubcomodule s h).toSubmodule = Submodule.span R (⇑b '' s)

The underlying submodule of a coordinate-span subcomodule is the span of the selected basis vectors.

@[simp]

theorem Module.Basis.mem_coordinateSpanSubcomodule {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (b : Basis ι R M) (s : Set ι) [Finite ι] (h : b.coordinateSpanIsStable s) (m : M) : m ∈ b.coordinateSpanSubcomodule s h ↔ m ∈ Submodule.span R (⇑b '' s)

Membership in a coordinate-span subcomodule is membership in the span of the selected basis vectors.

theorem Module.Basis.exists_subcomodule_toSubmodule_eq_span_iff_coordinateSpanIsStable {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] [Finite ι] (b : Basis ι R M) (s : Set ι) : (∃ (N : TauCeti.Subcomodule R C M), N.toSubmodule = Submodule.span R (⇑b '' s)) ↔ b.coordinateSpanIsStable s

A basis subset spans a subcomodule if and only if its coefficient columns have no entries outside the subset.

def Module.Basis.weightCoordinateSpanIsStable {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {α : Type u_1} [LinearOrder α] (b : Basis ι R M) (weight : ι → α) : Prop

Every upper weight-filtration step in a based comodule satisfies the coordinate-vanishing criterion.

Equations

• b.weightCoordinateSpanIsStable weight = ∀ (r : α), b.coordinateSpanIsStable {i : ι | r ≤ weight i}

@[simp]

theorem Module.Basis.weightCoordinateSpanIsStable_iff_blockTriangular {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {α : Type u_1} [LinearOrder α] (b : Basis ι R M) (weight : ι → α) : b.weightCoordinateSpanIsStable weight ↔ (TauCeti.Comodule.coefficientMatrix b).BlockTriangular (⇑OrderDual.toDual ∘ weight)

The upper weight-filtration steps are stable exactly when the coefficient matrix is block triangular with respect to the opposite weight order. The opposite order records that a column of weight r may only have rows of weight at least r.

def Module.Basis.weightCoordinateSpanSubcomodule {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {α : Type u_1} [LinearOrder α] (b : Basis ι R M) (weight : ι → α) (r : α) [Finite ι] (h : (TauCeti.Comodule.coefficientMatrix b).BlockTriangular (⇑OrderDual.toDual ∘ weight)) : TauCeti.Subcomodule R C M

A block-triangular coefficient matrix makes each upper weight-filtration step a subcomodule.

Equations

• b.weightCoordinateSpanSubcomodule weight r h = b.coordinateSpanSubcomodule {i : ι | r ≤ weight i} ⋯

@[simp]

theorem Module.Basis.weightCoordinateSpanSubcomodule_toSubmodule {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {α : Type u_1} [LinearOrder α] (b : Basis ι R M) (weight : ι → α) (r : α) [Finite ι] (h : (TauCeti.Comodule.coefficientMatrix b).BlockTriangular (⇑OrderDual.toDual ∘ weight)) : (b.weightCoordinateSpanSubcomodule weight r h).toSubmodule = Submodule.span R (⇑b '' {i : ι | r ≤ weight i})

The underlying submodule of an upper weight-filtration subcomodule is the span of the basis vectors of weight at least the cutoff.

@[simp]

theorem Module.Basis.mem_weightCoordinateSpanSubcomodule {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {α : Type u_1} [LinearOrder α] (b : Basis ι R M) (weight : ι → α) (r : α) [Finite ι] (h : (TauCeti.Comodule.coefficientMatrix b).BlockTriangular (⇑OrderDual.toDual ∘ weight)) (m : M) : m ∈ b.weightCoordinateSpanSubcomodule weight r h ↔ m ∈ Submodule.span R (⇑b '' {i : ι | r ≤ weight i})

Membership in a weight-coordinate-span subcomodule is membership in the span of the basis vectors whose weights are at least the cutoff.