kerParam_range_eq_centralizer_of_count_le_one

English

If all cycle counts are at most one, then the range of kerParam g equals the centralizer of g.

Русский

Если все счётчики цикла не более единицы, то range kerParam g совпадает с центральизатором g.

LaTeX

$$$ (kerParam g).range = Subgroup.centralizer\{ g \}$ при условии $\forall i, g.cycleType.count i \le 1$$$

Lean4

theorem kerParam_range_eq_centralizer_of_count_le_one (h_count : ∀ i, g.cycleType.count i ≤ 1) :
    (kerParam g).range = Subgroup.centralizer { g } := by
  ext x
  refine ⟨fun hx ↦ kerParam_range_le_centralizer hx, fun hx ↦ ?_⟩
  simp_rw [kerParam_range_eq, Subgroup.mem_map, MonoidHom.mem_ker, Subgroup.coe_subtype, Subtype.exists,
    exists_and_right, exists_eq_right]
  use hx
  ext c : 2
  rw [← Multiset.nodup_iff_count_le_one, cycleType_def,
    Multiset.nodup_map_iff_inj_on (cycleFactorsFinset g).nodup] at h_count
  exact h_count _ (by simp) _ c.prop ((mem_range_toPermHom_iff).mp (by simp) c)

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