Theorems · Definition · algebraic geometry
AlgebraicGeometry.SheafedSpace.IsOpenImmersion
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : AlgebraicGeometry.SheafedSpace C} → (X ⟶ Y) → PropA morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism of PresheafedSpaces
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.InducedCategory.Hom.homproof · cited by 850
- AlgebraicGeometry.SheafedSpacestatement and proof · cited by 142
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersionproof · cited by 44
Cited by32
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersionproof · cited by 28
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctorstatement and proof · cited by 13
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invAppstatement and proof · cited by 12
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrictstatement and proof · cited by 5
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_appstatement and proof · cited by 2
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrictstatement and proof · cited by 2
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_isostatement · cited by 2
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invAppstatement and proof · cited by 1
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'statement and proof · cited by 1
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturalitystatement and proof · cited by 1
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrictstatement and proof · cited by 1
- AlgebraicGeometry.SheafedSpace.GlueData.mk.injstatement and proof · cited by 1