GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_locallyQuasiFinite_of_field
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_locallyQuasiFinite_of_field
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open IsLocalRingLean source · statement
theorem
_root_.GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_locallyQuasiFinite_of_field
{k : Type u} [Field k] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of k)}
[Smooth f] [PreconnectedSpace A]
(G : RelativeGroupLaw k f) (n : ℕ) [LocallyQuasiFinite (G.schemeNsmul n)] :
Flat (G.schemeNsmul n)