Multiplicative bases

MultiplicativeBasisDeformations.Foundations.IntegralTable

The graded algebra 𝒪P and its reduction #

For a ray table P with a degree function on the rays, the linearization 𝒪P over any commutative ring is graded by the degrees of the rays (galgLin), and reduction of coefficients along a ring map is a ring map 𝒪P → kP (redLin). This is the algebra A^{(4)} = 𝒪P of integral-deformations.tex.

source
noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.projLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] (p : ℤ) :
↥(P.Lin O) →ₗ[O] ↥(P.Lin O)

The degree projections of 𝒪P.

Instances For
    source
    theorem MultiplicativeBasisDeformations.RaySys.Mult.projLin_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] (p : ℤ) (r : R) :
    (P.projLin d O p) (P.b O r) = if d r = p then P.b O r else 0
    source
    theorem MultiplicativeBasisDeformations.RaySys.Mult.projLin_comp {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] (p q : ℤ) :
    P.projLin d O p ∘ₗ P.projLin d O q = if q = p then P.projLin d O q else 0
    source
    theorem MultiplicativeBasisDeformations.RaySys.Mult.projLin_sum {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] :
    ∑ p ∈ Finset.image d Finset.univ, P.projLin d O p = LinearMap.id
    source
    theorem MultiplicativeBasisDeformations.RaySys.Mult.repr_projLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] (p : ℤ) (x : ↥(P.Lin O)) (r : R) :
    ((P.basis O).repr ((P.projLin d O p) x)) r = if d r = p then ((P.basis O).repr x) r else 0
    source
    noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.grLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] :
    GExt.ZGr ↥(P.Lin O)

    The grading of 𝒪P by the degrees of the rays.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.RaySys.Mult.grLin_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] (r : R) :
      (P.grLin d O).IsHom (d r) (P.b O r)
      source
      theorem MultiplicativeBasisDeformations.RaySys.Mult.repr_eq_zero_of_isHom {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (O : Type u) [CommRing O] [Nontrivial O] {p : ℤ} {x : ↥(P.Lin O)} (hx : (P.grLin d O).IsHom p x) {r : R} (hr : d r ≠ p) :
      ((P.basis O).repr x) r = 0
      source
      noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.galgLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (d : R → ℤ) (hdm : ∀ (r s t : R), P.mul r s = some t → d t = d r + d s) (O : Type u) [CommRing O] [Nontrivial O] (hde' : ∀ (x : V), d (P.e x) = 0) :
      GExt.GAlg ↥(P.Lin O)

      𝒪P as a graded algebra.

      Instances For

        Reduction of coefficients #

        source
        theorem MultiplicativeBasisDeformations.RaySys.Mult.map_mem_Lin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (x : ↥(P.Lin O)) :
        (↑x).map ⇑red ∈ P.Lin K
        source
        def MultiplicativeBasisDeformations.RaySys.Mult.redLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) :
        ↥(P.Lin O) →+* ↥(P.Lin K)

        Reduction 𝒪P → kP.

        Instances For
          source
          theorem MultiplicativeBasisDeformations.RaySys.Mult.redLin_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (r : R) :
          (P.redLin red) (P.b O r) = P.b K r
          source
          theorem MultiplicativeBasisDeformations.RaySys.Mult.redLin_smul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (a : O) (x : ↥(P.Lin O)) :
          (P.redLin red) (a • x) = red a • (P.redLin red) x
          source
          theorem MultiplicativeBasisDeformations.RaySys.Mult.repr_redLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (x : ↥(P.Lin O)) (r : R) :
          ((P.basis K).repr ((P.redLin red) x)) r = red (((P.basis O).repr x) r)