Commit 2024-10-11 13:11 15074a61

View on Github →

feat(AlgebraicGeometry): factorization of morphisms with affine target (#15033)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added def AlgebraicGeometry.affineTargetImage

added def AlgebraicGeometry.affineTargetImageFactorization

added theorem AlgebraicGeometry.affineTargetImageFactorization_app_injective

added theorem AlgebraicGeometry.affineTargetImageFactorization_comp

added def AlgebraicGeometry.affineTargetImageInclusion

added theorem AlgebraicGeometry.affineTargetImageInclusion_app_surjective

added def AlgebraicGeometry.arrowIsoΓSpecOfIsAffine

added def AlgebraicGeometry.specTargetImage

added def AlgebraicGeometry.specTargetImageFactorization

added theorem AlgebraicGeometry.specTargetImageFactorization_app_injective

added theorem AlgebraicGeometry.specTargetImageFactorization_comp

added def AlgebraicGeometry.specTargetImageIdeal

added def AlgebraicGeometry.specTargetImageRingHom

added theorem AlgebraicGeometry.specTargetImageRingHom_surjective

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv

added theorem AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq