Module

UnramifiedPointRigidity.lean

Nyll.SchemeTheory.Morphisms.UnramifiedPointRigidity

2 declarations indexed from sourceView source ↗

Module documentation

Unramified maps determined at one nonempty test scheme

The relative equalizer of maps to a separated unramified scheme is both open and closed. Agreement after a map from a nonempty scheme makes this equalizer nonempty. A preconnected source therefore forces the maps equal.

Imports6

Nyll.SchemeTheory.Morphisms.UnramifiedHomExt
Mathlib.AlgebraicGeometry.Morphisms.IsIso
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Mathlib.Topology.Connected.Clopen

Imported by2

theorem

hom_ext_of_nonempty_of_unramified

L32 ↗

AlgebraicGeometry.Over.hom_ext_of_nonempty_of_unramified

Documentation

Over a preconnected source, maps into a separated unramified scheme are equal if they agree after any map from a nonempty scheme.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem Over.hom_ext_of_nonempty_of_unramified
    {S : Scheme.{u}} {X Y Z : Over S}
    [PreconnectedSpace X.left] [Nonempty Z.left]
    [FormallyUnramified Y.hom] [LocallyOfFiniteType Y.hom] [IsSeparated Y.hom]
    (f g : X ⟶ Y) (i : Z ⟶ X) (h : i ≫ f = i ≫ g) : f = g

theorem

eq_id_of_unramified_of_fixes_nonempty

L53 ↗

AlgebraicGeometry.Scheme.Hom.eq_id_of_unramified_of_fixes_nonempty