Theorems · Inductive type · category theory

CategoryTheory.GrothendieckTopology.Cover.Arrow

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → J.Cover X → Type (max u v)

An auxiliary structure, used to define S.index.

Defined in: Mathlib.CategoryTheory.Sites.Grothendieck
Cited by: 99 results in Mathlib
Foundations: Depth 33 from the axioms, rests on 228 definitions · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement · cited by 32,673
CategoryTheory.GrothendieckTopologystatement · cited by 1,415
CategoryTheory.GrothendieckTopology.Coverstatement · cited by 211

Cited by152

Results whose statement or proof uses this declaration.

CategoryTheory.GrothendieckTopology.Cover.shapeproof · cited by 147
CategoryTheory.GrothendieckTopology.Cover.Arrow.Ystatement and proof · cited by 78
CategoryTheory.GrothendieckTopology.Cover.Arrow.fstatement and proof · cited by 45
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Zstatement and proof · cited by 32
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁statement and proof · cited by 28
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relationstatement · cited by 27
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂statement and proof · cited by 27
CategoryTheory.Functor.IsDenseSubsite.mapPreimageproof · cited by 23
CategoryTheory.GrothendieckTopology.Cover.Relation.fststatement · cited by 22
CategoryTheory.GrothendieckTopology.Cover.Relation.sndstatement · cited by 22
CategoryTheory.Meqproof · cited by 17
CategoryTheory.GrothendieckTopology.Cover.Arrow.hfstatement and proof · cited by 15