algebraRat — Mathlib

English

Equal characteristic zero implies the existence of a ℚ-algebra structure on R modulo any nontrivial ideal.

Русский

Равная характеристика нулю влечёт существование структуры ℚ-алгебра на R/I для любого ненулевого идеала I.

LaTeX

$$$\\text{Algebra }\\mathbb{Q} \\; R$ and CharZero on quotients imply a universal ℚ-algebra structure.$$

Lean4

/-- Equal characteristic implies `ℚ`-algebra. -/
noncomputable def algebraRat (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) : Algebra ℚ R :=
  haveI : Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) := ⟨h⟩
  RingHom.toAlgebra
    { toFun := fun x => x.num /ₚ ↑x.pnatDen
      map_zero' := by simp [divp]
      map_one' := by simp
      map_mul' := by
        intro a b
        simp only [← divp_assoc, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul, divp_eq_iff_mul_eq, pnatCast_eq_natCast,
          Rat.coe_pnatDen, Units.val_mul]
        trans (↑((a * b).num * a.den * b.den) : R)
        · simp_rw [Int.cast_mul, Int.cast_natCast]
          ring
        rw [Rat.mul_num_den' a b]
        simp
      map_add' := by
        intro a b
        simp only [Units.add_divp, pnatCast_eq_natCast, Rat.coe_pnatDen, divp_mul_eq_mul_divp, Units.divp_add,
          divp_divp_eq_divp_mul, divp_eq_iff_mul_eq, Units.val_mul]
        trans (↑((a + b).num * a.den * b.den) : R)
        · simp_rw [Int.cast_mul, Int.cast_natCast]
          ring
        rw [Rat.add_num_den' a b]
        simp }

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