ofCompIso

Mathlib.CategoryTheory.Limits.Shapes.Kernels

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsKernel.ofCompIso

Lean4

/-- If `i` is an isomorphism such that `l ≫ i.hom = f`, any kernel of `f` is a kernel of `l`. -/
def ofCompIso {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : l ≫ i.hom = f) {s : KernelFork f} (hs : IsLimit s) :
    IsLimit (KernelFork.ofι (Fork.ι s) <| show Fork.ι s ≫ l = 0 by simp [← i.comp_inv_eq.2 h.symm]) :=
  Fork.IsLimit.mk _ (fun s => hs.lift <| KernelFork.ofι (Fork.ι s) <| by simp [← h]) (fun s => by simp) fun s m h =>
    by
    apply Fork.IsLimit.hom_ext hs
    simpa using h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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