Commit 2023-07-15 00:13 2922c5fd

View on Github →

feat: port AlgebraicGeometry.Morphisms.RingHomProperties (#5663)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

added theorem AlgebraicGeometry.affineLocally_iff_affineOpens_le

added theorem AlgebraicGeometry.affineLocally_respectsIso

added theorem AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally

added theorem AlgebraicGeometry.scheme_restrict_basicOpen_of_localizationPreserves

added def AlgebraicGeometry.sourceAffineLocally

added theorem AlgebraicGeometry.sourceAffineLocally_isLocal

added theorem AlgebraicGeometry.sourceAffineLocally_of_source_open_cover_aux

added theorem AlgebraicGeometry.sourceAffineLocally_respectsIso

added theorem RingHom.PropertyIsLocal.affineLocally_of_comp

added theorem RingHom.PropertyIsLocal.affineLocally_of_isOpenImmersion

added theorem RingHom.PropertyIsLocal.affineLocally_stableUnderComposition

added theorem RingHom.PropertyIsLocal.affine_openCover_TFAE

added theorem RingHom.PropertyIsLocal.affine_openCover_iff

added theorem RingHom.PropertyIsLocal.isLocal_sourceAffineLocally

added theorem RingHom.PropertyIsLocal.is_local_affineLocally

added theorem RingHom.PropertyIsLocal.openCover_TFAE

added theorem RingHom.PropertyIsLocal.sourceAffineLocally_comp_of_isOpenImmersion

added theorem RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover

added theorem RingHom.PropertyIsLocal.source_affine_openCover_iff

added theorem RingHom.PropertyIsLocal.source_openCover_iff

added theorem RingHom.RespectsIso.basicOpen_iff

added theorem RingHom.RespectsIso.basicOpen_iff_localization

added theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff

added theorem RingHom.StableUnderBaseChange.Γ_pullback_fst

Modified Mathlib/RingTheory/Localization/Basic.lean