Module

UniversalHomeomorphismSections.lean

Nyll.SchemeTheory.Etale.UniversalHomeomorphismSections

2 declarations indexed from sourceView source ↗

Module documentation

Descending étale sections along universal homeomorphisms

A section of the base-changed étale morphism is an open immersion. The homeomorphism on the total spaces carries its image to an open subscheme of the original étale scheme. The projection of this open subscheme is étale, surjective, and universally injective, hence an isomorphism.

Imports7

Nyll.SchemeTheory.Morphisms.EtaleRadicial
Nyll.SchemeTheory.Morphisms.RadicialDescent
Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.Topology.Maps.Basic

Imported by4

theorem

exists_section_of_integral_universallyInjective_surjective

L36 ↗

AlgebraicGeometry.Etale.exists_section_of_integral_universallyInjective_surjective

Documentation

A section after a universal homeomorphism descends to an actual section of the original étale morphism.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.Etale

Lean source · statement

theorem exists_section_of_integral_universallyInjective_surjective
    {X Y V : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f]
    (p : V ⟶ Y) [Etale p] (w : X ⟶ V) (hw : w ≫ p = f) :
    ∃ r : Y ⟶ V, r ≫ p = 𝟙 Y ∧ f ≫ r = w

theorem

exists_lift_of_integral_universallyInjective_surjective

L87 ↗

AlgebraicGeometry.Etale.exists_lift_of_integral_universallyInjective_surjective