Module

AbelianUnitMultiplicationCover.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianUnitMultiplicationCover

4 declarations indexed from sourceView source ↗

Module documentation

Multiplication covers of degree invertible in the ground field

The actual multiplication map is finite étale whenever its integer is a unit. Combined with the degree lifting theorem, this supplies a multiplication cover over every connected finite étale cover whose degree is invertible, in arbitrary characteristic.

Imports5

Imported by2

theorem

isFiniteEtale_schemeNsmul_of_isUnit

L36 ↗

GoodReductionJacobian.RelativeGroupLaw.isFiniteEtale_schemeNsmul_of_isUnit

Documentation

Multiplication by an invertible integer is an actual finite étale morphism.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
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} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
include hc in

Lean source · statement

theorem isFiniteEtale_schemeNsmul_of_isUnit (n : ℕ) (hn : IsUnit (n : K)) :
    IsFiniteEtale (G.schemeNsmul n)

def

unitMultiplicationCover

L52 ↗

GoodReductionJacobian.RelativeGroupLaw.unitMultiplicationCover

Documentation

The original multiplication morphism bundled as a finite étale cover.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
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} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · statement

def unitMultiplicationCover (n : ℕ) (hn : IsUnit (n : K)) : FiniteEtale A

theorem

isConnected_unitMultiplicationCover

L56 ↗

GoodReductionJacobian.RelativeGroupLaw.isConnected_unitMultiplicationCover

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
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} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · statement

theorem isConnected_unitMultiplicationCover [GeometricallyConnected f]
    (n : ℕ) (hn : IsUnit (n : K)) : IsConnected (G.unitMultiplicationCover hc n hn)

theorem

nonempty_unitMultiplicationCover_hom

L65 ↗

GoodReductionJacobian.RelativeGroupLaw.nonempty_unitMultiplicationCover_hom

Documentation

Every connected finite étale cover of invertible degree is dominated by the multiplication cover of that same degree, without a characteristic-zero hypothesis.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
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} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · statement

theorem nonempty_unitMultiplicationCover_hom [IsSepClosed K] [GeometricallyConnected f]
    (W : FiniteEtale A) [IsConnected W]
    (hn : IsUnit ((Nat.card ((fiber (G.one (𝟙 (Spec (.of K)))).1).obj W)) : K)) :
    Nonempty (G.unitMultiplicationCover hc
      (Nat.card ((fiber (G.one (𝟙 (Spec (.of K)))).1).obj W)) hn ⟶ W)

Module documentation

Multiplication covers of degree invertible in the ground field

Declarations

isFiniteEtale_schemeNsmul_of_isUnit

unitMultiplicationCover

isConnected_unitMultiplicationCover

nonempty_unitMultiplicationCover_hom