chainsMap_f_3_comp_chainsIso₃ — Mathlib

English

There is a two-variable chains map ChainsMap₂ for pairs (G×G) → A to (H×H) → B induced by Prod.map f f and φ, acting on the carrier accordingly.

Русский

Существует отображение ChainsMap₂ для пар (G×G) → A в (H×H) → B, индуцируемое Prod.map f f и φ, действующее на носитель соответствующим образом.

LaTeX

$$$\mathrm{ChainsMap}_2 f φ : \mathrm{ModuleCat.of}_k (G × G →_0 A) \to \mathrm{ModuleCat.of}_k (H × H →_0 B)$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem chainsMap_f_3_comp_chainsIso₃ :
    (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom = (chainsIso₃ A).hom ≫ chainsMap₃ f φ :=
  by
  ext
  simp [chainsMap_f, chainsIso₃, ← Fin.comp_tail]

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