NYLL
Module

Perfection.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.Perfection
2 declarations indexed from sourceView source ↗

Module documentation

Perfection invariance

Purely inseparable extension of the constant field preserves connectedness for an arbitrary scheme. The existing descent theorem for actual finite étale covers then identifies the canonical fundamental-group homomorphism with a topological group isomorphism after passage to a perfect closure.

The perfect-closure formulation uses exponential characteristic, so it also includes characteristic zero, with exponential characteristic one.

Source: Stacks Project, Lemma 58.14.2, Tag 0BTW: https://stacks.math.columbia.edu/tag/0BTW

Imports9
Imported by1

Declarations

theorem

connectedSpace_of_purelyInseparable_constant_extension

L42 ↗
AlgebraicGeometry.FiniteEtale.connectedSpace_of_purelyInseparable_constant_extension
Documentation

A purely inseparable extension of the constant field preserves connectedness without any finiteness assumptions on the scheme.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
theorem connectedSpace_of_purelyInseparable_constant_extension
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsPurelyInseparable k L]
    (X : Scheme.{u}) [ConnectedSpace X] (f : X ⟶ Spec (.of k)) :
    ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)
theorem

perfection_invariance

L61 ↗
AlgebraicGeometry.FiniteEtale.perfection_invariance
Documentation

Perfection preserves connectedness and makes the actual pullback map on étale fundamental groups an isomorphism of topological groups. There are no quasi-compactness, quasi-separatedness, Noetherian, or finite-type hypotheses.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
theorem perfection_invariance
    (k L : Type u) [Field k] [Field L] [Algebra k L]
    (p : ℕ) [ExpChar k p] [ExpChar L p] [PerfectRing L p]
    [IsPerfectClosure (algebraMap k L) p]
    (X : Scheme.{u}) [ConnectedSpace X] (f : X ⟶ Spec (.of k)) :
    ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) ∧
      ∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
        (ξ : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f),
        ∃ e : π₁ᵉᵗ(ξ) ≃ₜ* π₁ᵉᵗ(ξ ≫ Limits.pullback.snd
            (Spec.map (CommRingCat.ofHom (algebraMap k L))) f),
          ∀ a : π₁ᵉᵗ(ξ), e a = fundamentalGroupHom (Limits.pullback.snd
            (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) ξ a

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