Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Projective.Chart.BaseChange

Base change of the standard Weierstrass charts #

The three standard affine charts of a projective Weierstrass cubic commute with arbitrary extension of the coefficient ring. The comparison is an algebra equivalence S ⊗[R] ChartRing W i ≃ₐ[S] ChartRing (W.map (algebraMap R S)) i, characterized on pure tensors by coefficient extension. No flatness or ellipticity assumption is needed.

These comparisons give the affine pieces of base change for the projective cubic. The map chartRingMap also makes coefficient extension available for arbitrary ring homomorphisms. Its functoriality laws are TauCeti.chartRingMap_id, TauCeti.chartRingMap_comp_chartRingMap, and TauCeti.chartRingMap_chartRingMap.

The construction uses Mathlib's Algebra.TensorProduct.tensorQuotientEquiv and MvPolynomial.algebraTensorAlgEquiv.

References #

source
@[simp]
theorem WeierstrassCurve.Projective.map_chartRelation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) (f : R →+* S) (k : Fin 2) :
(MvPolynomial.map f) (W.chartRelation i k) = (W.map f).chartRelation i k

The equations of a standard chart extend coefficientwise.

source
theorem WeierstrassCurve.Projective.map_span_chartRelation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) (f : R →+* S) :
Ideal.map (MvPolynomial.map f) (Ideal.span (Set.range (W.chartRelation i))) = Ideal.span (Set.range ((W.map f).chartRelation i))

The defining ideal of a standard chart extends coefficientwise.

source
noncomputable def WeierstrassCurve.Projective.chartRingMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) (f : R →+* S) :
W.ChartRing i →+* (W.map f).ChartRing i

Coefficient extension on the coordinate ring of a standard Weierstrass chart.

Equations
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.Projective.chartRingMap_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) (f : R →+* S) (p : MvPolynomial (Fin 3) R) :
    (W.chartRingMap i f) ((Ideal.Quotient.mk (Ideal.span (Set.range (W.chartRelation i)))) p) = (Ideal.Quotient.mk (Ideal.span (Set.range ((W.map f).chartRelation i)))) ((MvPolynomial.map f) p)

    Coefficient extension sends the class of a polynomial to the class of its image.

    source
    @[simp]
    theorem WeierstrassCurve.Projective.chartRingMap_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) (f : R →+* S) (r : R) :
    (W.chartRingMap i f) ((algebraMap R (W.ChartRing i)) r) = (algebraMap S ((W.map f).ChartRing i)) (f r)

    Coefficient extension respects the structure maps of the chart rings.

    source
    noncomputable def WeierstrassCurve.Projective.chartRingBaseChangeEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) [Algebra R S] :
    TensorProduct R S (W.ChartRing i) ≃ₐ[S] (W.map (algebraMap R S)).ChartRing i

    Arbitrary scalar extension commutes with the coordinate ring of each standard affine chart of the projective Weierstrass cubic.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem WeierstrassCurve.Projective.chartRingBaseChangeEquiv_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) [Algebra R S] (s : S) (x : W.ChartRing i) :
      (W.chartRingBaseChangeEquiv i) (s ⊗ₜ[R] x) = s • (W.chartRingMap i (algebraMap R S)) x

      On pure tensors, the comparison uses the coefficient-extension map on chart rings.

      source
      @[simp]
      theorem WeierstrassCurve.Projective.chartRingBaseChangeEquiv_symm_chartRingMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Projective R) (i : Fin 3) [Algebra R S] (x : W.ChartRing i) :
      (W.chartRingBaseChangeEquiv i).symm ((W.chartRingMap i (algebraMap R S)) x) = 1 ⊗ₜ[R] x

      The inverse comparison recovers the original chart element as 1 ⊗ x from its coefficient extension.

      source
      @[simp]
      theorem TauCeti.chartRingMap_id {R : Type u_1} [CommRing R] {W : WeierstrassCurve.Projective R} {i : Fin 3} :
      W.chartRingMap i (RingHom.id R) = RingHom.id (W.ChartRing i)

      Coefficient extension along the identity is the identity on the chart ring.

      source
      theorem TauCeti.chartRingMap_comp_chartRingMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve.Projective R} {i : Fin 3} {T : Type u_3} [CommRing T] {f : R →+* S} {g : S →+* T} :
      ((W.map f).chartRingMap i g).comp (W.chartRingMap i f) = W.chartRingMap i (g.comp f)

      Successive coefficient extensions compose to extension along the composite ring map.

      source
      @[simp]
      theorem TauCeti.chartRingMap_chartRingMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve.Projective R} {i : Fin 3} {T : Type u_3} [CommRing T] {f : R →+* S} {g : S →+* T} (x : W.ChartRing i) :
      ((W.map f).chartRingMap i g) ((W.chartRingMap i f) x) = (W.chartRingMap i (g.comp f)) x

      Successive coefficient extensions on an element normalize to a single extension.