Commit 2024-07-01 12:34 66e97554

View on Github →

chore(AlgebraicGeometry/Morphisms): split basic file (#14297) Moves constructors for properties from other properties in a new file. Removes morphismRestrict_base as it is a duplicate of morphismRestrict_val_base.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE

deleted def AlgebraicGeometry.AffineTargetMorphismProperty.diagonal

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_targetAffineLocally

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso

deleted def AlgebraicGeometry.MorphismProperty.topologically

deleted theorem AlgebraicGeometry.MorphismProperty.topologically_isStableUnderComposition

deleted theorem AlgebraicGeometry.MorphismProperty.topologically_iso_le

deleted theorem AlgebraicGeometry.MorphismProperty.topologically_propertyIsLocalAtTarget

deleted theorem AlgebraicGeometry.MorphismProperty.topologically_respectsIso

deleted theorem AlgebraicGeometry.diagonal_targetAffineLocally_eq_targetAffineLocally

deleted theorem AlgebraicGeometry.diagonal_targetAffineLocally_of_openCover

deleted theorem AlgebraicGeometry.morphismRestrict_base

deleted theorem AlgebraicGeometry.universally_isLocalAtTarget

deleted theorem AlgebraicGeometry.universally_isLocalAtTarget_of_morphismRestrict

Created Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE

added def AlgebraicGeometry.AffineTargetMorphismProperty.diagonal

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_targetAffineLocally

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso

added def AlgebraicGeometry.MorphismProperty.topologically

added theorem AlgebraicGeometry.MorphismProperty.topologically_isStableUnderComposition

added theorem AlgebraicGeometry.MorphismProperty.topologically_iso_le

added theorem AlgebraicGeometry.MorphismProperty.topologically_propertyIsLocalAtTarget

added theorem AlgebraicGeometry.MorphismProperty.topologically_respectsIso

added theorem AlgebraicGeometry.diagonal_targetAffineLocally_eq_targetAffineLocally

added theorem AlgebraicGeometry.diagonal_targetAffineLocally_of_openCover

added theorem AlgebraicGeometry.universally_isLocalAtTarget

added theorem AlgebraicGeometry.universally_isLocalAtTarget_of_morphismRestrict

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean