NYLL
Module

AbelianMultiplicationCover.lean

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

Module documentation

Multiplication covers and their actual torsion fibres

For a proper smooth commutative relative group law in characteristic zero, multiplication by a positive integer is finite étale. Geometric connectedness makes this an actual connected cover. At its unit point, its geometric fibre is identified with the actual torsion subgroup of algebraic points, using the pullback universal property and the existing scheme-kernel comparison.

Imports14
Imported by7

Declarations

theorem

isFiniteEtale_schemeNsmul_of_charZero

L47 ↗
GoodReductionJacobian.RelativeGroupLaw.isFiniteEtale_schemeNsmul_of_charZero
Documentation

The actual positive multiplication map is finite étale; its relative dimension is obtained from smoothness and the group law.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
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)
include hc in
Lean source · statement
theorem isFiniteEtale_schemeNsmul_of_charZero [CharZero K] [IsProper f] [Smooth f]
    (n : ℕ+) : IsFiniteEtale (G.schemeNsmul (n : ℕ))
def

multiplicationCover

L67 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCover
Documentation

The finite étale cover whose actual scheme morphism is multiplication by n.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
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 multiplicationCover [CharZero K] [IsProper f] [Smooth f] (n : ℕ+) : FiniteEtale A
theorem

isConnected_multiplicationCover

L73 ↗
GoodReductionJacobian.RelativeGroupLaw.isConnected_multiplicationCover
Documentation

Geometric connectedness of the group scheme makes its multiplication cover connected.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
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 isConnected_multiplicationCover [CharZero K] [IsProper f] [Smooth f]
    [GeometricallyConnected f] (n : ℕ+) : IsConnected (G.multiplicationCover hc n)
def

pointOverEquivKernelSection

L80 ↗
GoodReductionJacobian.RelativeGroupLaw.pointOverEquivKernelSection
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
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 · full declaration
def pointOverEquivKernelSection (a : A ⟶ A) (e : Spec (CommRingCat.of K) ⟶ A) :
    SchemeHomOver e a ≃ SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) (pullback.snd a e) where
  toFun x := ⟨pullback.lift x.1 (𝟙 _) (x.2.trans (Category.id_comp e).symm),
    pullback.lift_snd _ _ _⟩
  invFun z := ⟨z.1 ≫ pullback.fst a e, by
    rw [Category.assoc, pullback.condition, ← Category.assoc, z.2, Category.id_comp]⟩
  left_inv x := by
    apply Subtype.ext
    exact pullback.lift_fst _ _ _
  right_inv z := by
    apply Subtype.ext
    apply pullback.hom_ext
    · exact pullback.lift_fst _ _ _
    · rw [pullback.lift_snd]
      exact z.2.symm
def

multiplicationCoverFiberEquivTorsion

L98 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverFiberEquivTorsion
Documentation

The actual geometric fibre at the unit of the multiplication cover is the actual torsion subgroup of algebraic points.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
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 multiplicationCoverFiberEquivTorsion [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f]
    (n : ℕ+) :
    (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
        (G.multiplicationCover hc n) ≃ ProCGroups.torsionLevel (G.AlgPoints hc K) n

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