mem_range_toPermHom_iff — Mathlib

English

A permutation τ lies in the range of toPermHom g precisely when it preserves cycle-factor sizes: the size of the support of τ c equals that of c, for all cycle-factors c.

Русский

Перестановка τ лежит в образе toPermHom g тогда и только тогда, когда она сохраняет размер поддержки: для всех факторов цикла размер поддержи τ c равен размеру c.

LaTeX

$$$τ ∈ (toPermHom g).range \\iff ∀ c, #(τ c).val.support = #c.val.support$$$

Lean4

theorem mem_range_toPermHom_iff {τ} : τ ∈ (toPermHom g).range ↔ ∀ c, #(τ c).val.support = #c.val.support :=
  by
  constructor
  · rintro ⟨k, rfl⟩ c
    rw [coe_toPermHom, Equiv.Perm.support_conj]
    apply Finset.card_map
  · obtain ⟨a⟩ := Basis.nonempty g
    exact fun hτ ↦ ⟨toCentralizer a ⟨τ, hτ⟩, toPermHom_apply_toCentralizer a ⟨τ, hτ⟩⟩

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