Commit 2025-10-21 18:22 3218e4a7

View on Github →

chore(AlgebraicGeometry): add missing lemmas about morphism classes (#30596)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.app_surjective

added theorem AlgebraicGeometry.isClosedImmersion_iff_isAffineHom

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source

Modified Mathlib/AlgebraicGeometry/Morphisms/Descent.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

added theorem AlgebraicGeometry.IsFinite.comp_iff

added theorem AlgebraicGeometry.IsFinite.of_comp

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

modified theorem AlgebraicGeometry.Scheme.Hom.isConstructible_image

modified theorem AlgebraicGeometry.Scheme.Hom.isConstructible_preimage

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

modified theorem AlgebraicGeometry.Flat.epi_of_flat_of_surjective

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

modified def AlgebraicGeometry.Scheme.Hom.coborderRange

modified theorem AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range

modified def AlgebraicGeometry.Scheme.Hom.liftCoborder

modified theorem AlgebraicGeometry.Scheme.Hom.liftCoborder_ι

Modified Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

added theorem AlgebraicGeometry.IsIntegralHom.comp_iff

added theorem AlgebraicGeometry.IsIntegralHom.of_comp

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

added theorem AlgebraicGeometry.IsProper.comp_iff

added theorem AlgebraicGeometry.IsProper.of_comp

deleted theorem AlgebraicGeometry.IsProper.of_comp_of_isSeparated

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

deleted theorem AlgebraicGeometry.quasiCompact_over_affine_iff

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

modified theorem AlgebraicGeometry.IsAffineOpen.isQuasiSeparated

added theorem AlgebraicGeometry.QuasiCompact.of_comp

modified theorem AlgebraicGeometry.QuasiSeparated.of_comp

added theorem AlgebraicGeometry.Scheme.quasiSeparatedSpace_of_isOpenCover

modified theorem AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace

added theorem AlgebraicGeometry.quasiCompact_iff_compactSpace

deleted theorem AlgebraicGeometry.quasiSeparatedSpace_iff_affine

added theorem AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens

modified theorem AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated

added theorem AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace

deleted theorem AlgebraicGeometry.quasiSeparated_over_affine_iff

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

modified theorem AlgebraicGeometry.IsAffineHom.comp_iff

added theorem AlgebraicGeometry.IsClosedImmersion.comp_iff

modified theorem AlgebraicGeometry.isSeparated_of_injective

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/AlgebraicGeometry/Noetherian.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

modified def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'

modified def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase

modified def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft

modified def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight

modified def AlgebraicGeometry.Scheme.Pullback.openCoverOfRight

Modified Mathlib/AlgebraicGeometry/QuasiAffine.lean

Modified Mathlib/AlgebraicGeometry/ValuativeCriterion.lean