Documentation

TauCeti.RingTheory.GradedAlgebra.CoeffSubalgebra.Basic

The graded subalgebra of B[X] cut out by a graded family of coefficients #

Let B be an R-algebra and let M : ℕ → Submodule R B be a graded family of submodules: 1 ∈ M 0 and M m * M n ⊆ M (m + n) (SetLike.GradedMonoid M). The polynomials ∑ bₙ Xⁿ with bₙ ∈ M n for every n form an R-subalgebra TauCeti.coeffSubalgebra M of B[X]: it is the direct sum ⨁ₙ Mₙ Xⁿ, realized inside B[X] so that elements of different degrees that are equal in B stay apart. This file grades it by the power of X: the degree n piece consists of the monomials b Xⁿ with b ∈ M n, and the homogeneous components of a polynomial are its monomials.

Two instances motivate the construction. For an ideal I of a commutative ring R and M n = Iⁿ it is Mathlib's Rees algebra reesAlgebra I, whose grading in TauCeti.RingTheory.ReesAlgebra.Grading is the one constructed here. For a divisor D of an algebraic function field and M n = L(nD) it is the section ring ⨁ₙ L(nD) of D (TauCeti.FieldTheory.FunctionField.RiemannRoch.SectionRing), the graded ring from which projective models of a curve are built as Proj.

Main definitions #

Main results #

source
def TauCeti.coeffSubalgebra {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] :
Subalgebra R (Polynomial B)

The R-subalgebra of B[X] of polynomials whose n-th coefficient lies in M n, for a graded family M of submodules of B: the direct sum ⨁ₙ Mₙ Xⁿ realized inside B[X].

