Commit 2024-11-14 04:36 410e5f28

View on Github →

feat(AlgebraicGeometry): universally injective morphisms (#18845)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

added theorem AlgebraicGeometry.UniversallyClosed.of_comp_surjective

Created Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

added theorem AlgebraicGeometry.Scheme.Hom.injective

added theorem AlgebraicGeometry.UniversallyInjective.iff_diagonal

added theorem AlgebraicGeometry.UniversallyInjective.respectsIso

added theorem AlgebraicGeometry.universallyInjective_eq

added theorem AlgebraicGeometry.universallyInjective_eq_diagonal

Modified Mathlib/AlgebraicGeometry/PullbackCarrier.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

added theorem CategoryTheory.Limits.pullback.isIso_diagonal_iff

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.diagonal_isomorphisms

Modified Mathlib/Topology/Maps/Basic.lean