Documentation

TauCeti.RingTheory.Node.BaseChange

Base change of the nodal equation #

The coordinate algebra of xy = a commutes with change of coefficient ring. The canonical isomorphism identifies the two coordinates and the scalar extension maps. It gives the affine chart comparison needed when a nodal curve is pulled back along a morphism of bases.

Reference #

source
noncomputable def TauCeti.NodeAlgebra.baseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a : R) :
TensorProduct R S (NodeAlgebra R a) ≃ₐ[S] NodeAlgebra S ((algebraMap R S) a)

The isomorphism from the scalar extension of the nodal algebra to the nodal algebra of the image of its smoothing parameter.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TauCeti.NodeAlgebra.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a : R) :
    NodeAlgebra R a →+* NodeAlgebra S ((algebraMap R S) a)

    The ring map taking the original nodal coordinates into the changed coefficient ring.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.NodeAlgebra.map_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a r : R) :
      (map a) ((algebraMap R (NodeAlgebra R a)) r) = (algebraMap S (NodeAlgebra S ((algebraMap R S) a))) ((algebraMap R S) r)

      Changing coefficients sends constants to their images in the new coefficient ring.

      source
      @[simp]
      theorem TauCeti.NodeAlgebra.map_coord {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a : R) (i : Fin 2) :
      (map a) (coord a i) = coord ((algebraMap R S) a) i

      Changing coefficients preserves each nodal coordinate.

      source
      @[simp]
      theorem TauCeti.NodeAlgebra.baseChange_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a : R) (s : S) (x : NodeAlgebra R a) :
      (baseChange a) (s ⊗ₜ[R] x) = s • (map a) x

      Base change of a pure tensor is scalar multiplication of the changed coordinate map.

      source
      @[simp]
      theorem TauCeti.NodeAlgebra.baseChange_symm_coord {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a : R) (i : Fin 2) :
      (baseChange a).symm (coord ((algebraMap R S) a) i) = 1 ⊗ₜ[R] coord a i

      The inverse base-change map sends the new coordinates to the old coordinates in the extended algebra.