Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.Hom.coborderRange
{X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [AlgebraicGeometry.IsImmersion f] → Y.OpensGiven an immersion f : X ⟶ Y, this is the biggest open set U ⊆ Y containing the image of X
such that X is closed in U.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- Set.rangeproof · cited by 4,705
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- AlgebraicGeometry.Scheme.Opensstatement · cited by 1,149
- AlgebraicGeometry.PresheafedSpace.Hom.baseproof · cited by 1,135
- AlgebraicGeometry.LocallyRingedSpace.Hom.toHomproof · cited by 995
- AlgebraicGeometry.Scheme.Hom.toLRSHom'proof · cited by 895
- coborderproof · cited by 22
- AlgebraicGeometry.IsImmersionstatement and proof · cited by 17
Cited by9
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.liftCoborderstatement and proof · cited by 6
- AlgebraicGeometry.Scheme.Hom.liftCoborder_ιstatement and proof · cited by 6
- AlgebraicGeometry.Scheme.Hom.liftCoborder_preimagestatement and proof · cited by 2
- AlgebraicGeometry.liftCoborder_appstatement and proof · cited by 1
- AlgebraicGeometry.isIso_of_comp_eq_sigmaSpecproof · cited by 1
- AlgebraicGeometry.Scheme.Hom.coborderRange.congr_simpstatement and proof · cited by 0
- AlgebraicGeometry.Scheme.Hom.liftCoborder_ι_assocstatement and proof · cited by 0
- AlgebraicGeometry.IsImmersion.isImmersion_iff_existsproof · cited by 0
- AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborderstatement and proof · cited by 0