H1InfRes — Mathlib

English

The inflation map is injective as a morphism of short complexes.

Русский

Инфляционная карта инъективна как морфизм кратких комплексов.

LaTeX

$$$\text{instMonoModuleCatFH1InfRes}$$$

Lean4

/-- The short complex `H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A)`. -/
@[simps X₁ X₂ X₃ f g]
noncomputable def H1InfRes : ShortComplex (ModuleCat k)
    where
  X₁ := groupCohomology (A.quotientToInvariants S) 1
  X₂ := groupCohomology A 1
  X₃ := groupCohomology ((Action.res _ S.subtype).obj A) 1
  f := map (QuotientGroup.mk' S) (subtype _ _ <| le_comap_invariants A.ρ S) 1
  g := map S.subtype (𝟙 _) 1
  zero := by
    rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S) (fun f φ => map f φ 1), map₁_one]

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