NYLL
Module

AbelianUnitTorsionFiber.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianUnitTorsionFiber
10 declarations indexed from sourceView source ↗

Module documentation

Actual torsion fibres of invertible multiplication covers

The indices form the multiplicative submonoid of positive integers invertible in the ground field. The actual fibre comparison and its transition formula work in arbitrary characteristic over a separably closed field.

Imports9
Imported by5

Declarations

def

unitIndices

L36 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.unitIndices
Documentation

The positive multiplication indices invertible in the ground field.

Source context 6 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
Lean source · full declaration
def unitIndices (K : Type) [Field K] : Submonoid ℕ+ where
  carrier := {n | IsUnit ((n : ℕ) : K)}
  one_mem' := by
    change IsUnit ((1 : ℕ) : K)
    rw [Nat.cast_one]
    exact isUnit_one
  mul_mem' := by
    intro a b ha hb
    change IsUnit (((a : ℕ) * (b : ℕ) : ℕ) : K)
    rw [Nat.cast_mul]
    exact ha.mul hb
def

cover

L52 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.cover
Documentation

The actual multiplication cover at an allowed index.

Source context 7 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def cover [IsProper f] [Smooth f] (n : unitIndices K) : FiniteEtale A
theorem

isConnected_cover

L56 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.isConnected_cover
Documentation

The allowed multiplication cover is connected when the group is geometrically connected.

Source context 7 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem isConnected_cover [IsProper f] [Smooth f] [GeometricallyConnected f]
    (n : unitIndices K) : IsConnected (cover G hc n)
def

pointOverEquivKernelSection

L60 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.pointOverEquivKernelSection
Source context 7 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (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

fiberEquivTorsion

L78 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fiberEquivTorsion
Documentation

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

Source context 7 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def fiberEquivTorsion [IsSepClosed K] [IsProper f] [Smooth f]
    (n : unitIndices K) :
    (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
        (cover G hc n) ≃ ProCGroups.torsionLevel (G.AlgPoints hc K) n.1
def

transition

L92 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.transition
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 CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def transition [IsProper f] [Smooth f] (n m : unitIndices K) :
    cover G hc (n * m) ⟶ cover G hc n
theorem

fiberEquivTorsion_toPoint

L101 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fiberEquivTorsion_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 CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem fiberEquivTorsion_toPoint
    [IsSepClosed K] [IsProper f] [Smooth f] (n : unitIndices K)
    (x : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (cover G hc n)) :
    (AlgPoints.toPoint (fiberEquivTorsion G hc n x).1).1 =
      (FiniteEtale.fiberObjEquivHom (G.one (𝟙 (Spec (CommRingCat.of K)))).1
        (cover G hc n) x).left
theorem

fiberEquivTorsion_transition

L134 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fiberEquivTorsion_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 CategoryTheory.PreGaloisCategory
open AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem fiberEquivTorsion_transition
    [IsSepClosed K] [IsProper f] [Smooth f] (n m : unitIndices K)
    (x : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (cover G hc (n * m))) :
    fiberEquivTorsion G hc n
        ((FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).map
          (transition G hc n m) x) =
      ProCGroups.torsionTransition (G.AlgPoints hc K) n.1 m.1
        (fiberEquivTorsion G hc (n * m) x)
def

translation

L160 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.translation
Documentation

Translation by an actual torsion section is a deck automorphism of the allowed cover.

Source context 7 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def translation [IsProper f] [Smooth f] (n : unitIndices K)
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f)
    (ht : G.IsTorsionPoint (𝟙 _) (n.1 : ℕ) t) : Aut (cover G hc n)
theorem

finite_torsionLevel

L167 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.finite_torsionLevel
Documentation

Every allowed actual torsion group is finite over a separably closed field.

Source context 7 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_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem finite_torsionLevel [IsSepClosed K] [IsProper f] [Smooth f]
    (n : unitIndices K) : Finite (ProCGroups.torsionLevel (G.AlgPoints hc K) n.1)

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