Theorems · Theorem · algebraic geometry

AlgebraicGeometry.FormallyUnramified.hom_ext

∀ {X Y Z' Z : AlgebraicGeometry.Scheme} (i : Z' ⟶ Z),
  IsNilpotent (AlgebraicGeometry.Scheme.Hom.ker i) →
    ∀ [AlgebraicGeometry.IsClosedImmersion i] (f : X ⟶ Y) [AlgebraicGeometry.FormallyUnramified f] {g₁ g₂ : Z ⟶ X},
      CategoryTheory.CategoryStruct.comp i g₁ = CategoryTheory.CategoryStruct.comp i g₂ →
        CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → g₁ = g₂

Given any commuting diagram `` Z' --→ X | | ↓ ↓ Z --→ Y ` With X ⟶ Y formally unramified and Z' ⟶ Z an infinitesimal thickening, there exists at most one arrow Z ⟶ X` making the diagram commute.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Cited by

0 results in Mathlib

Foundations

Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsClosedImmersionAlgebraicGeometry.FormallyUnramified