GoodReductionJacobian.RelativeGroupLaw.formallyUnramified_schemeNsmul_of_forall_sqZero
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_formallyUnramified_schemeNsmul_of_forall_sqZero
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe uLean source · statement
theorem
_root_.GoodReductionJacobian.RelativeGroupLaw.formallyUnramified_schemeNsmul_of_forall_sqZero
{R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
(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 : ℕ)
(hTF : ∀ (R' S' : CommRingCat.{u}) (φ : R' ⟶ S'), Function.Surjective φ →
RingHom.ker φ.hom ^ 2 = ⊥ →
∀ (t : Spec R' ⟶ Spec (CommRingCat.of R)) (k : SchemeHomOver t f),
schemeHomOverComp (Spec.map φ) rfl k = G.one (Spec.map φ ≫ t) →
G.nsmul t n k = G.one t → k = G.one t) :
FormallyUnramified (G.schemeNsmul n)