NYLL
Module

AbelianMultiplicationCofinality.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationCofinality
2 declarations indexed from sourceView source ↗

Module documentation

Cofinality of multiplication covers

Multiplication by the order of a finite fibre permutation group kills its monodromy action. The actual pullback cover consequently has a section, constructed by fullness of the finite monodromy functor. This gives an actual morphism from a multiplication cover to every connected finite étale cover of the proper smooth group scheme.

Imports12
Imported by2

Declarations

theorem

pullback_fixed_of_pointed_fixed

L37 ↗
GoodReductionJacobian.RelativeGroupLaw.pullback_fixed_of_pointed_fixed
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem pullback_fixed_of_pointed_fixed
    {X Y : Scheme} {K : Type} [Field K] [IsSepClosed K]
    (f : X ⟶ Y) (x : Spec (.of K) ⟶ X) (y : Spec (.of K) ⟶ Y)
    (h : x ≫ f = y) (W : FiniteEtale Y)
    (hf : ∀ (g : π₁ᵉᵗ(x)) (w : (fiber y).obj W),
      pointedFundamentalGroupHom f x y h g • w = w) :
    ∀ (g : π₁ᵉᵗ(x)) (w : (fiber x).obj ((FiniteEtale.pullback f).obj W)),
      g • w = w
theorem

exists_multiplicationCover_hom

L56 ↗
GoodReductionJacobian.RelativeGroupLaw.exists_multiplicationCover_hom
Documentation

Every connected finite étale cover is dominated by an actual positive multiplication cover. No classification of the given cover as an isogeny is assumed.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem exists_multiplicationCover_hom (W : FiniteEtale A) [IsConnected W] :
    ∃ n : ℕ+, Nonempty (G.multiplicationCover hc n ⟶ W)

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