Commit 2023-07-03 16:14 c156373e

View on Github →

feat: port AlgebraicGeometry.Morphisms.QuasiCompact (#5642)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Created Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

added def AlgebraicGeometry.QuasiCompact.affineProperty

added theorem AlgebraicGeometry.QuasiCompact.affineProperty_isLocal

added theorem AlgebraicGeometry.QuasiCompact.affineProperty_stableUnderBaseChange

added theorem AlgebraicGeometry.QuasiCompact.affineProperty_toProperty

added theorem AlgebraicGeometry.QuasiCompact.affine_openCover_iff

added theorem AlgebraicGeometry.QuasiCompact.affine_openCover_tFAE

added theorem AlgebraicGeometry.QuasiCompact.is_local_at_target

added theorem AlgebraicGeometry.QuasiCompact.openCover_iff

added theorem AlgebraicGeometry.QuasiCompact.openCover_tFAE

added theorem AlgebraicGeometry.compactSpace_iff_quasiCompact

added theorem AlgebraicGeometry.compact_open_induction_on

added theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen

added theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact

added theorem AlgebraicGeometry.isCompact_basicOpen

added theorem AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union

added theorem AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union

added theorem AlgebraicGeometry.quasiCompact_eq_affineProperty

added theorem AlgebraicGeometry.quasiCompact_iff_affineProperty

added theorem AlgebraicGeometry.quasiCompact_iff_forall_affine

added theorem AlgebraicGeometry.quasiCompact_iff_spectral

added theorem AlgebraicGeometry.quasiCompact_over_affine_iff

added theorem AlgebraicGeometry.quasiCompact_respectsIso

added theorem AlgebraicGeometry.quasiCompact_stableUnderBaseChange

added theorem AlgebraicGeometry.quasiCompact_stableUnderComposition

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.Hom.continuous

added theorem AlgebraicGeometry.Scheme.mem_basicOpen_top'