comp_const

Mathlib.CategoryTheory.FiberedCategory.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const

Lean4

theorem comp_const : (ι F S) ⋙ forget F = (const (F.obj ⟨op S⟩)).obj S :=
  Functor.ext_of_iso (compIso F S) (fun _ ↦ rfl) (fun _ => rfl)

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

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

Разделы

Аффилиация

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