Module

AbelianMultiplicationDegreeLift.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationDegreeLift

2 declarations indexed from sourceView source ↗

Module documentation

Lifting multiplication by the degree through a connected cover

In every characteristic, a connected finite étale cover of a proper smooth geometrically connected group is dominated by multiplication by its actual geometric fibre cardinality. Commutativity of the fundamental group makes its finite monodromy image act freely and transitively; its order is therefore the degree, without replacing the degree by a factorial.

Imports7

Nyll.EtaleFundamentalGroups.GeometricFiber.ProperGroupScheme
Nyll.EtaleFundamentalGroups.GeometricFiber.Functoriality
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.EtaleFundamentalGroups.FiniteEtale.TrivialBaseChangeAlgebra
Mathlib.CategoryTheory.Galois.Full
Mathlib.CategoryTheory.Galois.Topology
Mathlib.GroupTheory.OrderOfElement

Imported by2

theorem

pullback_fixed_of_pointed

L32 ↗

GoodReductionJacobian.RelativeGroupLaw.pullback_fixed_of_pointed

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
    {X Y : Scheme} {K : Type} [Field K] [IsSepClosed K]
    (a : X ⟶ Y) (x : Spec (.of K) ⟶ X) (y : Spec (.of K) ⟶ Y)
    (h : x ≫ a = y) (W : FiniteEtale Y)
    (hf : ∀ (g : π₁ᵉᵗ(x)) (w : (fiber y).obj W),
      pointedFundamentalGroupHom a x y h g • w = w) :
    ∀ (g : π₁ᵉᵗ(x)) (w : (fiber x).obj ((FiniteEtale.pullback a).obj W)), g • w = w

theorem

exists_schemeNsmul_lift_degree

L49 ↗

GoodReductionJacobian.RelativeGroupLaw.exists_schemeNsmul_lift_degree

Documentation

Multiplication by the actual degree lifts to the original connected cover. No characteristic restriction or isogeny classification of the cover is assumed.

Source context 5 commands