restrictionToTruncGE'_naturality — Mathlib

English

If K is strictly supported relative to e, then every f i is an isomorphism.

Русский

Если K строго поддержан относительно e, то каждый f i является изоморфизмом.

LaTeX

$$For all i, IsIso((K.restrictionToTruncGE' e).f i)$$

Lean4

@[reassoc (attr := simp)]
theorem restrictionToTruncGE'_naturality :
    K.restrictionToTruncGE' e ≫ truncGE'Map φ e = restrictionMap φ e ≫ L.restrictionToTruncGE' e :=
  by
  ext i
  by_cases hi : e.BoundaryGE i
  ·
    simp [restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv _ e rfl hi, truncGE'Map_f_eq_opcyclesMap φ e hi rfl,
      restrictionXIso]
  · simp [restrictionToTruncGE'_f_eq_iso_hom_iso_inv _ e rfl hi, truncGE'Map_f_eq φ e hi rfl, restrictionXIso]

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