exists_apply_ne_one_iff_exists_monoidHom

English

There exists a (nonempty) equivalence between MulChar M R and Mˣ when roots of unity exist sufficiently many.

Русский

Существует непустое эквивалентное отображение между MulChar M R и Mˣ при наличии достаточного числа корней ед.

LaTeX

$$Nonempty (MulChar M R ≃* Mˣ)$$

Lean4

theorem exists_apply_ne_one_iff_exists_monoidHom (a : Mˣ) : (∃ χ : MulChar M R, χ a ≠ 1) ↔ ∃ φ : Mˣ →* Rˣ, φ a ≠ 1 :=
  by
  refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩
  · contrapose! hχ
    rwa [Units.ext_iff, coe_toUnitHom] at hχ
  · contrapose! hφ
    simpa only [ofUnitHom_eq, equivToUnitHom_symm_coe, Units.val_eq_one] using hφ

Похожие утверждения