GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOver_baseChange_baseChange_iso
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_schemeHomOver_baseChange_baseChange_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe uLean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOver_baseChange_baseChange_iso
{R : Type u} [CommRing R] {R' : Type u} [CommRing R'] {R'' : Type u} [CommRing R'']
(ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R))
(j : Spec (CommRingCat.of R'') ⟶ Spec (CommRingCat.of R'))
{A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)} (G : RelativeGroupLaw R f) :
∃ (u : SchemeHomOver (RelativeGroupLaw.baseChangeStr j (RelativeGroupLaw.baseChangeStr ι f))
(RelativeGroupLaw.baseChangeStr (j ≫ ι) f))
(v : SchemeHomOver (RelativeGroupLaw.baseChangeStr (j ≫ ι) f)
(RelativeGroupLaw.baseChangeStr j (RelativeGroupLaw.baseChangeStr ι f))),
u.1 ≫ v.1 = 𝟙 _ ∧ v.1 ≫ u.1 = 𝟙 _ ∧
u.1 ≫ pullback.fst f (j ≫ ι) = pullback.fst (pullback.snd f ι) j ≫ pullback.fst f ι ∧
∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R''))
(x y : SchemeHomOver t (RelativeGroupLaw.baseChangeStr j (RelativeGroupLaw.baseChangeStr ι
f))),
NeronModelInfra.schemeHomOverComp (((G.baseChange ι).baseChange j).mul t x y) u =
(G.baseChange (j ≫ ι)).mul t (NeronModelInfra.schemeHomOverComp x u)
(NeronModelInfra.schemeHomOverComp y u)