Mathlib Map

Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsClosedImmersion.isIso_of_ker_eq

∀ {Z₁ Z₂ X : AlgebraicGeometry.Scheme} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [AlgebraicGeometry.IsClosedImmersion i₁]
  [AlgebraicGeometry.IsClosedImmersion i₂] (f : Z₁ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp f i₂ = i₁ →
    AlgebraicGeometry.Scheme.Hom.ker i₁ = AlgebraicGeometry.Scheme.Hom.ker i₂ → CategoryTheory.IsIso f
Defined in
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Cited by
2 results in Mathlib
Foundations
Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AlgebraicGeometry.IsClosedImmersionAlgebraicGeometry.IsClosedImmersion
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.isPullback_of_isClosedImmersion · cited by 1AlgebraicGeometry.isPullb…AlgebraicGeometry.IsClosedImmersion.isIso_lift · cited by 0IsClosedImmersion.isIso_l…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compTop.top · cited by 9680Top.topCategoryTheory.Functor.map · cited by 8698Functor.mapCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeQuiver.Hom.op · cited by 1948Hom.opCategoryTheory.Equivalence.functor · cited by 1268Equivalence.functorCategoryTheory.IsIso · cited by 1156CategoryTheory.IsIsoEq.le · cited by 605Eq.leCategoryTheory.homOfLE · cited by 554CategoryTheory.homOfLEAlgebraicGeometry.Scheme.IdealSheafData · cited by 192Scheme.IdealSheafDataCategoryTheory.Over.forget · cited by 164Over.forgetAlgebraicGeometry.Scheme.Hom.ker · cited by 51Hom.kerAlgebraicGeometry.IsClosedImmersion · cited by 49AlgebraicGeometry.IsClose…IsClosedImmersion.isIso_of_ke…CITED BYCITES

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.