NYLL
Module

RelativeGroupLaw_surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul
2 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law surjective scheme Nsmul of forall surjective fibre scheme Nsmul

Imports13
Imported by1

Declarations

theorem

surjective_of_forall_surjective_schemeFibreEndo'

L42 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul.FibSurj.surjective_of_forall_surjective_schemeFibreEndo'
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
Lean source · statement
theorem FibSurj.surjective_of_forall_surjective_schemeFibreEndo'
    {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X) (hh : h ≫ f = f)
    (hfib : ∀ s : S, Surjective (schemeFibreEndo f h hh s)) :
    Surjective h
theorem

surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul

L71 ↗
GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul
Source context 6 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open RelativeGroupLaw_surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian in
Lean source · statement
theorem surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul
    {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) (n : ℕ)
    (hfib : ∀ s : (Spec (CommRingCat.of R) : Scheme.{u}), Surjective ((G.fibre s).schemeNsmul n)) :
    Surjective (G.schemeNsmul n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.