English
For a given equivalence f, and any a, the map sending a factor to its image under f preserves membership in the normalized factors under the commuting normalization condition.
Русский
Для заданного эквивалента f отображение фактора через f сохраняет принадлежность к нормализованным факторам при условии commuting нормализации.
LaTeX
$$normalizedFactorsEquiv (he) a : {f} frac{...} $$
Lean4
/-- If the monoid equiv `f : α ≃* β` commutes with `normalize` then, for `a : α`, it yields a
bijection between the `normalizedFactors` of `a` and of `f a`.
-/
def normalizedFactorsEquiv (he : ∀ x, normalize (f x) = f (normalize x)) (a : α) :
{ x // x ∈ normalizedFactors a } ≃ { y // y ∈ normalizedFactors (f a) } :=
Equiv.subtypeEquiv f fun x ↦ by
rcases eq_or_ne a 0 with rfl | ha
· simp
·
simp [mem_normalizedFactors_iff' ha, mem_normalizedFactors_iff' (EmbeddingLike.map_ne_zero_iff.mpr ha),
map_dvd_iff_dvd_symm, MulEquiv.irreducible_iff, he]
