Closed and open immersions

TheoremClosed immersions of constant fibre rank are isomorphisms#✓fully proved

A closed immersion between maps of constant fibre rank is an isomorphism.

theorem isIso_of_isClosedImmersion_of_finrank_comp_eq
    {X Y S : Scheme.{u}} (i : X ⟶ Y) (g : Y ⟶ S) (f : X ⟶ S) (w : i ≫ g = f)
    [IsClosedImmersion i] [IsFinite g] [Flat g] [LocallyOfFinitePresentation g]
    [Flat f] [LocallyOfFinitePresentation f]
    (h : ∀ s : ↥S, f.finrank s = g.finrank s) :
    IsIso i

TheoremReduced closed immersions with equal range are isomorphic#✓fully proved

Two reduced closed immersions with the same range are isomorphic over the target.

theorem AlgebraicGeometry.IsClosedImmersion.exists_iso_hom_comp_eq_of_range_eq
    {A B X : Scheme.{u}} (f : A ⟶ X) (g : B ⟶ X) [IsClosedImmersion f]
    [IsClosedImmersion g] [IsReduced A] [IsReduced B]
    (h : Set.range f.base = Set.range g.base) :
    ∃ e : A ≅ B, e.hom ≫ g = f

TheoremClosed immersions flat over the base of an étale map are open#✓fully proved

A closed immersion whose composite with an étale map is flat and locally of finite presentation is open.

theorem AlgebraicGeometry.IsOpenImmersion.of_isClosedImmersion_of_flat_comp_of_etale
    {Z X Y : Scheme.{u}} (i : Z ⟶ X) (g : X ⟶ Y) [IsClosedImmersion i] [Etale g]
    [Flat (i ≫ g)] [LocallyOfFinitePresentation (i ≫ g)] :
    IsOpenImmersion i ∧ Etale (i ≫ g)

TheoremClosed immersions are stable under base change#✓fully proved

Closed immersions transfer along pullback squares.

theorem AlgebraicGeometry.IsClosedImmersion.of_isPullback
    {S S₀ X X₀ : Scheme.{u}} (i : S₀ ⟶ S) [IsClosedImmersion i]
    {f : X ⟶ S} {f₀ : X₀ ⟶ S₀} {g : X₀ ⟶ X} (hg : IsPullback g f₀ f i) :
    IsClosedImmersion g

Used by 1

Used bySeparatedness descends along surjective closed immersions

TheoremSurjectivity is stable under base change#✓fully proved

Surjectivity transfers along pullback squares.

theorem AlgebraicGeometry.Surjective.of_isPullback
    {S S₀ X X₀ : Scheme.{u}} (i : S₀ ⟶ S) [Surjective i]
    {f : X ⟶ S} {f₀ : X₀ ⟶ S₀} {g : X₀ ⟶ X} (hg : IsPullback g f₀ f i) :
    Surjective g

Used by 2

Used byUniversal closedness descends along surjective closed immersions · Separatedness descends along surjective closed immersions

TheoremUniversal closedness descends along surjective closed immersions#✓fully proved

Universal closedness transfers along a pullback square whose base map is a surjective closed immersion.

theorem AlgebraicGeometry.UniversallyClosed.of_isPullback
    {S S₀ X X₀ : Scheme.{u}} (i : S₀ ⟶ S) [IsClosedImmersion i] [Surjective i]
    {f : X ⟶ S} {f₀ : X₀ ⟶ S₀} {g : X₀ ⟶ X} (hg : IsPullback g f₀ f i)
    [UniversallyClosed f₀] : UniversallyClosed f

Uses 1 · Used by 1

Proof usesSurjectivity is stable under base change

Used byProperness descends along surjective closed immersions

TheoremSeparatedness descends along surjective closed immersions#✓fully proved

Separatedness transfers along a pullback square whose base map is a surjective closed immersion.

theorem AlgebraicGeometry.IsSeparated.of_isPullback
    {S S₀ X X₀ : Scheme.{u}} (i : S₀ ⟶ S) [IsClosedImmersion i] [Surjective i]
    {f : X ⟶ S} {f₀ : X₀ ⟶ S₀} {g : X₀ ⟶ X} (hg : IsPullback g f₀ f i)
    [IsSeparated f₀] : IsSeparated f

Uses 2 · Used by 1

Proof usesClosed immersions are stable under base change · Surjectivity is stable under base change

Used byProperness descends along surjective closed immersions

TheoremProperness descends along surjective closed immersions#✓fully proved

Properness transfers along a pullback square whose base map is a surjective closed immersion.

theorem AlgebraicGeometry.IsProper.of_isPullback
    {S S₀ X X₀ : Scheme.{u}} (i : S₀ ⟶ S) [IsClosedImmersion i] [Surjective i]
    {f : X ⟶ S} {f₀ : X₀ ⟶ S₀} {g : X₀ ⟶ X} (hg : IsPullback g f₀ f i)
    [IsProper f₀] [LocallyOfFiniteType f] : IsProper f

Uses 2

Proof usesSeparatedness descends along surjective closed immersions · Universal closedness descends along surjective closed immersions

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.