English
The component of mapCycles₂ on an element x is exactly given by chainsMap₂ f φ applied to x, i.e. the underlying value coincides with the chains-level map.
Русский
Компонент отображения mapCycles₂ на элемент x равен chainsMap₂ f φ примененному к x; смысловая часть выражения совпадает на уровне цепей.
LaTeX
$$$ (mapCycles_2(f, \varphi)\, x)^{\!1} = \ big( chainsMap_2(f, \varphi) \big) x $$$
Lean4
instance mapCycles₁_quotientGroupMk'_epi : Epi (mapCycles₁ (QuotientGroup.mk' S) (resOfQuotientIso A S).inv) :=
by
rw [ModuleCat.epi_iff_surjective]
rintro ⟨x, hx⟩
choose! s hs using QuotientGroup.mk_surjective (s := S)
have hs₁ : QuotientGroup.mk ∘ s = id := funext hs
refine ⟨⟨mapDomain s x, ?_⟩, Subtype.ext <| by simp [mapCycles₁_hom, ← mapDomain_comp, hs₁]⟩
simpa [mem_cycles₁_iff, ← (mem_cycles₁_iff _).1 hx,
sum_mapDomain_index_inj (f := s) (fun x y h => by rw [← hs x, ← hs y, h])] using
Finsupp.sum_congr fun a b =>
QuotientGroup.induction_on a fun a => by
simp [← QuotientGroup.mk_inv, apply_eq_of_coe_eq A.ρ S (s a)⁻¹ a⁻¹ (by simp [hs])]
