Module

RelativeGroupLaw_fibre_schemeNsmul_eq_schemeFibreEndo.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_fibre_schemeNsmul_eq_schemeFibreEndo

3 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law fibre scheme Nsmul eq scheme Fibre Endo

Imports2

Imported by5

theorem

fibre_nsmul

L47 ↗

GoodReductionJacobian.RelativeGroupLaw.fibre_nsmul

Source context 8 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem fibre_nsmul (G : RelativeGroupLaw R f) (s : (Spec (CommRingCat.of R) : Scheme.{u}))
    {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))) (n : ℕ)
    (x : SchemeHomOver t' (fibreStr f s)) :
    (G.fibre s).nsmul t' n x = fibrePointOfBase s (G.nsmul _ n (fibrePointToBase s x))

theorem

nsmul_coe_eq_comp_schemeNsmul'

L56 ↗

GoodReductionJacobian.RelativeGroupLaw.nsmul_coe_eq_comp_schemeNsmul'

Source context 8 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
universe u
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem nsmul_coe_eq_comp_schemeNsmul' (G : RelativeGroupLaw R f) {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

fibre_schemeNsmul_eq_schemeFibreEndo

L79 ↗

GoodReductionJacobian.RelativeGroupLaw.fibre_schemeNsmul_eq_schemeFibreEndo

Source context 9 commands

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

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

Lean source · statement

theorem _root_.GoodReductionJacobian.RelativeGroupLaw.fibre_schemeNsmul_eq_schemeFibreEndo
    {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) (s : (Spec (CommRingCat.of R) : Scheme.{u})) (n : ℕ) :
    (G.fibre s).schemeNsmul n = schemeFibreEndo f (G.schemeNsmul n) (G.schemeNsmul_over n) s

Module documentation

Relative Group Law fibre scheme Nsmul eq scheme Fibre Endo

Declarations

fibre_nsmul

nsmul_coe_eq_comp_schemeNsmul'

fibre_schemeNsmul_eq_schemeFibreEndo