Theorems · Definition · algebraic geometry
AlgebraicGeometry.sigmaOpenCover
{σ : Type v} → (g : σ → AlgebraicGeometry.Scheme) → [inst : Small.{u, v} σ] → (∐ g).OpenCoverThe cover of ∐ X by the Xᵢ.
- Defined in
- Mathlib.AlgebraicGeometry.Limits
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Small
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functor.mapstatement · cited by 8,698
- CategoryTheory.Functor.compstatement · cited by 6,529
- Equiv.symmproof · cited by 3,681
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.Discretestatement · cited by 2,447
- CategoryTheory.Iso.reflproof · cited by 727
- CategoryTheory.Discrete.functorstatement and proof · cited by 633
- Smallstatement and proof · cited by 369
- CategoryTheory.Limits.sigmaObjstatement · cited by 302
- AlgebraicGeometry.Scheme.OpenCoverstatement · cited by 207
Cited by4
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSourceproof · cited by 1
- AlgebraicGeometry.sigmaOpenCover_fstatement and proof · cited by 1
- AlgebraicGeometry.sigmaOpenCover_I₀statement and proof · cited by 0
- AlgebraicGeometry.sigmaOpenCover_Xstatement and proof · cited by 0