Module

ClosedImmersionLift.lean

Nyll.SchemeTheory.Morphisms.ClosedImmersionLift

1 declaration indexed from sourceView source ↗

Module documentation

Factoring a map from a reduced scheme through a closed immersion

Set-theoretic containment suffices: the pullback is a surjective closed immersion into the reduced source, hence an isomorphism. In particular this applies to points valued in any field, without an algebraic closure hypothesis.

Imports3

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Properties

Imported by6

lemma

exists_lift_of_isReduced_of_range_subset

L29 ↗

AlgebraicGeometry.IsClosedImmersion.exists_lift_of_isReduced_of_range_subset

Documentation

A map from a reduced scheme factors through a closed immersion if its image is contained in the closed subscheme's image.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.IsClosedImmersion

Lean source · statement

lemma exists_lift_of_isReduced_of_range_subset
    {X Z Y : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    (f : Y ⟶ X) [IsReduced Y] (h : Set.range f ⊆ Set.range i) :
    ∃ g : Y ⟶ Z, g ≫ i = f

Module documentation

Factoring a map from a reduced scheme through a closed immersion

Declarations

exists_lift_of_isReduced_of_range_subset