NYLL
Module

AbelianMultiplicationTranslations.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationTranslations
9 declarations indexed from sourceView source ↗

Module documentation

Torsion translations of multiplication covers

Translation by an actual torsion section preserves the multiplication morphism. Its inverse is translation by the inverse section, so it gives an automorphism of the actual finite étale multiplication cover. On relative scheme points its action is the original group law, with no comparison of actions assumed.

Imports8
Imported by4

Declarations

theorem

point_comp_translate

L40 ↗
GoodReductionJacobian.RelativeGroupLaw.point_comp_translate
Documentation

Evaluation of translation on any relative point is multiplication by the same section pulled back to the test scheme.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
theorem point_comp_translate {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of K))
    (x : SchemeHomOver s f) (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f) :
    x.1 ≫ G.translate t =
      (G.mul s x (GoodReductionJacobian.schemeHomOverComp s (Category.comp_id s) t)).1
theorem

translate_comp_translate

L59 ↗
GoodReductionJacobian.RelativeGroupLaw.translate_comp_translate
Documentation

Composition of two translations is translation by their product.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
theorem translate_comp_translate
    (t u : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f) :
    G.translate t ≫ G.translate u = G.translate (G.mul (𝟙 _) t u)
def

translateIso

L72 ↗
GoodReductionJacobian.RelativeGroupLaw.translateIso
Documentation

Translation is an actual scheme isomorphism, with inverse translation by the inverse section.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · full declaration
def translateIso (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f) : A ≅ A where
  hom := G.translate t
  inv := G.translate (G.inv (𝟙 _) t)
  hom_inv_id := by
    rw [G.translate_comp_translate, G.mul_inv_cancel, G.translate_one]
  inv_hom_id := by
    rw [G.translate_comp_translate, G.inv_mul_cancel, G.translate_one]
theorem

translate_comp_schemeNsmul

L81 ↗
GoodReductionJacobian.RelativeGroupLaw.translate_comp_schemeNsmul
Documentation

Translation by an actual n-torsion section preserves the actual [n] map.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
theorem translate_comp_schemeNsmul (hc : G.IsCommutative) (n : ℕ)
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f)
    (ht : G.IsTorsionPoint (𝟙 _) n t) :
    G.translate t ≫ G.schemeNsmul n = G.schemeNsmul n
def

multiplicationCoverTranslation

L97 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverTranslation
Documentation

A torsion translation gives a deck automorphism of the actual finite étale multiplication cover.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
def multiplicationCoverTranslation (hc : G.IsCommutative) [CharZero K]
    [IsProper f] [Smooth f] (n : ℕ+)
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f)
    (ht : G.IsTorsionPoint (𝟙 _) (n : ℕ) t) :
    Aut (G.multiplicationCover hc n)
theorem

multiplicationCoverTranslation_hom_left

L107 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverTranslation_hom_left
Documentation

The underlying scheme map of the deck automorphism is the original translation morphism.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
theorem multiplicationCoverTranslation_hom_left (hc : G.IsCommutative) [CharZero K]
    [IsProper f] [Smooth f] (n : ℕ+)
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f)
    (ht : G.IsTorsionPoint (𝟙 _) (n : ℕ) t) :
    (G.multiplicationCoverTranslation hc n t ht).hom.left = G.translate t
theorem

point_comp_multiplicationCoverTranslation

L116 ↗
GoodReductionJacobian.RelativeGroupLaw.point_comp_multiplicationCoverTranslation
Documentation

On the actual underlying scheme points, a torsion deck translation acts by the original group law. This computes its action before any fibre-to-torsion comparison is applied.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
theorem point_comp_multiplicationCoverTranslation (hc : G.IsCommutative) [CharZero K]
    [IsProper f] [Smooth f] (n : ℕ+)
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f)
    (ht : G.IsTorsionPoint (𝟙 _) (n : ℕ) t)
    {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of K)) (x : SchemeHomOver s f) :
    x.1 ≫ (G.multiplicationCoverTranslation hc n t ht).hom.left =
      (G.mul s x (GoodReductionJacobian.schemeHomOverComp s (Category.comp_id s) t)).1
def

multiplicationFiberPoint

L127 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberPoint
Documentation

The point of the original group scheme underlying an actual geometric point in a multiplication-cover fibre.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
def multiplicationFiberPoint (hc : G.IsCommutative) [CharZero K]
    [IsProper f] [Smooth f] {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ A) (n : ℕ+)
    (z : (FiniteEtale.fiber ξ).obj (G.multiplicationCover hc n)) :
    SchemeHomOver (ξ ≫ f) f
theorem

multiplicationFiberPoint_map_translation

L147 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationFiberPoint_map_translation
Documentation

The action of a torsion deck translation on the actual geometric fibre is pointwise multiplication by the torsion section.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open RelativeGroupLaw_surjective_schemeNsmul_of_flat_of_field.GoodReductionJacobian.RelativeGroupLaw
  (nsmul_mul)
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f)
Lean source · statement
theorem multiplicationFiberPoint_map_translation (hc : G.IsCommutative) [CharZero K]
    [IsProper f] [Smooth f] {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ A) (n : ℕ+)
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f)
    (ht : G.IsTorsionPoint (𝟙 _) (n : ℕ) t)
    (z : (FiniteEtale.fiber ξ).obj (G.multiplicationCover hc n)) :
    G.multiplicationFiberPoint hc ξ n
        ((FiniteEtale.fiber ξ).map (G.multiplicationCoverTranslation hc n t ht).hom z) =
      G.mul (ξ ≫ f) (G.multiplicationFiberPoint hc ξ n z)
        (GoodReductionJacobian.schemeHomOverComp (ξ ≫ f) (Category.comp_id (ξ ≫ f)) t)

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