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