Structures · Geometry
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion
An open immersion of PresheafedSpaces is an open embedding f : X ⟶ U ⊆ Y of the underlying
spaces, such that the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.
- Shape
- One type argument · adds base_open, c_iso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CommRingCat
How is a type an instance?
Loading the hierarchy index…
Assumed by70
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_toPresheafedSpace
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso'
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace.congr_simp
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_uniq
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_inv
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft
Ancestors0
No ancestors.