NYLL
Module

UniversalHomeomorphism.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.UniversalHomeomorphism
3 declarations indexed from sourceView source ↗

Module documentation

Universal homeomorphisms preserve finite étale covers

Every affine chart of the lower scheme has an actual finite étale model of the upper cover. The models and their recovery isomorphisms supply the transition maps, whose equations are detected by fully faithful radicial pullback. Gluing gives essential surjectivity without a flatness condition.

Together with the previously established full faithfulness, this proves the finite étale equivalence for arbitrary schemes. For connected schemes, the induced map on fundamental groups is the forward map of a topological group isomorphism.

Source: Stacks Project, Proposition 58.8.4, Tag 0BQN: https://stacks.math.columbia.edu/tag/0BQN

Imports6
Imported by1

Declarations

theorem

pullback_essSurj_of_integral_universallyInjective_surjective

L44 ↗
AlgebraicGeometry.FiniteEtale.pullback_essSurj_of_integral_universallyInjective_surjective
Documentation

Actual affine models glue to a finite étale model along an arbitrary integral, universally injective, surjective scheme morphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
attribute [local instance] finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism
Lean source · statement
theorem pullback_essSurj_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).EssSurj
theorem

pullback_isEquivalence_of_universalHomeomorphism

L89 ↗
AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_universalHomeomorphism
Documentation

Pullback along a universal homeomorphism is an equivalence on finite étale covers, with no finiteness assumptions on the schemes.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
attribute [local instance] finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism
Lean source · statement
theorem pullback_isEquivalence_of_universalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (FiniteEtale.pullback f).IsEquivalence
theorem

universalHomeomorphism_fundamentalGroup_invariance

L109 ↗
AlgebraicGeometry.FiniteEtale.universalHomeomorphism_fundamentalGroup_invariance
Documentation

For connected schemes, the actual induced homomorphism of fundamental groups along a universal homeomorphism is a topological group isomorphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
attribute [local instance] finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism
Lean source · statement
theorem universalHomeomorphism_fundamentalGroup_invariance
    {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y] (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X) :
    ∃ e : π₁ᵉᵗ(ξ) ≃ₜ* π₁ᵉᵗ(ξ ≫ f),
      ∀ a : π₁ᵉᵗ(ξ), e a = fundamentalGroupHom f ξ a

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