cocycles₁_map_inv — Mathlib

English

Let A be a representation of G over k and f a 1‑cocycle with values in A. Then for every g ∈ G, Aρ(g) applied to f(g^{-1}) equals the additive negation of f(g): A.ρ(g)(f(g^{-1})) = -f(g).

Русский

Пусть A — представление группы G над кольцом k и f — 1‑кокцикл в A. Тогда для каждого g ∈ G выполняется Aρ(g) f(g^{-1}) = -f(g).

LaTeX

$$$\\\\forall f \\\\in \\, cocycles_1(A), \\\\forall g \\\\in G \\\\quad A.\\\\rho(g)(f(g^{-1})) = -f(g).$$$

Lean4

@[simp]
theorem cocycles₁_map_inv (f : cocycles₁ A) (g : G) : A.ρ g (f g⁻¹) = -f g := by
  rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g, (mem_cocycles₁_iff f).1 f.2 g g⁻¹]

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