Theorems · Definition · ring theory

StarAlgEquiv.arrowCongr

{R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      {A₁' : Type u_5} →
        {A₂' : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A₁] →
              [inst_2 : Semiring A₂] →
                [inst_3 : Semiring A₁'] →
                  [inst_4 : Semiring A₂'] →
                    [inst_5 : Algebra R A₁] →
                      [inst_6 : Algebra R A₂] →
                        [inst_7 : Algebra R A₁'] →
                          [inst_8 : Algebra R A₂'] →
                            [inst_9 : Star A₁] →
                              [inst_10 : Star A₂] →
                                [inst_11 : Star A₁'] →
                                  [inst_12 : Star A₂'] →
                                    (A₁ ≃⋆ₐ[R] A₁') → (A₂ ≃⋆ₐ[R] A₂') → (A₁ →⋆ₐ[R] A₂) ≃ (A₁' →⋆ₐ[R] A₂')

If A₁ is equivalent to A₁' and A₂ is equivalent to A₂' as star algebras, then the type of maps A₁ →⋆ₐ[R] A₂ is equivalent to the type of maps A₁' →⋆ₐ[R] A₂'. For non-unital star algebra homomorphisms, see StarAlgEquiv.arrowCongr'.

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

5 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebraAlgebraStarStarStarStar