Commit 2023-10-19 12:40 70998603

View on Github →

feat(Mathlib/AlgebraicGeometry): Move material on restriction to new file (#7749) Also provides new notations and fixed slow proofs

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

added theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff_of_isAffine

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac

added theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac

deleted def AlgebraicGeometry.Scheme.restrictFunctor

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_hom

deleted theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_left

deleted def AlgebraicGeometry.Scheme.restrictFunctorΓ

added theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace

deleted theorem AlgebraicGeometry.image_morphismRestrict_preimage

deleted theorem AlgebraicGeometry.isPullback_morphismRestrict

deleted def AlgebraicGeometry.morphismRestrict

deleted def AlgebraicGeometry.morphismRestrictEq

deleted def AlgebraicGeometry.morphismRestrictOpensRange

deleted def AlgebraicGeometry.morphismRestrictRestrict

deleted def AlgebraicGeometry.morphismRestrictRestrictBasicOpen

deleted def AlgebraicGeometry.morphismRestrictStalkMap

deleted theorem AlgebraicGeometry.morphismRestrict_base_coe

deleted theorem AlgebraicGeometry.morphismRestrict_c_app

deleted theorem AlgebraicGeometry.morphismRestrict_comp

deleted theorem AlgebraicGeometry.morphismRestrict_val_base

deleted theorem AlgebraicGeometry.morphismRestrict_ι

deleted def AlgebraicGeometry.pullbackRestrictIsoRestrict

deleted theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict

deleted theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict

deleted theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst

deleted theorem AlgebraicGeometry.Γ_map_morphismRestrict

Created Mathlib/AlgebraicGeometry/Restrict.lean

added def AlgebraicGeometry.Scheme.restrictFunctor

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict

added theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_hom

added theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_left

added def AlgebraicGeometry.Scheme.restrictFunctorΓ

added def AlgebraicGeometry.Scheme.restrictIsoOfEq

added def AlgebraicGeometry.Scheme.restrictRestrict

added def AlgebraicGeometry.Scheme.restrictRestrictComm

added theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict

added theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict

added theorem AlgebraicGeometry.image_morphismRestrict_preimage

added theorem AlgebraicGeometry.isPullback_morphismRestrict

added def AlgebraicGeometry.morphismRestrict

added def AlgebraicGeometry.morphismRestrictEq

added def AlgebraicGeometry.morphismRestrictOpensRange

added def AlgebraicGeometry.morphismRestrictRestrict

added def AlgebraicGeometry.morphismRestrictRestrictBasicOpen

added def AlgebraicGeometry.morphismRestrictStalkMap

added theorem AlgebraicGeometry.morphismRestrict_base_coe

added theorem AlgebraicGeometry.morphismRestrict_c_app

added theorem AlgebraicGeometry.morphismRestrict_comp

added theorem AlgebraicGeometry.morphismRestrict_val_base

added theorem AlgebraicGeometry.morphismRestrict_ι

added def AlgebraicGeometry.pullbackRestrictIsoRestrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst

added theorem AlgebraicGeometry.Γ_map_morphismRestrict

Modified Mathlib/Geometry/RingedSpace/Stalks.lean

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ'

Modified Mathlib/Topology/Category/TopCat/Opens.lean

added theorem TopologicalSpace.Opens.coe_inclusion