Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-22 08:25
970a6567
View on Github →
feat(AlgebraicGeometry): basic properties of separated morphisms and schemes (
#17960
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
added
theorem
AlgebraicGeometry.IsAffineOpen.preimage
deleted
theorem
AlgebraicGeometry.isAffineOpen.preimage
Modified
Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
deleted
theorem
AlgebraicGeometry.IsClosedImmersion.of_comp
added
theorem
AlgebraicGeometry.IsClosedImmersion.of_comp_isClosedImmersion
Modified
Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
added
theorem
AlgebraicGeometry.IsClosedImmersion.of_comp
added
theorem
AlgebraicGeometry.IsSeparated.comp_iff
added
theorem
AlgebraicGeometry.IsSeparated.of_comp
added
theorem
AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift
Modified
Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean
added
theorem
inl_coprodIsoPushout_hom
added
theorem
inl_coprodIsoPushout_inv
added
theorem
inr_coprodIsoPushout_hom
added
theorem
inr_coprodIsoPushout_inv
added
theorem
prodIsoPullback_hom_fst
added
theorem
prodIsoPullback_hom_snd
added
theorem
prodIsoPullback_inv_fst
added
theorem
prodIsoPullback_inv_snd
Created
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean
added
theorem
CategoryTheory.Limits.isPullback_equalizer_prod
added
theorem
CategoryTheory.Limits.isPushout_coequalizer_coprod