English
Let α be a finite set, g a permutation of α, a a basis element of g, and τ a range_toPermHom' g. Then the size of the support of the induced map a → τ equals the sum of the sizes of the supports of the cycle factors comprising τ.
Русский
Пусть α — конечный множество, g перестановка на α, a базисная величина для g, и τ элемент диапазона range_toPermHom' g. Тогда размер поддержки отображения a на τ равен сумме размеров опор факторов цикла, входящих в τ.
LaTeX
$$$\#((ofPermHom a τ).support) = \sum_{c \in (τ : Perm g.cycleFactorsFinset).support} \#(c.val.support)$$$
Lean4
theorem card_ofPermHom_support :
#(ofPermHom a τ).support = ∑ c ∈ (τ : Perm g.cycleFactorsFinset).support, #c.val.support :=
by
rw [ofPermHom_support, Finset.card_biUnion]
intro c _ d _ h
apply Equiv.Perm.Disjoint.disjoint_support
apply g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr h)
