Commit 2024-11-23 14:58 1620b762

View on Github →

feat(AlgebraicGeometry): preimmersions are stable under base change (#18915)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

added theorem AlgebraicGeometry.Scheme.Cover.exists_eq

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective

Created Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

added theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective

added theorem AlgebraicGeometry.SurjectiveOnStalks.Spec_iff

added theorem AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise

added theorem AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine

added theorem AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback

added theorem AlgebraicGeometry.SurjectiveOnStalks.of_comp

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.Hom.homeomorph_apply

added theorem AlgebraicGeometry.Scheme.homeoOfIso_apply

added theorem AlgebraicGeometry.Scheme.homeoOfIso_symm

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem isEmbedding_of_iSup_eq_top_of_preimage_subset_range