Module

PullbackEquivalence.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.PullbackEquivalence

3 declarations indexed from sourceView source ↗

Module documentation

Fundamental groups under an equivalence of finite étale covers

An equivalence on finite étale covers makes the canonical map on fundamental groups bijective. Its inverse is continuous because these automorphism groups are compact Hausdorff. This gives the fundamental-group conclusion of Stacks Project, Tag 0BQA, for connected schemes.

Imports3

Nyll.EtaleFundamentalGroups.GaloisCategories.Surjectivity
Nyll.EtaleFundamentalGroups.GeometricFiber.Injectivity
Mathlib.CategoryTheory.Adjunction.Limits

Imported by18

theorem

fundamentalGroupHom_bijective_of_pullback_isEquivalence

L35 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_bijective_of_pullback_isEquivalence

Documentation

An equivalence on finite étale covers makes the induced group map bijective.

Source context 7 commands

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

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

Lean source · statement

theorem fundamentalGroupHom_bijective_of_pullback_isEquivalence
    (f : X ⟶ Y) [(pullback f).IsEquivalence] (ξ : Spec (.of Ω) ⟶ X) :
    Function.Bijective (fundamentalGroupHom f ξ)

def

fundamentalGroupEquivOfPullbackEquivalence

L48 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfPullbackEquivalence

Documentation

The canonical map on fundamental groups is an isomorphism of topological groups whenever pullback is an equivalence on finite étale covers.

Source context 7 commands

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

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

Lean source · full declaration

def fundamentalGroupEquivOfPullbackEquivalence
    (f : X ⟶ Y) [(pullback f).IsEquivalence] (ξ : Spec (.of Ω) ⟶ X) :
    π₁ᵉᵗ(ξ) ≃ₜ* π₁ᵉᵗ(ξ ≫ f) where
  toMulEquiv := MulEquiv.ofBijective (fundamentalGroupHom f ξ)
    (fundamentalGroupHom_bijective_of_pullback_isEquivalence f ξ)
  continuous_toFun := (fundamentalGroupHom f ξ).continuous_toFun
  continuous_invFun :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := (MulEquiv.ofBijective (fundamentalGroupHom f ξ)
        (fundamentalGroupHom_bijective_of_pullback_isEquivalence f ξ)).toEquiv)
      (fundamentalGroupHom f ξ).continuous_toFun

lemma

fundamentalGroupEquivOfPullbackEquivalence_apply

L62 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfPullbackEquivalence_apply

Documentation

The isomorphism has the original canonical homomorphism as its forward map.

Source context 7 commands

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

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

Lean source · statement

lemma fundamentalGroupEquivOfPullbackEquivalence_apply
    (f : X ⟶ Y) [(pullback f).IsEquivalence] (ξ : Spec (.of Ω) ⟶ X)
    (a : π₁ᵉᵗ(ξ)) :
    fundamentalGroupEquivOfPullbackEquivalence f ξ a = fundamentalGroupHom f ξ a

Module documentation

Fundamental groups under an equivalence of finite étale covers

Declarations

fundamentalGroupHom_bijective_of_pullback_isEquivalence

fundamentalGroupEquivOfPullbackEquivalence

fundamentalGroupEquivOfPullbackEquivalence_apply