cocycles₂_ρ_map_inv_sub_map_inv

English

For g ∈ G, A.ρ(g)(f(g^{-1}, g)) - f(g, g^{-1}) = f(1,1) - f(g,1).

Русский

Для любого g ∈ G выполняется A.ρ(g)(f(g^{-1}, g)) - f(g, g^{-1}) = f(1,1) - f(g,1).

LaTeX

$$$$ A.\\\\rho(g)(f(g^{-1}, g)) - f(g, g^{-1}) = f(1,1) - f(g,1). $$$$

Lean4

theorem cocycles₂_ρ_map_inv_sub_map_inv (f : cocycles₂ A) (g : G) :
    A.ρ g (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1) :=
  by
  have := (mem_cocycles₂_iff f).1 f.2 g g⁻¹ g
  simp only [mul_inv_cancel, inv_mul_cancel, cocycles₂_map_one_fst _ g] at this
  exact sub_eq_sub_iff_add_eq_add.2 this.symm

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