English
Given a G-representation A and a normal S ≤ G, one obtains a short exact sequence 0 → Ker(mk) → A → A_S → 0 of G-representations, where mk is the quotient map to A_S.
Русский
Для пока G-представления A и нормальной S ≤ G получается кратная точная последовательность 0 → Ker(mk) → A → A_S → 0
LaTeX
$$coinvariantsShortComplex : ShortComplex (Rep k G)$$
Lean4
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `A` induces a short exact sequence of
`G`-representations `0 ⟶ Ker(mk) ⟶ A ⟶ A_S ⟶ 0` where `mk` is the quotient map to the
`S`-coinvariants `A_S`. -/
@[simps X₁ X₂ X₃ f g]
def coinvariantsShortComplex : ShortComplex (Rep k G)
where
X₁ := toCoinvariantsKer A S
X₂ := A
X₃ := toCoinvariants A S
f := subtype ..
g := mkQ ..
zero := by ext x; exact (Submodule.Quotient.mk_eq_zero _).2 x.2
