single_mem_cycles₂_iff — Mathlib

English

For x ∈ Finsupp (Prod G G) A.V.carrier, x ∈ Z2(G,A) iff the stated combination equals the combination with g-fst*g-snd, etc.

Русский

Для x ∈ Finsupp (Prod G G) A.V.carrier, x ∈ Z2(G,A) тогда, когда соблюдается указанная сумма-равенство.

LaTeX

$$x ∈ Z_2(G,A) ↔ x.sum (fun g a => single g.2 (A.ρ g.1⁻¹ a) + single g.1 a) = x.sum (fun g a => single (g.1 * g.2) a)$$

Lean4

theorem single_mem_cycles₂_iff (g : G × G) (a : A) :
    single g a ∈ cycles₂ A ↔ single (g.1 * g.2) (A.ρ g.1 a) = single g.2 a + single g.1 (A.ρ g.1 a) :=
  by
  rw [← (mapRange_injective (α := G) _ (map_zero _) (A.ρ.apply_bijective g.1⁻¹).1).eq_iff]
  simp [mem_cycles₂_iff, mapRange_add, eq_comm]

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