cyclesIso₀_inv_comp_cyclesMap — Mathlib

English

If f is epi, then the induced map on the 0th level is also epi, i.e., map(Id_G) f 0 is epi in the category of k-modules.

Русский

Если f — эпиморфизм, то индуцированное отображение на нулевом уровне также эпиморфно: map(Id_G) f 0 — эпиморфизм в категории модулей над k.

LaTeX

$$$\operatorname{Epi}\, f \Rightarrow \operatorname{Epi} \big(\mathrm{map}(\mathrm{Id}_G) f 0\big)$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cyclesIso₀_inv_comp_cyclesMap : (cyclesIso₀ A).inv ≫ cyclesMap f φ 0 = φ.hom ≫ (cyclesIso₀ B).inv :=
  (CommSq.vert_inv ⟨cyclesMap_comp_cyclesIso₀_hom f φ⟩).w.symm

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