Module

relativeGroupLaw_baseChange_eq.lean

Nyll.JacobianVarieties.Picard.relativeGroupLaw_baseChange_eq

2 declarations indexed from sourceView source ↗

Module documentation

Compatibility of the relative Picard group law with base change

A group law is determined by its multiplication. The multiplication comparison for base change therefore identifies the represented relative Picard group laws.

Imports13

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

ext_of_mul

L81 ↗

JacobianVarieties.Picard.Proofs.GroupLawBaseChange.GoodReductionJacobian.RelativeGroupLaw.ext_of_mul

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GroupLawBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian

Lean source · statement

theorem ext_of_mul {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G G' : RelativeGroupLaw R f)
    (h : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f),
      G.mul t x y = G'.mul t x y) :
    G = G'

theorem

relativeGroupLaw_baseChange_eq

L116 ↗

AlgebraicGeometry.RelPicard.relativeGroupLaw_baseChange_eq

Source context 11 commands