Commit 2023-06-19 08:58 2c9b00db

View on Github →

feat: port AlgebraicGeometry.OpenImmersion.Basic (#5046)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/OpenImmersion/Basic.lean

added def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_range

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq

added def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft

added def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit

added theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_uniq

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_toSheafedSpace

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_base

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_c

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_toPresheafedSpace

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso

added theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_openEmbedding