NYLL
Module

MultiplicationMorphisms.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.MultiplicationMorphisms
7 declarations indexed from sourceView source ↗

Module documentation

The multiplication morphism of a relative group law

The existing morphism G.mulRight f idPoint represents multiplication on every test scheme. Naturality supplies its unit identities and its relation to the actual multiplication-by-an-integer morphisms, over any commutative base ring.

Imports5
Imported by4

Declarations

theorem

pullback_lift_comp_mulRight_idPoint

L34 ↗
GoodReductionJacobian.RelativeGroupLaw.pullback_lift_comp_mulRight_idPoint
Documentation

The existing multiplication morphism evaluates a pair of relative points by the given group law.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · statement
theorem pullback_lift_comp_mulRight_idPoint {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f) :
    pullback.lift x.1 y.1 (x.2.trans y.2.symm) ≫ G.mulRight f idPoint =
      (G.mul t x y).1
theorem

one_coe_eq_comp_one

L53 ↗
GoodReductionJacobian.RelativeGroupLaw.one_coe_eq_comp_one
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · statement
theorem one_coe_eq_comp_one {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) :
    (G.one t).1 = t ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

leftUnit_comp_mulRight_idPoint

L61 ↗
GoodReductionJacobian.RelativeGroupLaw.leftUnit_comp_mulRight_idPoint
Documentation

Inserting the unit in the first coordinate followed by multiplication is the identity scheme morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · full declaration
theorem leftUnit_comp_mulRight_idPoint :
    pullback.lift (f ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1) (𝟙 A)
      (by rw [Category.assoc, (G.one (𝟙 _)).2, Category.comp_id, Category.id_comp]) ≫
        G.mulRight f idPoint = 𝟙 A := by
  let e : SchemeHomOver f f := ⟨f ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1,
    by rw [Category.assoc, (G.one (𝟙 _)).2, Category.comp_id]⟩
  have he : e = G.one f := Subtype.ext (G.one_coe_eq_comp_one f).symm
  have hm : G.mul f e idPoint = idPoint := by rw [he, G.one_mul]
  exact (G.pullback_lift_comp_mulRight_idPoint f e idPoint).trans (congrArg Subtype.val hm)
theorem

rightUnit_comp_mulRight_idPoint

L73 ↗
GoodReductionJacobian.RelativeGroupLaw.rightUnit_comp_mulRight_idPoint
Documentation

Inserting the unit in the second coordinate followed by multiplication is the identity scheme morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · full declaration
theorem rightUnit_comp_mulRight_idPoint :
    pullback.lift (𝟙 A) (f ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1)
      (by rw [Category.assoc, (G.one (𝟙 _)).2, Category.comp_id, Category.id_comp]) ≫
        G.mulRight f idPoint = 𝟙 A := by
  let e : SchemeHomOver f f := ⟨f ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1,
    by rw [Category.assoc, (G.one (𝟙 _)).2, Category.comp_id]⟩
  have he : e = G.one f := Subtype.ext (G.one_coe_eq_comp_one f).symm
  have hm : G.mul f idPoint e = idPoint := by rw [he, G.mul_one]
  exact (G.pullback_lift_comp_mulRight_idPoint f idPoint e).trans (congrArg Subtype.val hm)
theorem

unitPoint_comp_mulRight_idPoint

L84 ↗
GoodReductionJacobian.RelativeGroupLaw.unitPoint_comp_mulRight_idPoint
Documentation

The product unit point is sent to the unit by the actual multiplication morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · statement
theorem unitPoint_comp_mulRight_idPoint :
    pullback.lift (G.one (𝟙 (Spec (CommRingCat.of R)))).1
      (G.one (𝟙 (Spec (CommRingCat.of R)))).1 rfl ≫ G.mulRight f idPoint =
        (G.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

schemeNsmul_pair_id_comp_mulRight

L95 ↗
GoodReductionJacobian.RelativeGroupLaw.schemeNsmul_pair_id_comp_mulRight
Documentation

Pairing multiplication by n with the identity and then multiplying gives the actual multiplication-by-n+1 morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · statement
theorem schemeNsmul_pair_id_comp_mulRight (n : ℕ) :
    pullback.lift (G.schemeNsmul n) (𝟙 A)
      ((G.schemeNsmul_over n).trans (Category.id_comp f).symm) ≫
        G.mulRight f idPoint = G.schemeNsmul (n + 1)
theorem

unit_comp_schemeNsmul

L105 ↗
GoodReductionJacobian.RelativeGroupLaw.unit_comp_schemeNsmul
Documentation

Every multiplication-by-an-integer morphism fixes the unit section.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f)
Lean source · statement
theorem unit_comp_schemeNsmul (n : ℕ) :
    (G.one (𝟙 (Spec (CommRingCat.of R)))).1 ≫ G.schemeNsmul n =
      (G.one (𝟙 (Spec (CommRingCat.of R)))).1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.