Commit 2023-06-30 17:15 f68e3bd1

View on Github →

feat: port AlgebraicGeometry.Morphisms.Basic (#5599)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_iff

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_target_iff

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.stableUnderBaseChange

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyPullbackFstOfRightOfStableUnderBaseChange

added structure AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal

added def AlgebraicGeometry.AffineTargetMorphismProperty.StableUnderBaseChange

added def AlgebraicGeometry.AffineTargetMorphismProperty.diagonal

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonalOfTargetAffineLocally

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.isLocalOfOpenCoverImply

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk

added def AlgebraicGeometry.AffineTargetMorphismProperty.toProperty

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply

added def AlgebraicGeometry.AffineTargetMorphismProperty

added theorem AlgebraicGeometry.IsAffineOpen.map_isIso

added def AlgebraicGeometry.MorphismProperty.topologically

added theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_TFAE

added theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff

added structure AlgebraicGeometry.PropertyIsLocalAtTarget

added theorem AlgebraicGeometry.affine_cancel_left_isIso

added theorem AlgebraicGeometry.affine_cancel_right_isIso

added theorem AlgebraicGeometry.diagonalTargetAffineLocallyOfOpenCover

added theorem AlgebraicGeometry.diagonal_targetAffineLocally_eq_targetAffineLocally

added def AlgebraicGeometry.targetAffineLocally

added theorem AlgebraicGeometry.targetAffineLocallyOfOpenCover

added theorem AlgebraicGeometry.targetAffineLocally_respectsIso

added theorem AlgebraicGeometry.universallyIsLocalAtTarget

added theorem AlgebraicGeometry.universallyIsLocalAtTargetOfMorphismRestrict

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean