Module

Injectivity.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.Injectivity

1 declaration indexed from sourceView source ↗

Module documentation

Injectivity from essential surjectivity of finite-etale pullback

If pullback of finite-etale covers along a scheme morphism is essentially surjective, then the induced homomorphism on automorphism groups of geometric fiber functors is injective. The categorical result requires no fullness assumption.

Imports2

Imported by5

theorem

fundamentalGroupHom_injective_of_pullback_essSurj

L33 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_injective_of_pullback_essSurj

Documentation

Essential surjectivity of finite-etale pullback implies injectivity of the induced homomorphism on etale fundamental groups.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]

Lean source · statement

theorem fundamentalGroupHom_injective_of_pullback_essSurj
    (f : X ⟶ Y) [(pullback f).EssSurj]
    (ξ : Spec (.of Ω) ⟶ X) :
    Function.Injective (fundamentalGroupHom f ξ)

Module documentation

Injectivity from essential surjectivity of finite-etale pullback

Declarations

fundamentalGroupHom_injective_of_pullback_essSurj