NYLL
Module

AbelianMultiplicationTransitions.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationTransitions
5 declarations indexed from sourceView source ↗

Module documentation

Multiplication covers and Tate transitions

Multiplication by m gives an actual morphism from the (n*m) multiplication cover to the n multiplication cover. Under the identification of their geometric fibres with torsion points, this morphism induces the multiplication transition used in the full Tate module.

Imports9
Imported by4

Declarations

theorem

nsmul_nsmul_point

L37 ↗
GoodReductionJacobian.RelativeGroupLaw.nsmul_nsmul_point
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem nsmul_nsmul_point {T : Scheme.{0}}
    (t : T ⟶ Spec (CommRingCat.of K)) (n m : ℕ) (x : SchemeHomOver t f) :
    G.nsmul t n (G.nsmul t m x) = G.nsmul t (m * n) x
theorem

schemeNsmul_comp_schemeNsmul

L50 ↗
GoodReductionJacobian.RelativeGroupLaw.schemeNsmul_comp_schemeNsmul
Documentation

Composition of the actual multiplication morphisms multiplies their indices.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem schemeNsmul_comp_schemeNsmul (m n : ℕ) :
    G.schemeNsmul m ≫ G.schemeNsmul n = G.schemeNsmul (m * n)
def

multiplicationCoverTransition

L60 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverTransition
Documentation

The actual multiplication map [m] between the multiplication covers.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def multiplicationCoverTransition [CharZero K] [IsProper f] [Smooth f] (n m : ℕ+) :
    G.multiplicationCover hc (n * m) ⟶ G.multiplicationCover hc n
theorem

multiplicationCoverFiberEquivTorsion_toPoint

L69 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverFiberEquivTorsion_toPoint
Documentation

The fibre comparison identifies the same actual scheme point, including the transport from the scalar identity to the scheme identity.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem multiplicationCoverFiberEquivTorsion_toPoint
    [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f] (n : ℕ+)
    (x : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (G.multiplicationCover hc n)) :
    (AlgPoints.toPoint (G.multiplicationCoverFiberEquivTorsion hc n x).1).1 =
      (FiniteEtale.fiberObjEquivHom (G.one (𝟙 (Spec (CommRingCat.of K)))).1
        (G.multiplicationCover hc n) x).left
theorem

multiplicationCoverFiberEquivTorsion_transition

L102 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverFiberEquivTorsion_transition
Documentation

The actual geometric-fibre map of [m] is exactly the full Tate transition.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem multiplicationCoverFiberEquivTorsion_transition
    [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f] (n m : ℕ+)
    (x : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (G.multiplicationCover hc (n * m))) :
    G.multiplicationCoverFiberEquivTorsion hc n
        ((FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).map
          (G.multiplicationCoverTransition hc n m) x) =
      ProCGroups.torsionTransition (G.AlgPoints hc K) n m
        (G.multiplicationCoverFiberEquivTorsion hc (n * m) x)

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