NYLL
Module

RepresentsRelSubPic_kerPoints_mul_mem_and_comp_mem.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_kerPoints_mul_mem_and_comp_mem
5 declarations indexed from sourceView source ↗

Module documentation

Multiplication and endomorphisms of points reducing to the identity

Naturality of a relative group law makes its reduction kernel closed under multiplication. Every multiplicative endomorphism preserves that kernel.

Imports14
Imported by3

Declarations

theorem

comp_eq_one_iff

L70 ↗
JacobianVarieties.Picard.Proofs.KernelPointMultiplication.GoodReductionJacobian.RelativeGroupLaw.comp_eq_one_iff
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.KernelPointMultiplication
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
section ReducesToOne
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (L : RelativeGroupLaw R f)
  {T T₀ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₀ : T₀ ⟶ Spec (CommRingCat.of R)}
  (r : T₀ ⟶ T) (hr : r ≫ t = t₀)
Lean source · statement
theorem comp_eq_one_iff (x : SchemeHomOver t f) :
    r ≫ x.1 = (L.one t₀).1 ↔ GoodReductionJacobian.schemeHomOverComp r hr x = L.one t₀
theorem

comp_mul_eq_one_of_comp_eq_one

L75 ↗
JacobianVarieties.Picard.Proofs.KernelPointMultiplication.GoodReductionJacobian.RelativeGroupLaw.comp_mul_eq_one_of_comp_eq_one
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.KernelPointMultiplication
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
section ReducesToOne
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (L : RelativeGroupLaw R f)
  {T T₀ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₀ : T₀ ⟶ Spec (CommRingCat.of R)}
  (r : T₀ ⟶ T) (hr : r ≫ t = t₀)
include hr in
Lean source · statement
theorem comp_mul_eq_one_of_comp_eq_one (x y : SchemeHomOver t f)
    (hx : r ≫ x.1 = (L.one t₀).1) (hy : r ≫ y.1 = (L.one t₀).1) :
    r ≫ (L.mul t x y).1 = (L.one t₀).1
theorem

hom_one

L81 ↗
JacobianVarieties.Picard.Proofs.KernelPointMultiplication.GoodReductionJacobian.RelativeGroupLaw.hom_one
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.KernelPointMultiplication
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
section ReducesToOne
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (L : RelativeGroupLaw R f)
  {T T₀ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₀ : T₀ ⟶ Spec (CommRingCat.of R)}
  (r : T₀ ⟶ T) (hr : r ≫ t = t₀)
Lean source · statement
theorem hom_one (φ : SchemeHomOver f f)
    (hφ : ∀ {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver s f),
      NeronModelInfra.schemeHomOverComp (L.mul s x y) φ =
        L.mul s (NeronModelInfra.schemeHomOverComp x φ) (NeronModelInfra.schemeHomOverComp y φ))
    {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) :
    NeronModelInfra.schemeHomOverComp (L.one s) φ = L.one s
theorem

comp_comp_hom_eq_one_of_comp_eq_one

L95 ↗
JacobianVarieties.Picard.Proofs.KernelPointMultiplication.GoodReductionJacobian.RelativeGroupLaw.comp_comp_hom_eq_one_of_comp_eq_one
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.KernelPointMultiplication
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
section ReducesToOne
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (L : RelativeGroupLaw R f)
  {T T₀ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₀ : T₀ ⟶ Spec (CommRingCat.of R)}
  (r : T₀ ⟶ T) (hr : r ≫ t = t₀)
Lean source · statement
theorem comp_comp_hom_eq_one_of_comp_eq_one (φ : SchemeHomOver f f)
    (hφ : ∀ {S : Scheme.{u}} (s : S ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver s f),
      NeronModelInfra.schemeHomOverComp (L.mul s x y) φ =
        L.mul s (NeronModelInfra.schemeHomOverComp x φ) (NeronModelInfra.schemeHomOverComp y φ))
    (x : SchemeHomOver t f) (hx : r ≫ x.1 = (L.one t₀).1) :
    r ≫ (x.1 ≫ φ.1) = (L.one t₀).1
theorem

kerPoints_mul_mem_and_comp_mem

L108 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.kerPoints_mul_mem_and_comp_mem
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.KernelPointMultiplication
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
Lean source · full declaration
theorem _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.kerPoints_mul_mem_and_comp_mem
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) (A : Type u) [CommRing A] [Algebra R A] :
    let L := RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h
    let tε := Scheme.TwoAffineOpenCover.specMap R (DualNumber A)
    let t₀ := Scheme.TwoAffineOpenCover.specMap R A
    (∀ x y : SchemeHomOver tε D.toBase,
        dualNumberReduction R A ≫ x.1 = (L.one t₀).1 →
          dualNumberReduction R A ≫ y.1 = (L.one t₀).1 →
          dualNumberReduction R A ≫ (L.mul tε x y).1 = (L.one t₀).1) ∧
    (∀ (φ : SchemeHomOver D.toBase D.toBase),
        (∀ {T : Scheme.{u}} (s : T ⟶ Spec (.of R)) (x y : SchemeHomOver s D.toBase),
          NeronModelInfra.schemeHomOverComp (L.mul s x y) φ =
            L.mul s (NeronModelInfra.schemeHomOverComp x φ)
              (NeronModelInfra.schemeHomOverComp y φ)) →
        ∀ x : SchemeHomOver tε D.toBase, dualNumberReduction R A ≫ x.1 = (L.one t₀).1 →
          dualNumberReduction R A ≫ (x.1 ≫ φ.1) = (L.one t₀).1) := by
  intro L tε t₀
  refine ⟨fun x y hx hy => ?_, fun φ hφ x hx => ?_⟩
  · exact GoodReductionJacobian.RelativeGroupLaw.comp_mul_eq_one_of_comp_eq_one L
      (dualNumberReduction R A)
      (dualNumberReduction_comp_specMap R A) x y hx hy
  · exact GoodReductionJacobian.RelativeGroupLaw.comp_comp_hom_eq_one_of_comp_eq_one L
      (dualNumberReduction R A)
      φ hφ x hx

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