NYLL
Module

RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
4 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law base Change scheme Nsmul comp fst and eq pullback map

Imports2
Imported by1

Declarations

theorem

baseChange_nsmul

L55 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map.GoodReductionJacobian.RelativeGroupLaw.baseChange_nsmul
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
variable (ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R))
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem baseChange_nsmul (G : RelativeGroupLaw R f) {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of
  R')) (n : ℕ)
    (x : SchemeHomOver t' (baseChangeStr ι f)) :
    (G.baseChange ι).nsmul t' n x = baseChangePointOfBase ι (G.nsmul _ n (baseChangePointToBase ι
      x))
theorem

nsmul_coe_eq_comp_schemeNsmul

L64 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map.GoodReductionJacobian.RelativeGroupLaw.nsmul_coe_eq_comp_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_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
variable (ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R))
variable {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

baseChange_schemeNsmul_comp_fst_and_eq_pullback_map_aux

L74 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map.GoodReductionJacobian.RelativeGroupLaw.baseChange_schemeNsmul_comp_fst_and_eq_pullback_map_aux
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
variable {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
variable (ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R))
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
theorem baseChange_schemeNsmul_comp_fst_and_eq_pullback_map_aux (G : RelativeGroupLaw R f) (n : ℕ) :
    (G.baseChange ι).schemeNsmul n ≫ pullback.fst f ι = pullback.fst f ι ≫ G.schemeNsmul n ∧
    (G.baseChange ι).schemeNsmul n ≫ pullback.snd f ι = pullback.snd f ι ∧
    (G.baseChange ι).schemeNsmul n =
      pullback.map f ι f ι (G.schemeNsmul n) (𝟙 _) (𝟙 _)
        (by rw [Category.comp_id, G.schemeNsmul_over])
        (by rw [Category.comp_id, Category.id_comp]) := by
  have h1 : (G.baseChange ι).schemeNsmul n ≫ pullback.fst f ι = pullback.fst f ι ≫ G.schemeNsmul n
    := by
    change ((G.baseChange ι).nsmul (baseChangeStr ι f) n idPoint).1 ≫ _ = _
    rw [baseChange_nsmul, baseChangePointOfBase_coe, pullback.lift_fst,
      nsmul_coe_eq_comp_schemeNsmul,
      baseChangePointToBase_coe]
    simp only [Category.id_comp]
  have h2 : (G.baseChange ι).schemeNsmul n ≫ pullback.snd f ι = pullback.snd f ι :=
    (G.baseChange ι).schemeNsmul_over n
  refine ⟨h1, h2, ?_⟩
  apply pullback.hom_ext
  · rw [pullback.lift_fst, h1]
  · rw [pullback.lift_snd, h2, Category.comp_id]
theorem

baseChange_schemeNsmul_comp_fst_and_eq_pullback_map

L97 ↗
GoodReductionJacobian.RelativeGroupLaw.baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
Lean source · full declaration
theorem
  _root_.GoodReductionJacobian.RelativeGroupLaw.baseChange_schemeNsmul_comp_fst_and_eq_pullback_map
    {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
    (ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R))
    {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) (n : ℕ) :
    (G.baseChange ι).schemeNsmul n ≫ pullback.fst f ι = pullback.fst f ι ≫ G.schemeNsmul n ∧
    (G.baseChange ι).schemeNsmul n ≫ pullback.snd f ι = pullback.snd f ι ∧
    (G.baseChange ι).schemeNsmul n =
      pullback.map f ι f ι (G.schemeNsmul n) (𝟙 _) (𝟙 _)
        (by rw [Category.comp_id, G.schemeNsmul_over])
        (by rw [Category.comp_id, Category.id_comp]) :=
  GoodReductionJacobian.RelativeGroupLaw.baseChange_schemeNsmul_comp_fst_and_eq_pullback_map_aux ι
    G n

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