Theorems · Definition · ring theory

AlgEquiv.arrowCongr

{R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      {A₁' : Type uA₁'} →
        {A₂' : Type uA₂'} →
          [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₂'] → (A₁ ≃ₐ[R] A₁') → (A₂ ≃ₐ[R] A₂') → (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂')

If A₁ is equivalent to A₁' and A₂ is equivalent to A₂', then the type of maps A₁ →ₐ[R] A₂ is equivalent to the type of maps A₁' →ₐ[R] A₂'.

Defined in

Mathlib.Algebra.Algebra.Equiv

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebraAlgebra