Commit 2025-04-03 10:34 c6c1d4a8

View on Github →

feat(AlgebraicGeometry): universally open morphisms (#23606)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added theorem AlgebraicGeometry.topologically_isLocalAtSource'

added theorem AlgebraicGeometry.topologically_isLocalAtSource

added theorem AlgebraicGeometry.universally_isLocalAtSource

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Created Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean

added theorem AlgebraicGeometry.Flat.generalizingMap

added theorem AlgebraicGeometry.Scheme.Hom.isOpenMap

added theorem AlgebraicGeometry.UniversallyOpen.eq

added theorem AlgebraicGeometry.isOpenMap_of_generalizingMap

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.universally_mk'

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem GeneralizingMap.restrictPreimage

added theorem TopologicalSpace.IsOpenCover.generalizingMap_iff_comp

added theorem TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isOpenMap_iff_comp