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