f — Mathlib · SciLib

English

The isomorphism f(z) in the surjectivity statement is an isomorphism for filtered index categories.

Русский

Изоморфизм f(z) в утверждении о сюръективности является изоморфизмом при фильтрованных индексах.

LaTeX

$$$\text{IsIso } f(z)\;\text{ for } [IsFiltered J]$$$

Lean4

/-- The canonical map `colimit (pullback c.ι ((Functor.const J).map z)) ⟶ X`,
which is an isomorphism when `J` is filtered, see `isIso_f`. -/
noncomputable def f : colimit (pullback c.ι ((Functor.const J).map z)) ⟶ X :=
  colimit.desc _ (Cocone.mk X { app j := (pullback.snd c.ι ((Functor.const _).map z)).app j })

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