English
The map kerParam g is injective; equivalently, kerParam defines a faithful parametrization of the range.
Русский
Отображение kerParam g инъективно; следовательно, параметризация образа правдоподобна и верна.
LaTeX
$$Function.Injective (kerParam g)$$
Lean4
theorem kerParam_injective (g : Perm α) : Function.Injective (kerParam g) :=
by
rw [kerParam, MonoidHom.noncommCoprod_injective]
refine ⟨ofSubtype_injective, ?_, ?_⟩
· apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
· intro a
simp only [range_subtype, ne_eq]
simp only [zpowers_eq_closure, ← closure_iUnion]
apply disjoint_closure_of_disjoint_support
rintro - ⟨-⟩ - ⟨-, ⟨b, rfl⟩, -, ⟨h, rfl⟩, ⟨-⟩⟩
rw [← disjoint_iff_disjoint_support]
apply cycleFactorsFinset_pairwise_disjoint g a.2 b.2
simp only [ne_eq, ← Subtype.ext_iff]
exact ne_comm.mp h
· exact fun i ↦ subtype_injective _
· rw [noncommPiCoprod_range, ← ofSubtype.range.closure_eq]
simp only [zpowers_eq_closure, ← closure_iUnion]
apply disjoint_closure_of_disjoint_support
rintro - ⟨a, rfl⟩ - ⟨-, ⟨b, rfl⟩, ⟨-⟩⟩
exact (ofSubtype_support_disjoint a).mono_right (mem_cycleFactorsFinset_support_le b.2)
