Theorems · Inductive type · category theory

CategoryTheory.PreOneHypercover

{C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type (max (max u v) (w + 1))

The categorical data that is involved in a 1-hypercover of an object S. This consists of a family of morphisms f i : X i ⟶ S for i : I₀, and for each tuple (i₁, i₂) of elements in I₀, a family of objects Y j indexed by a type I₁ i₁ i₂, which are equipped with a map to the fibre product of X i₁ and X i₂, which is phrased here as the data of the two projections p₁ : Y j ⟶ X i₁, p₂ : Y j ⟶ X i₂ and the relation p₁ j ≫ f i₁ = p₂ j ≫ f i₂. (See GrothendieckTopology.OneHypercover for the topological conditions.)

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

180 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category