Documentation

TauCeti.Algebra.WordFiltration.Rees

The zero fibre of a word-filtration Rees algebra #

For a linear generating family f, the Rees algebra is the subalgebra of A[X] whose coefficient in degree n lies in wordFiltration f n. Its symbol map sends that coefficient to its class in the n-th associated-graded piece. This map is surjective, and its kernel is the ideal generated by the central parameter. Thus specializing the Rees parameter to zero gives the associated graded, even when A is noncommutative.

This symbol map differs from ambient polynomial evaluation at zero: a positive-degree monomial can have a nonzero symbol.

source
@[reducible, inline]
abbrev TauCeti.Algebra.wordFiltration.Rees {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) :
Subalgebra R (Polynomial A)

The Rees algebra of the word filtration generated by f.

Instances For
    source
    noncomputable def TauCeti.Algebra.wordFiltration.reesSymbol {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) :
    ↥(Rees f) →ₐ[R] AssociatedGraded f

    The symbol homomorphism from the Rees algebra to the associated graded.

    Instances For
      source
      @[simp]
      theorem TauCeti.Algebra.wordFiltration.reesSymbol_monomial {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (n : ℕ) (a : A) (ha : a ∈ wordFiltration f n) :
      (reesSymbol f) (coeffSubalgebra.monomial (wordFiltration f) n a ha) = (DirectSum.of (GradedPiece f) n) (Submodule.Quotient.mk ⟨a, ha⟩)

      A homogeneous Rees monomial maps to the corresponding homogeneous symbol.

      source
      @[simp]
      theorem TauCeti.Algebra.wordFiltration.reesSymbol_apply {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (p : ↥(Rees f)) (n : ℕ) :
      ((reesSymbol f) p) n = Submodule.Quotient.mk ⟨(↑p).coeff n, ⋯⟩

      The degree-n component of the symbol is the class of the n-th coefficient.

      source
      theorem TauCeti.Algebra.wordFiltration.reesSymbol_eq_zero_iff {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (p : ↥(Rees f)) :
      (reesSymbol f) p = 0 ↔ ∀ (n : ℕ), (↑p).coeff n ∈ wordFiltrationPrevious f n

      The symbol map vanishes exactly when each coefficient lies one step lower.

      source
      theorem TauCeti.Algebra.wordFiltration.reesSymbol_surjective {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) :
      Function.Surjective ⇑(reesSymbol f)

      Every associated-graded element has a Rees lift.

      source
      @[simp]
      theorem TauCeti.Algebra.wordFiltration.reesSymbol_X {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) :
      (reesSymbol f) (coeffSubalgebra.X (wordFiltration f) ⋯) = 0

      The central Rees parameter has zero symbol.

      source
      theorem TauCeti.Algebra.wordFiltration.reesSymbol_eq_zero_iff_exists_X_mul_eq {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (p : ↥(Rees f)) :
      (reesSymbol f) p = 0 ↔ ∃ (q : ↥(Rees f)), coeffSubalgebra.X (wordFiltration f) ⋯ * q = p

      A Rees element has zero symbol exactly when it is a multiple of the parameter.

      source
      theorem TauCeti.Algebra.wordFiltration.ker_reesSymbol {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) :
      RingHom.ker ↑(reesSymbol f) = Ideal.span {coeffSubalgebra.X (wordFiltration f) ⋯}

      The kernel of the symbol map is the principal ideal of the central parameter.

      source
      noncomputable def TauCeti.Algebra.wordFiltration.reesZeroFiberEquiv {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) :
      (↥(Rees f) ⧸ Ideal.span {coeffSubalgebra.X (wordFiltration f) ⋯}) ≃ₐ[R] AssociatedGraded f

      Specializing the Rees parameter to zero gives the associated graded algebra.

      Instances For
        source
        @[simp]
        theorem TauCeti.Algebra.wordFiltration.reesZeroFiberEquiv_mk {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (p : ↥(Rees f)) :
        (reesZeroFiberEquiv f) ((Ideal.Quotient.mk (Ideal.span {coeffSubalgebra.X (wordFiltration f) ⋯})) p) = (reesSymbol f) p

        The zero-fibre comparison sends the class of a Rees polynomial to its symbol.