Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-07-31 09:13
7f9cbc06
View on Github →
feat(AlgebraicGeometry): Define preimmersions. (
#14748
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
added
theorem
AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion
added
theorem
AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion
deleted
theorem
AlgebraicGeometry.IsClosedImmersion.surjective_stalkMap
Created
Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
added
theorem
AlgebraicGeometry.IsPreimmersion.comp_iff
added
theorem
AlgebraicGeometry.IsPreimmersion.of_comp
added
theorem
AlgebraicGeometry.Scheme.Hom.embedding
added
theorem
AlgebraicGeometry.Scheme.Hom.stalkMap_surjective
added
theorem
AlgebraicGeometry.isPreimmersion_eq_inf
Modified
Mathlib/Geometry/RingedSpace/SheafedSpace.lean
added
theorem
AlgebraicGeometry.SheafedSpace.hom_stalk_ext
added
theorem
AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi