Commit 2023-07-04 18:51 cc5d11f2

View on Github →

feat: port AlgebraicGeometry.Morphisms.QuasiSeparated (#5691)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.IsAffineOpen.isQuasiSeparated

added def AlgebraicGeometry.QuasiSeparated.affineProperty

added theorem AlgebraicGeometry.QuasiSeparated.affineProperty_isLocal

added theorem AlgebraicGeometry.QuasiSeparated.affine_openCover_TFAE

added theorem AlgebraicGeometry.QuasiSeparated.affine_openCover_iff

added theorem AlgebraicGeometry.QuasiSeparated.is_local_at_target

added theorem AlgebraicGeometry.QuasiSeparated.openCover_iff

added theorem AlgebraicGeometry.QuasiSeparated.openCover_tFAE

added theorem AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen

added theorem AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated

added theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux

added theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs

added theorem AlgebraicGeometry.quasiSeparatedOfComp

added theorem AlgebraicGeometry.quasiSeparatedSpace_iff_affine

added theorem AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated

added theorem AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated

added theorem AlgebraicGeometry.quasiSeparated_eq_affineProperty

added theorem AlgebraicGeometry.quasiSeparated_eq_affineProperty_diagonal

added theorem AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact

added theorem AlgebraicGeometry.quasiSeparated_over_affine_iff

added theorem AlgebraicGeometry.quasiSeparated_respectsIso

added theorem AlgebraicGeometry.quasiSeparated_stableUnderBaseChange

added theorem AlgebraicGeometry.quasiSeparated_stableUnderComposition

added theorem AlgebraicGeometry.quasi_compact_affineProperty_diagonal_eq

added theorem AlgebraicGeometry.quasi_compact_affineProperty_iff_quasiSeparatedSpace