truncLE'ToRestriction_naturality — Mathlib

English

Duplicate instance: if i not boundary, then f i is an isomorphism.

Русский

Дубликат: если i не граница, то f i изоморфизм.

LaTeX

$$$\text{IsIso}\bigl((K.truncLE'ToRestriction e).f i\bigr)$$$

Lean4

@[reassoc (attr := simp)]
theorem truncLE'ToRestriction_naturality :
    truncLE'Map φ e ≫ L.truncLE'ToRestriction e = K.truncLE'ToRestriction e ≫ restrictionMap φ e :=
  (unopFunctor C c.symm).congr_map
    (congr_arg Quiver.Hom.op (restrictionToTruncGE'_naturality ((opFunctor C c').map φ.op) e.op))

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