H1CoresCoinfOfTrivial — Mathlib

English

If A is a G-representation trivial on a normal subgroup S, the induced morphism g in the core/coinfinity construction H1CoresCoinfOfTrivial A S is epi.

Русский

Пусть A — G-репрезентация, тривиальная на нормальной подгруппе S. Тогда морфизм g в конструкции H1CoresCoinfOfTrivial A S является эпиморфизмом.

LaTeX

$$$ \text{epi} \big( H1CoresCoinfOfTrivial(A,S).g \big) $$$

Lean4

/-- Given a `G`-representation `A` on which a normal subgroup `S ≤ G` acts trivially, this is the
short complex `H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A)`. -/
@[simps X₁ X₂ X₃ f g]
noncomputable def H1CoresCoinfOfTrivial : ShortComplex (ModuleCat k)
    where
  X₁ := H1 ((Action.res _ S.subtype).obj A)
  X₂ := H1 A
  X₃ := H1 (ofQuotient A S)
  f := map S.subtype (𝟙 _) 1
  g := map (QuotientGroup.mk' S) (resOfQuotientIso A S).inv 1
  zero := by rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]

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