Module

RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_isUnit.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_isUnit

1 declaration indexed from sourceView source ↗

Module documentation

Relative Group Law locally Quasi Finite scheme Nsmul of is Unit

Imports4

Imported by2

theorem

locallyQuasiFinite_schemeNsmul_of_isUnit

L32 ↗

GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_isUnit

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_isUnit
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u

Lean source · statement

theorem _root_.GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_isUnit
    {R : Type u} [Field R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    [LocallyOfFiniteType f] (G : RelativeGroupLaw R f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f),
      G.mul t x y = G.mul t y x)
    (n : ℕ) (hn : IsUnit (n : R)) :
    LocallyQuasiFinite (G.schemeNsmul n)

Module documentation

Relative Group Law locally Quasi Finite scheme Nsmul of is Unit

Declarations

locallyQuasiFinite_schemeNsmul_of_isUnit