Theorems · Theorem · ring theory

StarAlgHom.mk_coe

∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B) (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
        { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r)
  (h₆ :
    ∀ (x : A),
      (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                    commutes' := h₅ }.toRingHom).toFun
          (star x) =
        star
          ((↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                      commutes' := h₅ }.toRingHom).toFun
            x)),
  { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses Quot.sound

Assumes

CommSemiringSemiringAlgebraStarSemiringAlgebraStar