d₀₁ — Mathlib

English

The first differential maps A to the cochains on G with a concrete action; it is the differential d: A → C^1(G,A).

Русский

Первый дифференциал, отображающий A в коочеины степени 1, реализуется как d: A → C^1(G,A).

LaTeX

$$$d_{01}: A.V \to (ModuleCat.moduleCategory k).Hom (A.V) (G \to A.V)$$$

Lean4

/-- The 0th differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
`k`-linear map `A → Fun(G, A)`. It sends `(a, g) ↦ ρ_A(g)(a) - a.` -/
@[simps!]
def d₀₁ : A.V ⟶ ModuleCat.of k (G → A) :=
  ModuleCat.ofHom
    { toFun m g := A.ρ g m - m
      map_add' x y := funext fun g => by simp only [map_add, add_sub_add_comm]; rfl
      map_smul' r x := funext fun g => by dsimp; rw [map_smul, smul_sub] }

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