chainsMap_f_2_comp_chainsIso₂ — Mathlib

English

There is a basic induced map ChainsMap₁: ModuleCat.of k (G →₀ A) → ModuleCat.of k (H →₀ B) arising from f and φ, aligning with the domain/codomain carriers via lmapDomain and mapRange.

Русский

Существует базовое индуцированное отображение ChainsMap₁: модульного типа от G→₀A к H→₀B, получаемое из f и φ, согласующееся с носителями домена/кода через lmapDomain и mapRange.

LaTeX

$$$\mathrm{ChainsMap}_1 f φ : \mathrm{ModuleCat.of}_k (G \to_0 A) \to \mathrm{ModuleCat.of}_k (H \to_0 B)$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem chainsMap_f_2_comp_chainsIso₂ :
    (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ chainsMap₂ f φ :=
  by
  ext
  simp [chainsMap_f, chainsIso₂]

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