English
The cardinality of the support of ofPermHom a τ equals the sum of the cycle supports, i.e. the total size of all cycle supports under τ.
Русский
Кардиналитет опоры ofPermHom a τ равен сумме опор циклов — суммарный размер опор под τ.
LaTeX
$$ #(ofPermHom a τ).support = ∑ c ∈ (τ : Perm g.cycleFactorsFinset).support, #c.val.support$$
Lean4
theorem ofPermHom_support :
(ofPermHom a τ).support = (τ : Perm g.cycleFactorsFinset).support.biUnion (fun c ↦ c.val.support) :=
by
ext x
simp only [mem_support, Finset.mem_biUnion, ofPermHom_apply]
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)
· simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff, ← mem_support]
rintro ⟨c, -, hc⟩
rw [Function.mem_fixedPoints_iff] at hx
exact mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx
· rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm]
conv_lhs => rw [← hm]
rw [(g ^ m).injective.ne_iff, a.injective.ne_iff, not_iff_comm]
by_cases H : (τ : Perm g.cycleFactorsFinset) c = c
· simp only [H, iff_true]
push_neg
intro d hd
rw [← notMem_support]
have := g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop
rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at this
exact this (by aesop) hc
· simpa only [H, iff_false, not_not] using ⟨c, H, mem_support.mp hc⟩
