Module

GaloisDomination.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GaloisDomination

1 declaration indexed from sourceView source ↗

Module documentation

Domination by finite-etale Galois covers

Every connected finite-etale cover of a connected scheme is dominated by a Galois object. This file specializes the abstract Galois-category theorem to finite-etale schemes, choosing a geometric fiber functor canonically from an arbitrary point of the base.

Imports2

Mathlib.CategoryTheory.Galois.Decomposition
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected

Imported by2

lemma

exists_galois_domination

L32 ↗

AlgebraicGeometry.FiniteEtale.exists_galois_domination

Documentation

A connected finite-etale cover is dominated by a finite-etale Galois cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]

Lean source · statement

lemma exists_galois_domination (W : FiniteEtale X)
    [ConnectedSpace W.left] :
    ∃ (A : FiniteEtale X) (_ : A ⟶ W), IsGalois A

Module documentation

Domination by finite-etale Galois covers

Declarations

exists_galois_domination