Module

ClopenPullback.lean

Nyll.SchemeTheory.FiniteEtale.ClopenPullback

4 declarations indexed from sourceView source ↗

Module documentation

Descending clopen subsets through finite étale equivalences

A clopen subscheme is a subterminal finite étale scheme. An equivalence on finite étale schemes lifts this object and detects its subterminality, so its lift is again a clopen subscheme. Fullness also detects containment of clopen subsets. Consequently every clopen subset descends uniquely.

Imports8

Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Equivalence
Mathlib.CategoryTheory.EssentialImage
Mathlib.Topology.Sets.Closeds

Imported by3

def

clopenFiniteEtale

L37 ↗

AlgebraicGeometry.FiniteEtale.clopenFiniteEtale

Source context 5 commands

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

@[expose] public section
open CategoryTheory TopologicalSpace
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · full declaration

def clopenFiniteEtale {X : Scheme.{u}} (U : Clopens X) : FiniteEtale X where
  toComma := Over.mk (Scheme.Opens.ι U.toOpens)
  prop := by
    let : IsClosedImmersion (Scheme.Opens.ι U.toOpens) :=
      IsClosedImmersion.of_isPreimmersion (Scheme.Opens.ι U.toOpens) (by
        rw [Scheme.Opens.range_ι]
        exact U.isClosed)
    change IsFiniteEtale (Scheme.Opens.ι U.toOpens)
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance

lemma

range_clopenFiniteEtale

L47 ↗

AlgebraicGeometry.FiniteEtale.range_clopenFiniteEtale

Source context 5 commands

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

@[expose] public section
open CategoryTheory TopologicalSpace
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

lemma range_clopenFiniteEtale {X : Scheme.{u}} (U : Clopens X) :
    Set.range (clopenFiniteEtale U).hom = (U : Set X)

lemma

clopen_subset_of_preimage_subset

L52 ↗

AlgebraicGeometry.FiniteEtale.clopen_subset_of_preimage_subset

Documentation

Fullness of finite étale pullback reflects containment of clopen subsets.

Source context 5 commands

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

@[expose] public section
open CategoryTheory TopologicalSpace
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

lemma clopen_subset_of_preimage_subset {X Y : Scheme.{u}} (f : X ⟶ Y)
    [(FiniteEtale.pullback f).Full] (U V : Clopens Y)
    (h : f ⁻¹' (U : Set Y) ⊆ f ⁻¹' (V : Set Y)) :
    (U : Set Y) ⊆ (V : Set Y)

theorem

existsUnique_clopen_preimage_of_pullback_isEquivalence

L89 ↗

AlgebraicGeometry.FiniteEtale.existsUnique_clopen_preimage_of_pullback_isEquivalence

Documentation

If pullback is an equivalence on finite étale schemes, every clopen subset of the source is the inverse image of a unique clopen subset of the target.

Source context 5 commands

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

@[expose] public section
open CategoryTheory TopologicalSpace
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

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

Module documentation

Descending clopen subsets through finite étale equivalences

Declarations

clopenFiniteEtale

range_clopenFiniteEtale

clopen_subset_of_preimage_subset

existsUnique_clopen_preimage_of_pullback_isEquivalence