Commit 2024-06-24 12:36 ae6dfcde

View on Github →

feat(Geometry/OpenImmersion): lemmas for sheafed space/locally ringed space (#14039) copied from their presheafed space counter-part

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

modified def AlgebraicGeometry.IsOpenImmersion.isoRestrict

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_stalk_iso

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

added def AlgebraicGeometry.SheafedSpace.ofRestrict