NYLL
Module

RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
55 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law surjective scheme Nsmul of flat of field

Imports9
  • Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Kernel
  • Mathlib.AlgebraicGeometry.Morphisms.Flat
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.AlgebraicGeometry.PullbackCarrier
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.Topology.Connected.Clopen
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Imported by2

Declarations

theorem

schemeHomOverComp_mk

L60 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.schemeHomOverComp_mk
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem schemeHomOverComp_mk {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (ψ : T' ⟶ T) (x : SchemeHomOver t f) :
    (schemeHomOverComp ψ rfl x).1 = ψ ≫ x.1
theorem

inv_natural

L64 ↗
GoodReductionJacobian.RelativeGroupLaw.inv_natural
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.inv_natural {T T' : Scheme.{u}} (t :
  T ⟶ Spec (CommRingCat.of R))
    (t' : T' ⟶ Spec (CommRingCat.of R)) (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t f) :
    schemeHomOverComp ψ hψ (G.inv t x) = G.inv t' (schemeHomOverComp ψ hψ x)
theorem

nsmul_coe

L78 ↗
GoodReductionJacobian.RelativeGroupLaw.nsmul_coe
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.nsmul_coe {T : Scheme.{u}} (t : T ⟶
  Spec (CommRingCat.of R)) (n : ℕ) (x : SchemeHomOver t f) :
    (G.nsmul t n x).1 = x.1 ≫ G.schemeNsmul n
theorem

nsmul_mul

L91 ↗
GoodReductionJacobian.RelativeGroupLaw.nsmul_mul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.nsmul_mul (hc : G.IsCommutative) {T :
  Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ)
    (x y : SchemeHomOver t f) : G.nsmul t n (G.mul t x y) = G.mul t (G.nsmul t n x) (G.nsmul t n y)
theorem

nsmul_inv

L106 ↗
GoodReductionJacobian.RelativeGroupLaw.nsmul_inv
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.nsmul_inv (hc : G.IsCommutative) {T :
  Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ)
    (x : SchemeHomOver t f) : G.nsmul t n (G.inv t x) = G.inv t (G.nsmul t n x)
abbrev

prBase

L120 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.prBase
Documentation

The structure morphism of the double fibre product.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
abbrev prBase : pullback f f ⟶ Spec (CommRingCat.of R)
abbrev

ptFst

L123 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.ptFst
Documentation

The first projection as a point over the product base.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
abbrev ptFst : SchemeHomOver (prBase (f := f)) f
abbrev

ptSnd

L126 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.ptSnd
Documentation

The second projection as a point over the product base.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
abbrev ptSnd : SchemeHomOver (prBase (f := f)) f
def

mulHom

L129 ↗
GoodReductionJacobian.RelativeGroupLaw.mulHom
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.mulHom : pullback f f ⟶ A
theorem

mulHom_comp

L133 ↗
GoodReductionJacobian.RelativeGroupLaw.mulHom_comp
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.mulHom_comp : G.mulHom ≫ f = prBase
def

shear

L138 ↗
GoodReductionJacobian.RelativeGroupLaw.shear
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.shear : pullback f f ⟶
  pullback f f
def

shearInv

L144 ↗
GoodReductionJacobian.RelativeGroupLaw.shearInv
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.shearInv : pullback f f ⟶
  pullback f f
theorem

shear_fst

L150 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.shear_fst
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem shear_fst : G.shear ≫ pullback.fst f f = G.mulHom
theorem

shear_snd

L151 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.shear_snd
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem shear_snd : G.shear ≫ pullback.snd f f = pullback.snd f f
theorem

shearInv_fst

L153 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.shearInv_fst
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem shearInv_fst : G.shearInv ≫ pullback.fst f f = (G.mul prBase ptFst (G.inv
  prBase ptSnd)).1
theorem

shearInv_snd

L156 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.shearInv_snd
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem shearInv_snd : G.shearInv ≫ pullback.snd f f = pullback.snd f f
theorem

comp_mul_val

L159 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.comp_mul_val
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem comp_mul_val {S : Scheme.{u}} (s : S ⟶ pullback f f) (x y : SchemeHomOver (prBase (f := f))
  f) :
    s ≫ (G.mul prBase x y).1 = (G.mul (s ≫ prBase) (schemeHomOverComp s rfl x) (schemeHomOverComp s
      rfl y)).1
theorem

comp_inv_val

L166 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.comp_inv_val
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Shear
Lean source · statement
theorem comp_inv_val {S : Scheme.{u}} (s : S ⟶ pullback f f) (x : SchemeHomOver (prBase (f := f))
  f) :
    s ≫ (G.inv prBase x).1 = (G.inv (s ≫ prBase) (schemeHomOverComp s rfl x)).1
abbrev

qBase

L179 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.qBase
Documentation

The structure morphism of the pullback along the chosen base morphism.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
abbrev qBase : pullback s f ⟶ Spec (CommRingCat.of R)
abbrev

qA

L182 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.qA
Documentation

The chosen point pulled back along the first projection.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
abbrev qA : SchemeHomOver (qBase s (f := f)) f
abbrev

qY

L186 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.qY
Documentation

The point given by the second projection of the pullback.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
abbrev qY : SchemeHomOver (qBase s (f := f)) f
def

translate

L189 ↗
GoodReductionJacobian.RelativeGroupLaw.translate
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.translate : pullback s f ⟶
  pullback s f
def

translateInv

L196 ↗
GoodReductionJacobian.RelativeGroupLaw.translateInv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.translateInv : pullback s f
  ⟶ pullback s f
theorem

translate_fst

L202 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translate_fst
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translate_fst : G.translate s a ≫ pullback.fst s f = pullback.fst s f
theorem

translate_snd

L204 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translate_snd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translate_snd : G.translate s a ≫ pullback.snd s f = (G.mul (qBase s) (qA s
  a) (qY s)).1
theorem

translateInv_fst

L207 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translateInv_fst
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translateInv_fst : G.translateInv s a ≫ pullback.fst s f = pullback.fst s f
theorem

translateInv_snd

L209 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translateInv_snd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translateInv_snd : G.translateInv s a ≫ pullback.snd s f =
    (G.mul (qBase s) (G.inv (qBase s) (qA s a)) (qY s)).1
theorem

comp_mul_val'

L212 ↗
GoodReductionJacobian.RelativeGroupLaw.comp_mul_val'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.comp_mul_val' {S' : Scheme.{u}} (r :
  S' ⟶ pullback s f) (t' : S' ⟶ Spec (CommRingCat.of R))
    (hr : r ≫ qBase s = t') (x y : SchemeHomOver (qBase s (f := f)) f) :
    r ≫ (G.mul (qBase s) x y).1 =
      (G.mul t' (schemeHomOverComp r hr x) (schemeHomOverComp r hr y)).1
theorem

comp_inv_val'

L221 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.comp_inv_val'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem comp_inv_val' {S' : Scheme.{u}} (r : S' ⟶ pullback s f) (t' : S' ⟶ Spec (CommRingCat.of R))
    (hr : r ≫ qBase s = t') (x : SchemeHomOver (qBase s (f := f)) f) :
    r ≫ (G.inv (qBase s) x).1 = (G.inv t' (schemeHomOverComp r hr x)).1
theorem

translate_base

L226 ↗
GoodReductionJacobian.RelativeGroupLaw.translate_base
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.translate_base : G.translate s a ≫
  qBase s = qBase s
theorem

translateInv_base

L231 ↗
GoodReductionJacobian.RelativeGroupLaw.translateInv_base
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.translateInv_base : G.translateInv s
  a ≫ qBase s = qBase s
theorem

translate_qA

L236 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translate_qA
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translate_qA : schemeHomOverComp (G.translate s a) (G.translate_base s a) (qA s a) = qA s a
theorem

translate_qY

L242 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translate_qY
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translate_qY : schemeHomOverComp (G.translate s a) (G.translate_base s a) (qY s) =
    G.mul (qBase s) (qA s a) (qY s)
theorem

translateInv_qA

L247 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translateInv_qA
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translateInv_qA : schemeHomOverComp (G.translateInv s a) (G.translateInv_base s a) (qA s a)
  = qA s a
theorem

translateInv_qY

L253 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translateInv_qY
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem translateInv_qY : schemeHomOverComp (G.translateInv s a) (G.translateInv_base s a) (qY s) =
    G.mul (qBase s) (G.inv (qBase s) (qA s a)) (qY s)
theorem

translate_translateInv

L258 ↗
GoodReductionJacobian.RelativeGroupLaw.translate_translateInv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.translate_translateInv : G.translate
  s a ≫ G.translateInv s a = 𝟙 _
theorem

translateInv_translate

L274 ↗
GoodReductionJacobian.RelativeGroupLaw.translateInv_translate
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.translateInv_translate :
  G.translateInv s a ≫ G.translate s a = 𝟙 _
def

translateIso

L287 ↗
GoodReductionJacobian.RelativeGroupLaw.translateIso
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section Translate
variable {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver s f)
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.translateIso : pullback s f
  ≅ pullback s f
abbrev

unitSec

L299 ↗
GoodReductionJacobian.RelativeGroupLaw.unitSec
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
abbrev _root_.GoodReductionJacobian.RelativeGroupLaw.unitSec : Spec
  (CommRingCat.of k) ⟶ B
theorem

unitSec_comp

L303 ↗
GoodReductionJacobian.RelativeGroupLaw.unitSec_comp
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.unitSec_comp : L.unitSec ≫ g = 𝟙 _
theorem

unitSec_schemeNsmul

L308 ↗
GoodReductionJacobian.RelativeGroupLaw.unitSec_schemeNsmul
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.unitSec_schemeNsmul (n : ℕ) :
  L.unitSec ≫ L.schemeNsmul n = L.unitSec
def

pairUnit

L316 ↗
GoodReductionJacobian.RelativeGroupLaw.pairUnit
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.pairUnit : B ⟶ pullback g g
theorem

pairUnit_fst

L321 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.pairUnit_fst
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem pairUnit_fst : L.pairUnit ≫ pullback.fst g g = 𝟙 B
theorem

pairUnit_snd

L322 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.pairUnit_snd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem pairUnit_snd : L.pairUnit ≫ pullback.snd g g = g ≫ L.unitSec
theorem

pairUnit_mulHom

L325 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.pairUnit_mulHom
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem pairUnit_mulHom : L.pairUnit ≫ L.mulHom = 𝟙 B
theorem

symmetry_mulHom

L338 ↗
GoodReductionJacobian.RelativeGroupLaw.symmetry_mulHom
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.symmetry_mulHom (hc :
  L.IsCommutative) : (pullbackSymmetry g g).hom ≫ L.mulHom = L.mulHom
theorem

nn_cond

L351 ↗
GoodReductionJacobian.RelativeGroupLaw.nn_cond
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.nn_cond (n : ℕ) : g ≫ 𝟙 (Spec
  (CommRingCat.of k)) = L.schemeNsmul n ≫ g
def

nn

L357 ↗
GoodReductionJacobian.RelativeGroupLaw.nn
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.nn (n : ℕ) : pullback g g ⟶
  pullback g g
theorem

nn_fst

L362 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.nn_fst
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem nn_fst (n : ℕ) : L.nn n ≫ pullback.fst g g = pullback.fst g g ≫
  L.schemeNsmul n
theorem

nn_snd

L365 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.nn_snd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem nn_snd (n : ℕ) : L.nn n ≫ pullback.snd g g = pullback.snd g g ≫
  L.schemeNsmul n
theorem

range_nn

L369 ↗
GoodReductionJacobian.RelativeGroupLaw.range_nn
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.range_nn (n : ℕ) : Set.range (L.nn n)
  =
    pullback.fst g g ⁻¹' Set.range (L.schemeNsmul n) ∩ pullback.snd g g ⁻¹' Set.range
      (L.schemeNsmul n)
theorem

nn_translateInv

L377 ↗
GoodReductionJacobian.RelativeGroupLaw.nn_translateInv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.nn_translateInv (hc :
  L.IsCommutative) (n : ℕ) :
    L.nn n ≫ L.translateInv g idPoint = L.translateInv g idPoint ≫ L.nn n
theorem

translate_id_snd

L398 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw.translate_id_snd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem translate_id_snd : L.translate g idPoint ≫ pullback.snd g g = L.mulHom
theorem

surjective_schemeNsmul_of_flat_of_field'

L403 ↗
GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_flat_of_field'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
section C4
variable {k : Type u} [Field k] {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of k)} (L :
  RelativeGroupLaw k g)
Lean source · statement
theorem
  _root_.GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_flat_of_field'
    [LocallyOfFiniteType g] [IrreducibleSpace B] (hc : L.IsCommutative) (n : ℕ)
    [Flat (L.schemeNsmul n)] : Surjective (L.schemeNsmul n)
theorem

surjective_schemeNsmul_of_flat_of_field

L524 ↗
GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_flat_of_field
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.shear_fst
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.shear_snd
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.shearInv_fst
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.shearInv_snd
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.translate_fst
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.translate_snd
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.translateInv_fst
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.translateInv_snd
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.pairUnit_fst
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.pairUnit_snd
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.nn_fst
attribute [local simp] GoodReductionJacobian.RelativeGroupLaw.nn_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
  _root_.GoodReductionJacobian GoodReductionJacobian in
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_flat_of_field
    {k : Type u} [Field k] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of k)}
    [LocallyOfFiniteType f] [IrreducibleSpace A]
    (G : RelativeGroupLaw k f)
    (hc : G.IsCommutative)
    (n : ℕ) [Flat (G.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.