Instances For
    source
    @[simp]
    theorem TauCeti.mem_coeffSubalgebra_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {f : Polynomial B} :
    f ∈ coeffSubalgebra M ↔ ∀ (n : ℕ), f.coeff n ∈ M n
    source
    theorem TauCeti.monomial_mem_coeffSubalgebra_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} {b : B} :
    (Polynomial.monomial n) b ∈ coeffSubalgebra M ↔ b ∈ M n

    A monomial b Xⁿ lies in coeffSubalgebra M exactly when b ∈ M n.

    source
    noncomputable def TauCeti.coeffSubalgebra.monomial {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (n : ℕ) (b : B) (hb : b ∈ M n) :
    ↥(coeffSubalgebra M)

    The monomial b Xⁿ of coeffSubalgebra M, for b ∈ M n.

    Instances For
      source
      @[simp]
      theorem TauCeti.coeffSubalgebra.coe_monomial {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (n : ℕ) (b : B) (hb : b ∈ M n) :
      ↑(monomial M n b hb) = (Polynomial.monomial n) b
      source
      noncomputable def TauCeti.coeffSubalgebra.X {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
      ↥(coeffSubalgebra M)

      The central polynomial parameter, when its coefficient belongs to degree one.

      Instances For
        source
        @[simp]
        theorem TauCeti.coeffSubalgebra.coe_X {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
        ↑(X M h1) = Polynomial.X
        source
        theorem TauCeti.coeffSubalgebra.commute_X {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (a : ↥(coeffSubalgebra M)) :
        Commute (X M h1) a

        The polynomial parameter commutes with every element of the coefficient subalgebra.

        source
        instance TauCeti.coeffSubalgebra.span_X_isTwoSided {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
        (Ideal.span {X M h1}).IsTwoSided

        The ideal generated by the central polynomial parameter is two-sided.

        source
        theorem TauCeti.coeffSubalgebra.X_mul_injective {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
        Function.Injective fun (a : ↥(coeffSubalgebra M)) => X M h1 * a

        Multiplication by the polynomial parameter is injective.

        source
        @[instance_reducible]
        noncomputable def TauCeti.coeffSubalgebra.algebra {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
        Algebra (Polynomial R) ↥(coeffSubalgebra M)

        The parameter-ring algebra structure, available when the polynomial parameter belongs to the coefficient subalgebra. Install it with letI := coeffSubalgebra.algebra M h1.

        Instances For
          source
          @[simp]
          theorem TauCeti.coeffSubalgebra.algebraMap_X {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
          (algebraMap (Polynomial R) ↥(coeffSubalgebra M)) Polynomial.X = X M h1
          source
          @[simp]
          theorem TauCeti.coeffSubalgebra.coe_algebraMap {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (p : Polynomial R) :
          ↑((algebraMap (Polynomial R) ↥(coeffSubalgebra M)) p) = Polynomial.map (algebraMap R B) p
          source
          theorem TauCeti.coeffSubalgebra.isScalarTower {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
          IsScalarTower R (Polynomial R) ↥(coeffSubalgebra M)

          The parameter-ring algebra structure extends the coefficient-ring algebra structure.

          source
          theorem TauCeti.coeffSubalgebra.monomial_coeff_mem {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (f : ↥(coeffSubalgebra M)) (n : ℕ) :
          (Polynomial.monomial n) ((↑f).coeff n) ∈ coeffSubalgebra M

          The monomial formed by any single coefficient of an element of coeffSubalgebra M lies in coeffSubalgebra M.

          source
          noncomputable def TauCeti.coeffSubalgebra.grade {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (n : ℕ) :
          Submodule R ↥(coeffSubalgebra M)

          The degree n piece of coeffSubalgebra M: the monomials b Xⁿ with b ∈ M n.

          Instances For
            source
            theorem TauCeti.coeffSubalgebra.mem_grade_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} {f : ↥(coeffSubalgebra M)} :
            f ∈ grade M n ↔ ∃ b ∈ M n, (Polynomial.monomial n) b = ↑f

            The elements of degree n of coeffSubalgebra M are the monomials b Xⁿ with b ∈ M n.

            source
            theorem TauCeti.coeffSubalgebra.mem_grade_iff_monomial_coeff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} {f : ↥(coeffSubalgebra M)} :
            f ∈ grade M n ↔ (Polynomial.monomial n) ((↑f).coeff n) = ↑f

            An element of coeffSubalgebra M has degree n exactly when it is the monomial of degree n formed by its n-th coefficient.

            source
            theorem TauCeti.coeffSubalgebra.monomial_mem_grade {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (n : ℕ) (b : B) (hb : b ∈ M n) :
            monomial M n b hb ∈ grade M n

            The monomial b Xⁿ with b ∈ M n has degree n.

            source
            theorem TauCeti.coeffSubalgebra.X_mem_grade_one {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
            X M h1 ∈ grade M 1

            The polynomial parameter belongs to the degree-one piece.

            source
            theorem TauCeti.coeffSubalgebra.coeff_eq_zero_of_mem_grade {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {m n : ℕ} {f : ↥(coeffSubalgebra M)} (hf : f ∈ grade M n) (hmn : m ≠ n) :
            (↑f).coeff m = 0

            The coefficients of an element of degree n vanish away from n.

            source
            theorem TauCeti.coeffSubalgebra.coeff_eq_zero_iff_of_mem_grade {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} {f : ↥(coeffSubalgebra M)} (hf : f ∈ grade M n) :
            (↑f).coeff n = 0 ↔ f = 0

            An element of degree n vanishes exactly when its n-th coefficient does.

            source
            theorem TauCeti.coeffSubalgebra.eval_one_of_mem_grade {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} {f : ↥(coeffSubalgebra M)} (hf : f ∈ grade M n) :
            Polynomial.eval 1 ↑f = (↑f).coeff n

            Evaluating an element of degree n at X = 1 gives its n-th coefficient.

            source
            instance TauCeti.coeffSubalgebra.gradedMonoid {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] :
            SetLike.GradedMonoid (grade M)
            source
            theorem TauCeti.coeffSubalgebra.isInternal_grade {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] :
            DirectSum.IsInternal (grade M)

            coeffSubalgebra M is the internal direct sum of its graded pieces.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.coeffSubalgebra.gradedAlgebra {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] :
            GradedAlgebra (grade M)

            The grading of coeffSubalgebra M by the power of X.

            source
            @[simp]
            theorem TauCeti.coeffSubalgebra.coe_decompose_apply {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (f : ↥(coeffSubalgebra M)) (n : ℕ) :
            ↑↑(((DirectSum.decompose (grade M)) f) n) = (Polynomial.monomial n) ((↑f).coeff n)

            The degree n component of an element f of coeffSubalgebra M is the monomial f.coeff n • Xⁿ.

            source
            noncomputable def TauCeti.coeffSubalgebra.gradeEquiv {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (n : ℕ) :
            ↥(M n) ≃ₗ[R] ↥(grade M n)

            The R-linear isomorphism b ↦ b Xⁿ from M n onto the degree n piece of coeffSubalgebra M.

            Instances For
              source
              @[simp]
              theorem TauCeti.coeffSubalgebra.coe_gradeEquiv_apply {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (n : ℕ) (b : ↥(M n)) :
              ↑↑((gradeEquiv M n) b) = (Polynomial.monomial n) ↑b
              source
              @[simp]
              theorem TauCeti.coeffSubalgebra.coe_gradeEquiv_symm_apply {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (n : ℕ) (f : ↥(grade M n)) :
              ↑((gradeEquiv M n).symm f) = (↑↑f).coeff n

              Generation in degree one #

              source
              theorem TauCeti.coeffSubalgebra_le_coeffSubalgebra_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {M' : ℕ → Submodule R B} [SetLike.GradedMonoid M'] :
              coeffSubalgebra M ≤ coeffSubalgebra M' ↔ ∀ (n : ℕ), M n ≤ M' n

              coeffSubalgebra M ≤ coeffSubalgebra M' exactly when M n ≤ M' n for every n.

              source
              theorem Submodule.adjoin_map_monomial_one_eq_coeffSubalgebra_pow {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (N : Submodule R B) :
              Algebra.adjoin R ↑(map (↑R (Polynomial.monomial 1)) N) = TauCeti.coeffSubalgebra fun (n : ℕ) => N ^ n

              The subalgebra of B[X] generated by the monomials b X with b ∈ N is coeffSubalgebra of the powers n ↦ Nⁿ, the polynomials whose n-th coefficient lies in Nⁿ.

              For an ideal N of a commutative ring B = R this is Mathlib's adjoin_monomial_eq_reesAlgebra, and the proof is the same.

              source
              theorem TauCeti.coeffSubalgebra.map_val_adjoin_grade_one {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] :
              Subalgebra.map (coeffSubalgebra M).val (Algebra.adjoin R ↑(grade M 1)) = coeffSubalgebra fun (n : ℕ) => M 1 ^ n

              The subalgebra of coeffSubalgebra M generated by its elements of degree one is, inside B[X], coeffSubalgebra of the powers n ↦ (M 1)ⁿ.

              source
              theorem TauCeti.coeffSubalgebra.monomial_mem_adjoin_grade_one_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} {b : B} (hb : b ∈ M n) :
              monomial M n b hb ∈ Algebra.adjoin R ↑(grade M 1) ↔ b ∈ M 1 ^ n

              A monomial b Xⁿ lies in the subalgebra generated by the elements of degree one exactly when b ∈ (M 1)ⁿ, that is, when b is a sum of products of n elements of M 1.

              source
              theorem TauCeti.coeffSubalgebra.grade_subset_adjoin_grade_one_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] {n : ℕ} :
              ↑(grade M n) ⊆ ↑(Algebra.adjoin R ↑(grade M 1)) ↔ M n ≤ M 1 ^ n

              Generation in degree one, degree by degree. The elements of degree n of coeffSubalgebra M lie in the subalgebra generated by its elements of degree one exactly when M n ≤ (M 1)ⁿ.

              source
              theorem TauCeti.coeffSubalgebra.adjoin_grade_one_eq_top_iff {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] :
              Algebra.adjoin R ↑(grade M 1) = ⊤ ↔ ∀ (n : ℕ), M n ≤ M 1 ^ n

              Generation in degree one. coeffSubalgebra M is generated as an R-algebra by its elements of degree one exactly when M n ≤ (M 1)ⁿ for every n, that is, when every element of M n is a sum of products of n elements of M 1.

              source
              theorem TauCeti.coeffSubalgebra.adjoin_monomial_one_eq_top {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (s : Set B) :
              Algebra.adjoin R (Set.range fun (b : ↑s) => monomial (fun (n : ℕ) => Submodule.span R s ^ n) 1 ↑b ⋯) = ⊤

              Generators in degree one. coeffSubalgebra of the powers n ↦ Nⁿ of the submodule N = span R s is generated as an R-algebra by the monomials b X with b ∈ s.

              The degree zero piece and evaluation at X = 1 #

              source
              theorem TauCeti.coeffSubalgebra.algebraMap_grade_pow_zero_surjective {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (N : Submodule R B) :
              Function.Surjective ⇑(algebraMap R ↥(grade (fun (n : ℕ) => N ^ n) 0))

              The degree zero piece of coeffSubalgebra of the powers n ↦ Nⁿ is the image of R, since N⁰ = 1 is the image of R in B.

              source
              noncomputable def TauCeti.coeffSubalgebra.eval {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (r : R) :
              ↥(coeffSubalgebra M) →ₐ[R] B

              Evaluation at a scalar parameter, also for a noncommutative coefficient algebra.

              Instances For
                source
                theorem TauCeti.coeffSubalgebra.eval_apply {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (r : R) (f : ↥(coeffSubalgebra M)) :
                (eval M r) f = Polynomial.eval ((algebraMap R B) r) ↑f

                Scalar evaluation agrees with ambient polynomial evaluation.

                source
                @[simp]
                theorem TauCeti.coeffSubalgebra.eval_monomial {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (r : R) (n : ℕ) (b : B) (hb : b ∈ M n) :
                (eval M r) (monomial M n b hb) = b * (algebraMap R B) r ^ n
                source
                @[simp]
                theorem TauCeti.coeffSubalgebra.eval_X {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (r : R) (h1 : 1 ∈ M 1) :
                (eval M r) (X M h1) = (algebraMap R B) r
                source
                @[simp]
                theorem TauCeti.coeffSubalgebra.eval_algebraMap {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) (r : R) (p : Polynomial R) :
                (eval M r) ((algebraMap (Polynomial R) ↥(coeffSubalgebra M)) p) = (algebraMap R B) (Polynomial.eval r p)
                source
                noncomputable def TauCeti.coeffSubalgebra.evalOne {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] :
                ↥(coeffSubalgebra M) →ₐ[R] B

                Evaluation at X = 1, ∑ bₙ Xⁿ ↦ ∑ bₙ, as an R-algebra map.

                Instances For
                  source
                  theorem TauCeti.coeffSubalgebra.evalOne_eq_eval {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] :
                  evalOne M = eval M 1

                  Evaluation at one is scalar evaluation with parameter 1.

                  source
                  @[simp]
                  theorem TauCeti.coeffSubalgebra.evalOne_X {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (h1 : 1 ∈ M 1) :
                  (evalOne M) (X M h1) = 1
                  source
                  theorem TauCeti.coeffSubalgebra.evalOne_apply {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (f : ↥(coeffSubalgebra M)) :
                  (evalOne M) f = Polynomial.eval 1 ↑f

                  Evaluation at X = 1 is ambient polynomial evaluation at 1.

                  source
                  @[simp]
                  theorem TauCeti.coeffSubalgebra.evalOne_monomial {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {M : ℕ → Submodule R B} [SetLike.GradedMonoid M] (n : ℕ) (b : B) (hb : b ∈ M n) :
                  (evalOne M) (monomial M n b hb) = b
                  source
                  theorem TauCeti.coeffSubalgebra.evalOne_surjective {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (M : ℕ → Submodule R B) [SetLike.GradedMonoid M] (hM : ⨆ (n : ℕ), M n = ⊤) :
                  Function.Surjective ⇑(evalOne M)

                  Evaluation at one is surjective when the graded pieces span the coefficient algebra.