Structures · Geometry
AlgebraicGeometry.Scheme.Cover.LocallyDirected
A directed P-cover of a scheme X is a cover 𝒰 with an ordering
on the indices and compatible transition maps 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j such that
every x : 𝒰ᵢ ×[X] 𝒰ⱼ comes from some 𝒰ₖ for a k ≤ i and k ≤ j.
- Defined in
- Mathlib.AlgebraicGeometry.Cover.Directed
- Shape
- One type argument · adds trans, trans_id, trans_comp, w, directed, property_trans
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- AlgebraicGeometry.IsOpenImmersion
How is a type an instance?
Loading the hierarchy index…
Assumed by89
- AlgebraicGeometry.Scheme.Cover.trans
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone
- AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.prop_trans
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTrans
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans
- AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans
- AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimit
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap
- AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase
- AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected
- AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected
- AlgebraicGeometry.Scheme.Cover.trans_map
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι
- AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected
- AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left
- AlgebraicGeometry.Scheme.Cover.LocallyDirected.w
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone
- AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst
- AlgebraicGeometry.Scheme.Cover.trans_id
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι
- AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitGluedCocone
- AlgebraicGeometry.Scheme.Cover.trans_comp
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd
- AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans
- AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq
- AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected
- AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id
- AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instCategoryI₀Cover
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_I₀
- AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj
Ancestors0
No ancestors.