Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion

{X Y : AlgebraicGeometry.LocallyRingedSpace} → (X ⟶ Y) → Prop

A morphism of LocallyRingedSpaces is an open immersion if it is an open immersion as a morphism of SheafedSpaces

Defined in
Mathlib.Geometry.RingedSpace.OpenImmersion
Cited by
28 results in Mathlib
Foundations
Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.IsOpenImmersion · cited by 476AlgebraicGeometry.IsOpenI…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor · cited by 13IsOpenImmersion.opensFunc…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp · cited by 12IsOpenImmersion.invAppAlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift · cited by 7IsOpenImmersion.liftAlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict · cited by 4IsOpenImmersion.isoRestri…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac · cited by 3IsOpenImmersion.lift_facAlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict · cited by 2IsOpenImmersion.isoRestri…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app · cited by 2IsOpenImmersion.invApp_appAlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq · cited by 1IsOpenImmersion.lift_uniqAlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict · cited by 1IsOpenImmersion.isoRestri…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_stalk_iso · cited by 1IsOpenImmersion.of_stalk_…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset · cited by 1IsOpenImmersion.pullback_…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso · cited by 1IsOpenImmersion.to_isoAlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace · cited by 1IsOpenImmersion.locallyRi…AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp · cited by 1IsOpenImmersion.app_invAppQuiver.Hom · cited by 32603Quiver.HomAlgebraicGeometry.LocallyRingedSpace · cited by 205AlgebraicGeometry.Locally…AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom · cited by 31Hom.toShHomAlgebraicGeometry.SheafedSpace.IsOpenImmersion · cited by 23SheafedSpace.IsOpenImmers…LocallyRingedSpace.IsOpenImme…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by41

Results whose statement or proof uses this declaration.