Commit 2024-07-19 11:08 23c87df3

View on Github →

feat(AlgebraicGeometry): Being an isomorphism is local at the target. (#14882)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Created Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

added theorem AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective

added theorem AlgebraicGeometry.isomorphisms_eq_stalkwise

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

added theorem AlgebraicGeometry.isOpenImmersion_eq_inf

Created Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

added theorem AlgebraicGeometry.Scheme.Hom.surjective

added theorem AlgebraicGeometry.Surjective.comp_iff

added theorem AlgebraicGeometry.Surjective.of_comp

added theorem AlgebraicGeometry.surjective_eq_topologically

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem isOpenMap_iff_isOpenMap_of_iSup_eq_top

Modified Mathlib/Topology/Sets/Opens.lean

added theorem TopologicalSpace.Opens.mem_top