W_whiskerLeft_iff

Mathlib.CategoryTheory.Sites.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff

Lean4

theorem W_whiskerLeft_iff {P Q : Cᵒᵖ ⥤ A} (f : P ⟶ Q) : K.W (whiskerLeft G.op f) ↔ J.W f :=
  by
  rw [← W_inverseImage_whiskeringLeft J K G]
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru