Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.Pullback.diagonalCover
{X Y : AlgebraicGeometry.Scheme} →
(f : X ⟶ Y) →
(𝒰 : Y.OpenCover) →
((i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) →
(CategoryTheory.Limits.pullback.diagonalObj f).OpenCoverGiven 𝒰 i covering Y and 𝒱 i j covering 𝒰 i, this is the open cover
𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂ ranging over all i, j₁, j₂.
- Defined in
- Mathlib.AlgebraicGeometry.Pullbacks
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.PreZeroHypercover.I₀statement and proof · cited by 763
- CategoryTheory.PreZeroHypercover.Xstatement and proof · cited by 649
- CategoryTheory.PreZeroHypercover.fstatement · cited by 542
- AlgebraicGeometry.IsOpenImmersionstatement · cited by 476
- CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercoverstatement and proof · cited by 469
- AlgebraicGeometry.Scheme.precoveragestatement · cited by 336
- AlgebraicGeometry.Scheme.OpenCoverstatement and proof · cited by 207
- CategoryTheory.Limits.pullback.diagonalObjstatement · cited by 80
- CategoryTheory.Precoverage.ZeroHypercover.pullback₁statement and proof · cited by 64
- AlgebraicGeometry.Scheme.Cover.pullbackHomproof · cited by 32
Cited by9
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRangeproof · cited by 6
- AlgebraicGeometry.Scheme.Pullback.diagonalCover_mapstatement and proof · cited by 2
- AlgebraicGeometry.Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteTypeproof · cited by 2
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eqproof · cited by 1
- AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonalstatement and proof · cited by 1
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D₀proof · cited by 1