Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_fibre_mul_comm

theorem

fibre_mul_comm

GoodReductionJacobian.RelativeGroupLaw.fibre_mul_comm

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_fibre_mul_comm
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u

Lean source · statement

theorem _root_.GoodReductionJacobian.RelativeGroupLaw.fibre_mul_comm
    {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f),
      G.mul t x y = G.mul t y x)
    (s : (Spec (CommRingCat.of R) : Scheme.{u}))
    {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of (RelativeGroupLaw.baseResidueField s)))
    (x y : SchemeHomOver t' (RelativeGroupLaw.fibreStr f s)) :
    (G.fibre s).mul t' x y = (G.fibre s).mul t' y x

RelativeGroupLaw_fibre_mul_comm.lean

Module documentation

Relative Group Law fibre mul comm

fibre_mul_comm

Module documentation

Relative Group Law fibre mul comm

Declarations

fibre_mul_comm