Commit 2024-10-24 05:08 923081a6

View on Github →

feat(AlgebraicGeometry/Restrict): more API for Scheme.Opens. (#17968)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added def AlgebraicGeometry.Scheme.Hom.isoImage

added theorem AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι

added theorem AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι

modified theorem AlgebraicGeometry.Scheme.Hom.map_resLE

added theorem AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι

added theorem AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι

modified theorem AlgebraicGeometry.Scheme.Hom.resLE_id

modified theorem AlgebraicGeometry.Scheme.Hom.resLE_map

added def AlgebraicGeometry.Scheme.homOfLE

added theorem AlgebraicGeometry.Scheme.homOfLE_app

added theorem AlgebraicGeometry.Scheme.homOfLE_apply

added theorem AlgebraicGeometry.Scheme.homOfLE_base

added theorem AlgebraicGeometry.Scheme.homOfLE_homOfLE

added theorem AlgebraicGeometry.Scheme.homOfLE_rfl

added theorem AlgebraicGeometry.Scheme.homOfLE_ι

added def AlgebraicGeometry.Scheme.isoOfEq

added theorem AlgebraicGeometry.Scheme.isoOfEq_hom_ι

added theorem AlgebraicGeometry.Scheme.isoOfEq_inv_ι

added theorem AlgebraicGeometry.Scheme.isoOfEq_rfl

deleted theorem AlgebraicGeometry.Scheme.map_basicOpen'

added theorem AlgebraicGeometry.Scheme.map_basicOpen

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_ofRestrict

deleted def AlgebraicGeometry.Scheme.restrictIsoOfEq

deleted def AlgebraicGeometry.Scheme.restrictRestrict

deleted theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict

deleted theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict

added theorem AlgebraicGeometry.Scheme.toIso_inv_ι

added def AlgebraicGeometry.Scheme.topIso

added theorem AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image

added theorem AlgebraicGeometry.Scheme.ι_toIso_inv

deleted theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι