lowerCentralSeries_map_subtype_le

English

The map of γ_n(H) under the inclusion H ↪ G sits inside γ_n(G).

Русский

образ γ_n(H) под включением H → G лежит в γ_n(G).

LaTeX

$$$(lowerCentralSeries H n).map H.subtype \\le \\lowerCentralSeries G n$$$

Lean4

theorem lowerCentralSeries_map_subtype_le (H : Subgroup G) (n : ℕ) :
    (lowerCentralSeries H n).map H.subtype ≤ lowerCentralSeries G n := by
  induction n with
  | zero => simp
  | succ d hd =>
    rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]
    apply Subgroup.closure_mono
    rintro x1 ⟨x2, ⟨x3, hx3, x4, _hx4, rfl⟩, rfl⟩
    exact ⟨x3, hd (mem_map.mpr ⟨x3, hx3, rfl⟩), x4, by simp⟩

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