English
For a ∈ g.Basis and c ∈ cycleFactorsFinset, the element a c is supported on c.
Русский
Для a ∈ g.Basis и c ∈ cycleFactorsFinset элемент a c поддерживается на c.
LaTeX
$$a.mem_support_self c$$
Lean4
theorem ofPermHomFun_apply_mem_support_cycle_iff {x : α} {c : g.cycleFactorsFinset} :
ofPermHomFun a τ x ∈ ((τ : Perm g.cycleFactorsFinset) c : Perm α).support ↔ x ∈ c.val.support :=
by
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, m, hm⟩)
· simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx]
suffices ∀ (d : g.cycleFactorsFinset), x ∉ (d : Perm α).support by simp only [this]
intro d hx'
rw [Function.mem_fixedPoints_iff, ← notMem_support] at hx
apply hx
exact mem_cycleFactorsFinset_support_le d.prop hx'
· rw [ofPermHomFun_apply_of_cycleOf_mem a τ hd hm] --
rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]
by_cases h : c = d
· simp only [h, hd, mem_support_self]
· have H : Disjoint c.val d.val := cycleFactorsFinset_pairwise_disjoint g c.prop d.prop (Subtype.coe_ne_coe.mpr h)
have H' : Disjoint ((τ : Perm g.cycleFactorsFinset) c : Perm α) ((τ : Perm g.cycleFactorsFinset) d : Perm α) :=
cycleFactorsFinset_pairwise_disjoint g ((τ : Perm g.cycleFactorsFinset) c).prop
((τ : Perm g.cycleFactorsFinset) d).prop
(by
intro h'; apply h
simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h')
rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'
simp only [H hd, H' (mem_support_self a _)]
