Module

AbelianMultiplicationAlgebraicPoints.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationAlgebraicPoints

3 declarations indexed from sourceView source ↗

Module documentation

Actual multiplication fibres as algebraic division points

The fibre point is converted to the additive group of actual algebraic points. Its division equation and monodromy translation are consequences of the original finite étale cover and group scheme law.

Imports3

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationFiberAction
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.AlgebraicPoints
Mathlib.Algebra.Algebra.Hom

Imported by2

def

multiplicationFiberAlgPoint

L34 ↗

GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberAlgPoint

Documentation

An actual multiplication-cover fibre point, expressed as an algebraic point.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory 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] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  {Ω : Type} [Field Ω] [IsSepClosed Ω] [Algebra K Ω]
omit [IsAlgClosed K] in

Lean source · statement

def multiplicationFiberAlgPoint
    (ξ : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap K Ω))) f)
    (n : ℕ+) (z : (FiniteEtale.fiber ξ.1).obj (G.multiplicationCover hc n)) :
    G.AlgPoints hc Ω

theorem

nsmul_multiplicationFiberAlgPoint

L44 ↗

GoodReductionJacobian.RelativeGroupLaw.nsmul_multiplicationFiberAlgPoint

Documentation

The algebraic point constructed from the fibre satisfies its actual division equation.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory 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] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  {Ω : Type} [Field Ω] [IsSepClosed Ω] [Algebra K Ω]
omit [IsAlgClosed K] in

Lean source · statement

theorem nsmul_multiplicationFiberAlgPoint
    (ξ : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap K Ω))) f)
    (n : ℕ+) (z : (FiniteEtale.fiber ξ.1).obj (G.multiplicationCover hc n)) :
    (n : ℕ) • G.multiplicationFiberAlgPoint hc ξ n z = AlgPoints.ofPoint ξ

theorem

multiplicationFiberAlgPoint_smul

L78 ↗

GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberAlgPoint_smul

Documentation

Actual monodromy on the fibre is addition of the actual torsion point, also after passage to the algebraic-point group over the geometric field.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory 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] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  {Ω : Type} [Field Ω] [IsSepClosed Ω] [Algebra K Ω]

Lean source · statement

theorem multiplicationFiberAlgPoint_smul
    (ξ : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap K Ω))) f)
    (n : ℕ+)
    (τ : FiniteEtale.fiber ξ.1 ≅ FiniteEtale.fiber (G.one (𝟙 (Spec (.of K)))).1)
    (g : π₁ᵉᵗ(ξ.1))
    (z : (FiniteEtale.fiber ξ.1).obj (G.multiplicationCover hc n)) :
    G.multiplicationFiberAlgPoint hc ξ n (g • z) =
      G.multiplicationFiberAlgPoint hc ξ n z +
        AlgPoints.map (L := G) (hc := hc) (T := K) (T' := Ω) (Algebra.ofId K Ω)
          (G.multiplicationMonodromy hc n (continuousConjAut τ g)).1

Module documentation

Actual multiplication fibres as algebraic division points

Declarations

multiplicationFiberAlgPoint

nsmul_multiplicationFiberAlgPoint

multiplicationFiberAlgPoint_smul