lsingle_comp_chainsMap_f — Mathlib

English

For any x in Fin n → G, the basic element lsingl e x composed with the chain map equals the action of φ on lsingle(f ∘ x).

Русский

Для каждого x ∈ Fin n → G, элемент lsingle x после применения цепного отображения равен действию φ на lsingle (f ∘ x).

LaTeX

$$lsingle x ≫ (chainsMap f φ).f n = φ.hom ≫ lsingle (f ∘ x)$$

Lean4

@[reassoc (attr := simp)]
theorem lsingle_comp_chainsMap_f (n : ℕ) (x : Fin n → G) :
    ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n = φ.hom ≫ ModuleCat.ofHom (lsingle (f ∘ x)) :=
  by
  ext
  simp [chainsMap_f]

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