GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_forall_flat_fibre_schemeNsmul
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_forall_flat_fibre_schemeNsmul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobianLean source · statement
theorem
_root_.GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_forall_flat_fibre_schemeNsmul
{R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
[Flat f] [LocallyOfFinitePresentation f] (G : RelativeGroupLaw R f) (n : ℕ)
(hfib : ∀ s : (Spec (CommRingCat.of R) : Scheme.{u}), Flat ((G.fibre s).schemeNsmul n)) :
Flat (G.schemeNsmul n)