instMonoModuleCatFH1InfRes — Mathlib

English

The inflation morphism is mono.

Русский

Инфляционный морфизм является моно.

LaTeX

$$$\mathrm{Mono}(H^1\!Inf\!Res).f$$$

Lean4

/-- The inflation map `H¹(G ⧸ S, A^S) ⟶ H¹(G, A)` is a monomorphism. -/
instance : Mono (H1InfRes A S).f :=
  by
  rw [ModuleCat.mono_iff_injective, injective_iff_map_eq_zero]
  intro x hx
  induction x using H1_induction_on with
  | @h x =>
    simp_all only [H1InfRes_X₂, H1InfRes_X₁, H1InfRes_f, H1π_comp_map_apply (QuotientGroup.mk' S)]
    rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩
    refine
      (H1π_eq_zero_iff _).2
        ⟨⟨y, fun s => ?_⟩,
          funext fun g =>
            QuotientGroup.induction_on g fun g => Subtype.ext <| by simpa [-SetLike.coe_eq_coe] using congr_fun hy g⟩
    simpa [coe_mapCocycles₁ (x := x), sub_eq_zero, (QuotientGroup.eq_one_iff s.1).2 s.2] using congr_fun hy s.1

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