Module

ClopenFull.lean

Nyll.SchemeTheory.FiniteEtale.ClopenFull

8 declarations indexed from sourceView source ↗

Module documentation

Clopen descent from fullness of finite étale pullback

A clopen subset is represented by its characteristic section of the trivial cover with two sheets. Fullness descends that section, without any hypothesis that arbitrary finite étale covers descend. Lifting inclusions of clopen subschemes proves uniqueness. For quasi-compact quasi-separated schemes, this gives a homeomorphism on connected components.

This proves, in particular, the connected-component consequence of full faithfulness discussed in Stacks Project, Section 58.19, Tag 0BLE.

Imports14

Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.FiniteEtale.ClopenPullback
Nyll.SchemeTheory.Topology.ConnectedComponentsMap
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Basic
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
Mathlib.Topology.Sets.Closeds

Imported by1

Nyll.SchemeTheory.FiniteEtale.All

theorem

section_descent_of_pullback_full

L43 ↗

AlgebraicGeometry.FiniteEtale.section_descent_of_pullback_full

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem section_descent_of_pullback_full
    {X Y : Scheme.{u}} (f : X ⟶ Y) [(FiniteEtale.pullback f).Full]
    (W : FiniteEtale Y) (a : X ⟶ W.left) (ha : a ≫ W.hom = f) :
    ∃ s : Y ⟶ W.left, s ≫ W.hom = 𝟙 Y ∧ f ≫ s = a

theorem

exists_characteristic_morphism

L86 ↗

AlgebraicGeometry.FiniteEtale.exists_characteristic_morphism

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem exists_characteristic_morphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Clopens X) :
    ∃ a : X ⟶ Y ⨿ Y,
      a ≫ coprod.desc (𝟙 Y) (𝟙 Y) = f ∧
        a ⁻¹' Set.range (coprod.inl : Y ⟶ Y ⨿ Y) = (U : Set X)

theorem

isFiniteEtale_double

L133 ↗

AlgebraicGeometry.FiniteEtale.isFiniteEtale_double

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem isFiniteEtale_double (Y : Scheme.{u}) :
    IsFiniteEtale (coprod.desc (𝟙 Y) (𝟙 Y))

theorem

isClopen_range_inl

L148 ↗

AlgebraicGeometry.FiniteEtale.isClopen_range_inl

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem isClopen_range_inl (Y : Scheme.{u}) :
    IsClopen (Set.range (coprod.inl : Y ⟶ Y ⨿ Y))

theorem

existsUnique_clopen_preimage_of_pullback_full

L158 ↗

AlgebraicGeometry.FiniteEtale.existsUnique_clopen_preimage_of_pullback_full

Documentation

Fullness alone descends every clopen subset uniquely. The cover used to construct the descent is the trivial two-sheeted cover.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem existsUnique_clopen_preimage_of_pullback_full
    {X Y : Scheme.{u}} (f : X ⟶ Y) [(FiniteEtale.pullback f).Full]
    (U : Clopens X) :
    ∃! V : Clopens Y, f ⁻¹' (V : Set Y) = (U : Set X)

theorem

bijective_clopen_preimage_of_pullback_full

L181 ↗

AlgebraicGeometry.FiniteEtale.bijective_clopen_preimage_of_pullback_full

Documentation

Fullness of finite étale pullback gives a bijection on clopen subsets.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · full declaration

theorem bijective_clopen_preimage_of_pullback_full
    {X Y : Scheme.{u}} (f : X ⟶ Y) [(FiniteEtale.pullback f).Full] :
    Function.Bijective (fun U : Clopens Y =>
      (⟨f ⁻¹' (U : Set Y), U.isClopen.preimage f.continuous⟩ : Clopens X)) := by
  constructor
  · intro U V h
    have hpre : f ⁻¹' (U : Set Y) = f ⁻¹' (V : Set Y) :=
      congrArg (fun C : Clopens X => (C : Set X)) h
    apply Clopens.ext
    exact Set.Subset.antisymm
      (clopen_subset_of_preimage_subset f U V hpre.subset)
      (clopen_subset_of_preimage_subset f V U hpre.symm.subset)
  · intro U
    obtain ⟨V, hV, _⟩ := existsUnique_clopen_preimage_of_pullback_full f U
    exact ⟨V, Clopens.ext hV⟩

theorem

connectedSpace_iff_of_pullback_full

L198 ↗

AlgebraicGeometry.FiniteEtale.connectedSpace_iff_of_pullback_full

Documentation

Fullness of finite étale pullback preserves and reflects connectedness.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem connectedSpace_iff_of_pullback_full
    {X Y : Scheme.{u}} (f : X ⟶ Y) [(FiniteEtale.pullback f).Full] :
    ConnectedSpace X ↔ ConnectedSpace Y

theorem

connectedComponentsMap_isHomeomorph_of_pullback_full

L206 ↗

AlgebraicGeometry.FiniteEtale.connectedComponentsMap_isHomeomorph_of_pullback_full

Documentation

For qcqs schemes, fullness of finite étale pullback identifies their actual spaces of connected components. Essential surjectivity is unnecessary.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem connectedComponentsMap_isHomeomorph_of_pullback_full
    {X Y : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    [CompactSpace Y] [QuasiSeparatedSpace Y]
    (f : X ⟶ Y) [(FiniteEtale.pullback f).Full] :
    IsHomeomorph f.continuous.connectedComponentsMap

Module documentation

Clopen descent from fullness of finite étale pullback

Declarations