Commit 2024-07-18 18:03 20d3080a

View on Github →

feat(AlgebraicGeometry): closed immersions are local at the target (#14763) Shows that closed immersions are local at the target.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added def AlgebraicGeometry.arrowIsoSpecΓOfIsAffine

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.IsClosedImmersion.eq_inf

added theorem AlgebraicGeometry.IsClosedImmersion.of_surjective_of_isAffine

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

Modified Mathlib/RingTheory/LocalProperties.lean

added theorem surjective_respectsIso