Documentation

DerivedAlgGeo.LinearAlgebra.GradedBasis

Graded pieces determined by a weighted basis #

Given a basis-like family b : ι → A and a weight w : ι → ℕ, this file defines the weight-k submodule as the span of the corresponding basis vectors. It proves that a linearly independent spanning family gives an internal direct-sum decomposition and that multiplicativity may be checked on basis vectors.

The construction is independent of numerical intersection rings and algebraic geometry. Geometric numerical-ring constructors consume it from AlgebraicGeometry/Numerical/Core/GradedBasis.lean.

source
def DerivedAlgGeo.LinearAlgebra.gradedPiece {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] (b : ι → A) (w : ι → ℕ) (k : ℕ) :
Submodule ℚ A

The span of the vectors of weight k.

Equations
Instances For
    source
    theorem DerivedAlgGeo.LinearAlgebra.mem_gradedPiece {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] {b : ι → A} {w : ι → ℕ} (i : ι) :
    b i ∈ gradedPiece b w (w i)

    Every vector of the indexed family lies in its own graded piece.

    source
    theorem DerivedAlgGeo.LinearAlgebra.gradedPiece_eq_bot {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] {b : ι → A} {w : ι → ℕ} {n : ℕ} (hw : ∀ (i : ι), w i ≤ n) {k : ℕ} (hk : n < k) :
    gradedPiece b w k = ⊥

    If all weights are at most n, every graded piece above n vanishes.

    source
    theorem DerivedAlgGeo.LinearAlgebra.gradedPiece_iSupIndep {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] {b : ι → A} {w : ι → ℕ} (hb : LinearIndependent ℚ b) :
    iSupIndep (gradedPiece b w)

    Graded pieces cut out by distinct weights are independent.

    source
    theorem DerivedAlgGeo.LinearAlgebra.gradedPiece_iSup_eq_top {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] {b : ι → A} {w : ι → ℕ} (hsp : Submodule.span ℚ (Set.range b) = ⊤) :
    ⨆ (k : ℕ), gradedPiece b w k = ⊤

    The graded pieces span whenever the indexed family spans.

    source
    theorem DerivedAlgGeo.LinearAlgebra.gradedPiece_isInternal {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] {b : ι → A} {w : ι → ℕ} (hb : LinearIndependent ℚ b) (hsp : Submodule.span ℚ (Set.range b) = ⊤) :
    DirectSum.IsInternal (gradedPiece b w)

    A linearly independent spanning family decomposes the module as the direct sum of its weight pieces.

    source
    theorem DerivedAlgGeo.LinearAlgebra.gradedPiece_mul_mem {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] {b : ι → A} {w : ι → ℕ} (hmul : ∀ (p q : ι), b p * b q ∈ gradedPiece b w (w p + w q)) {i j : ℕ} {x y : A} (hx : x ∈ gradedPiece b w i) (hy : y ∈ gradedPiece b w j) :
    x * y ∈ gradedPiece b w (i + j)

    Multiplicativity of the grading, promoted from indexed vectors to all elements of their weight pieces.