English
Equivalences between zpow expressions on a full permutation and its restricted subtype permutation hold under the right invariant conditions on the support.
Русский
Сохранение эквивалентности zpow между полной перестановкой и её ограничением на подтип выполняется при корректных условия инвариантности опоры.
LaTeX
$$$c^n = ofSubtype(g.subtypePerm) \\iff c.subtypePerm (isInvariant_of_support_le) ^n = g.subtypePerm$$$
Lean4
theorem zpow_eq_ofSubtype_subtypePerm_iff {g c : Equiv.Perm α} {s : Finset α} (hg : ∀ x, g x ∈ s ↔ x ∈ s)
(hc : c.support ⊆ s) (n : ℤ) :
c ^ n = ofSubtype (g.subtypePerm hg) ↔ c.subtypePerm (isInvariant_of_support_le hc) ^ n = g.subtypePerm hg :=
by
constructor
· intro h
ext ⟨x, hx⟩
simp only [Perm.congr_fun h x, subtypePerm_apply_zpow_of_mem, Subtype.coe_mk, subtypePerm_apply]
rw [ofSubtype_apply_of_mem]
· simp only [Subtype.coe_mk, subtypePerm_apply]
· exact hx
· intro h; ext x
rw [← h]
by_cases hx : x ∈ s
· rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx, subtypePerm_zpow, subtypePerm_apply]
· rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx, ← notMem_support]
exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))
