Module

AbelianMultiplicationFiberAction.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationFiberAction

4 declarations indexed from sourceView source ↗

Module documentation

Actual multiplication-cover action at an arbitrary geometric point

Transport through a path to the unit identifies actual monodromy with translation by the same torsion point on every geometric fibre. Naturality against the deck translation proves the comparison; it is not an input.

Imports5

Imported by2

theorem

multiplicationFiber_smul_eq_translation

L38 ↗

GoodReductionJacobian.RelativeGroupLaw.multiplicationFiber_smul_eq_translation

Documentation

At any geometric point, actual monodromy is the deck translation whose torsion parameter is obtained by transport to the unit.

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 Ω]
omit [IsSepClosed Ω] in

Lean source · statement

theorem multiplicationFiber_smul_eq_translation
    (ξ : Spec (.of Ω) ⟶ A) (n : ℕ+)
    (τ : FiniteEtale.fiber ξ ≅ FiniteEtale.fiber (G.one (𝟙 (Spec (.of K)))).1)
    (g : π₁ᵉᵗ(ξ))
    (z : (FiniteEtale.fiber ξ).obj (G.multiplicationCover hc n)) :
    g • z = (FiniteEtale.fiber ξ).map
      (G.torsionDeckTranslation hc n
        (G.multiplicationMonodromy hc n (continuousConjAut τ g))).hom z

theorem

multiplicationFiberPoint_smul

L70 ↗

GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberPoint_smul

Documentation

The transported monodromy acts on the actual point of the group scheme by its actual group law, at the chosen geometric point.

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 Ω]

Lean source · statement

theorem multiplicationFiberPoint_smul
    (ξ : Spec (.of Ω) ⟶ A) (n : ℕ+)
    (τ : FiniteEtale.fiber ξ ≅ FiniteEtale.fiber (G.one (𝟙 (Spec (.of K)))).1)
    (g : π₁ᵉᵗ(ξ))
    (z : (FiniteEtale.fiber ξ).obj (G.multiplicationCover hc n)) :
    G.multiplicationFiberPoint hc ξ n (g • z) =
      G.mul (ξ ≫ f) (G.multiplicationFiberPoint hc ξ n z)
        (GoodReductionJacobian.schemeHomOverComp (ξ ≫ f) (Category.comp_id (ξ ≫ f))
          (G.torsionPointSection hc n
            (G.multiplicationMonodromy hc n (continuousConjAut τ g))))

theorem

multiplicationFiberPoint_nsmul

L89 ↗

GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberPoint_nsmul

Documentation

Every point of the actual multiplication-cover fibre is an actual division point of the chosen geometric 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 Ω]
omit [IsAlgClosed K] in

Lean source · statement

theorem multiplicationFiberPoint_nsmul
    (ξ : Spec (.of Ω) ⟶ A) (n : ℕ+)
    (z : (FiniteEtale.fiber ξ).obj (G.multiplicationCover hc n)) :
    G.nsmul (ξ ≫ f) (n : ℕ) (G.multiplicationFiberPoint hc ξ n z) =
      (⟨ξ, rfl⟩ : SchemeHomOver (ξ ≫ f) f)

theorem

multiplicationFiberPoint_field_action

L100 ↗

GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberPoint_field_action

Documentation

At a field-valued point, the actual Galois displacement of a division point is the torsion point obtained from actual multiplication monodromy.

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 Ω]

Lean source · full declaration

theorem multiplicationFiberPoint_field_action
    {L : Type} [Field L] [Algebra L Ω] [IsSepClosure L Ω]
    (j : Spec (.of L) ⟶ A) (n : ℕ+)
    (τ : FiniteEtale.fiber
        (Spec.map (CommRingCat.ofHom (algebraMap L Ω)) ≫ j) ≅
      FiniteEtale.fiber (G.one (𝟙 (Spec (.of K)))).1)
    (σ : Ω ≃ₐ[L] Ω)
    (z : (FiniteEtale.fiber
      (Spec.map (CommRingCat.ofHom (algebraMap L Ω)) ≫ j)).obj
        (G.multiplicationCover hc n)) :
    let xi := Spec.map (CommRingCat.ofHom (algebraMap L Ω))
    let g := FiniteEtale.fundamentalGroupHom j xi
      (toAut (FiniteEtale.fiber xi) (Ω ≃ₐ[L] Ω) σ)
    Spec.map (CommRingCat.ofHom σ.toRingHom) ≫
      (G.multiplicationFiberPoint hc (xi ≫ j) n z).1 =
      (G.mul ((xi ≫ j) ≫ f) (G.multiplicationFiberPoint hc (xi ≫ j) n z)
        (GoodReductionJacobian.schemeHomOverComp ((xi ≫ j) ≫ f)
          (Category.comp_id ((xi ≫ j) ≫ f))
          (G.torsionPointSection hc n
            (G.multiplicationMonodromy hc n (continuousConjAut τ g))))).1 := by
  intro xi g
  have hfield := FiniteEtale.fundamentalGroupHom_field_fiberLift j
    (G.multiplicationCover hc n) σ z
  change (G.multiplicationFiberPoint hc (xi ≫ j) n (g • z)).1 =
    Spec.map (CommRingCat.ofHom σ.toRingHom) ≫
      (G.multiplicationFiberPoint hc (xi ≫ j) n z).1 at hfield
  exact hfield.symm.trans (congrArg Subtype.val
    (G.multiplicationFiberPoint_smul hc (xi ≫ j) n τ g z))

Module documentation

Actual multiplication-cover action at an arbitrary geometric point

Declarations

multiplicationFiber_smul_eq_translation

multiplicationFiberPoint_smul

multiplicationFiberPoint_nsmul

multiplicationFiberPoint_field_action