Module

ClosedNeighborhoodEqualizer.lean

Nyll.SchemeTheory.Etale.ClosedNeighborhoodEqualizer

1 declaration indexed from sourceView source ↗

Module documentation

Equalizing maps after refining a closed-subscheme neighborhood

Two maps from a closed subscheme into an unramified scheme, equal at a chosen point, become equal after an étale refinement of the ambient scheme through which the point lifts. We pull back the open diagonal to form their equality locus, then apply the constructed neighborhood lifting theorem. The test scheme may be any nonempty one-point scheme.

Imports6

Nyll.SchemeTheory.Etale.ClosedNeighborhoodLift
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Pullbacks

Imported by2

theorem

exists_refinement_equalizing_of_closedImmersion

L38 ↗

AlgebraicGeometry.Etale.exists_refinement_equalizing_of_closedImmersion

Documentation

Maps into a locally finite type formally unramified scheme that agree at a point agree on the closed restriction of a pointed ambient étale refinement.

Source context 5 commands

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

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

Lean source · statement

theorem exists_refinement_equalizing_of_closedImmersion
    {X Z W B P : Scheme.{u}} [Subsingleton P] [Nonempty P]
    (i : Z ⟶ X) [IsClosedImmersion i]
    (f : W ⟶ B) [FormallyUnramified f] [LocallyOfFiniteType f]
    (a b : Z ⟶ W) (hab : a ≫ f = b ≫ f)
    (p : P ⟶ Z) (hp : p ≫ a = p ≫ b) :
    ∃ (V : Scheme.{u}) (g : V ⟶ X), Etale g ∧
      pullback.fst i g ≫ a = pullback.fst i g ≫ b ∧
      ∃ q : P ⟶ pullback i g, q ≫ pullback.fst i g = p

Module documentation

Equalizing maps after refining a closed-subscheme neighborhood

Declarations

exists_refinement_equalizing_of_closedImmersion