Module

RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_field.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_field

1 declaration indexed from sourceView source ↗

Module documentation

Relative Group Law flat scheme Nsmul of is Finite of field

Imports6

Imported by2

theorem

flat_schemeNsmul_of_isFinite_of_field

L33 ↗

GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_isFinite_of_field

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_field
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian IsLocalRing
universe u

Lean source · statement

theorem _root_.GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_isFinite_of_field
    {k : Type u} [Field k] {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of k)}
    (L : RelativeGroupLaw k f) (hJ : AbelianSchemePropertyBundle k f)
    (n : ℕ) (hfin : IsFinite (L.schemeNsmul n)) :
    Flat (L.schemeNsmul n)

Module documentation

Relative Group Law flat scheme Nsmul of is Finite of field

Declarations

flat_schemeNsmul_of_isFinite_of_field