Commit 2024-10-26 13:47 d4e8628a

View on Github →

feat(AlgebraicGeometry): morphisms into separated schemes are determined by a dense subset (#18151)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

added theorem AlgebraicGeometry.IsSeparated.of_isAffineHom

added theorem AlgebraicGeometry.ext_of_isDominant

added theorem AlgebraicGeometry.ext_of_isDominant_of_isSeparated

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

added theorem AlgebraicGeometry.IsDominant.of_comp_of_isOpenImmersion

added theorem AlgebraicGeometry.surjective_of_isDominant_of_isClosed_range

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

added theorem CategoryTheory.Over.isPullback_of_binaryFan_isLimit

added def CategoryTheory.Over.prodLeftIsoPullback

added theorem CategoryTheory.Over.prodLeftIsoPullback_hom_fst

added theorem CategoryTheory.Over.prodLeftIsoPullback_hom_snd

added theorem CategoryTheory.Over.prodLeftIsoPullback_inv_fst

added theorem CategoryTheory.Over.prodLeftIsoPullback_inv_snd

Created Mathlib/CategoryTheory/Limits/Shapes/Connected.lean

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

deleted theorem CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits

deleted theorem CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits