range_norm_eq_ker_applyAsHom_sub — Mathlib

English

The range of applyAsHom(leftRegular) minus identity coincides with the kernel of the norm map on the left regular representation when g generates a finite cyclic group.

Русский

Образ applyAsHom(левого регулярного) минус единица совпадает с ядром нормировочной карты на левом регулярном представлении, когда g порождает конечную циклическую группу.

LaTeX

$$$ \operatorname{range}(\mathrm{applyAsHom}_{k,G}(g) - \mathrm{id}) = \ker(\mathrm{leftRegular}_{k,G}.\mathrm{norm}.hom) $$$

Lean4

theorem range_norm_eq_ker_applyAsHom_sub (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    LinearMap.range (leftRegular k G).norm.hom.hom = LinearMap.ker (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom :=
  le_antisymm (fun _ ⟨_, h⟩ => by simp_all [← h]) fun x hx =>
    ⟨single 1 (x g), by ext j;
      simpa [Representation.norm] using
        (apply_eq_of_leftRegular_eq_of_generator g hg _ (by simpa [sub_eq_zero] using hx) j).symm⟩

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