map₁_one — Mathlib

English

There is an induced map mapCycles₂ : cycles₂ A → cycles₂ B for the given f and φ, analogous to mapCycles₁ but at the second level.

Русский

Существует индуцированное отображение mapCycles₂: cycles₂ A → cycles₂ B для данного f и φ, подобное mapCycles₁, но на втором уровне.

LaTeX

$$$ mapCycles_2(f, \varphi) : \mathrm{cycles}_2(A) \to \mathrm{cycles}_2(B) $$$

Lean4

@[simp]
theorem map₁_one (φ : A ⟶ (Action.res _ (1 : G →* H)).obj B) : map (1 : G →* H) φ 1 = 0 :=
  by
  simp only [← cancel_epi (H1π A), H1π_comp_map, Limits.comp_zero]
  ext x
  rw [ModuleCat.hom_comp]
  refine (H1π_eq_zero_iff _).2 ?_
  simpa [coe_mapCycles₁ _ φ x, mapDomain, map_finsuppSum] using
    (boundaries₁ B).finsuppSum_mem k x.1 _ fun _ _ => single_one_mem_boundaries₁ (A := B) _

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