Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S),
  CategoryTheory.Sieve.ofArrows X f = CategoryTheory.Sieve.ofArrows X' f' →
    ((F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence)

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

2 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category