Theorems · Definition · commutative algebra

LinearEquiv.arrowCongrAddEquiv

{R₁ : Type u_9} →
  {R₂ : Type u_10} →
    {R₁' : Type u_11} →
      {R₂' : Type u_12} →
        {M₁ : Type u_13} →
          {M₂ : Type u_14} →
            {M₁' : Type u_15} →
              {M₂' : Type u_16} →
                [inst : Semiring R₁] →
                  [inst_1 : Semiring R₂] →
                    [inst_2 : Semiring R₁'] →
                      [inst_3 : Semiring R₂'] →
                        [inst_4 : AddCommMonoid M₁] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : AddCommMonoid M₁'] →
                              [inst_7 : AddCommMonoid M₂'] →
                                [inst_8 : Module R₁ M₁] →
                                  [inst_9 : Module R₂ M₂] →
                                    [inst_10 : Module R₁' M₁'] →
                                      [inst_11 : Module R₂' M₂'] →
                                        {σ₁₂ : R₁ →+* R₂} →
                                          {σ₂₁ : R₂ →+* R₁} →
                                            {σ₁'₂' : R₁' →+* R₂'} →
                                              {σ₂'₁' : R₂' →+* R₁'} →
                                                {σ₁₁' : R₁ →+* R₁'} →
                                                  {σ₂₂' : R₂ →+* R₂'} →
                                                    {σ₂₁' : R₂ →+* R₁'} →
                                                      {σ₁₂' : R₁ →+* R₂'} →
                                                        [inst_12 : RingHomInvPair σ₁₂ σ₂₁] →
                                                          [inst_13 : RingHomInvPair σ₂₁ σ₁₂] →
                                                            [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                                                              [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                                                                [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] →
                                                                  [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] →
                                                                    [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] →
                                                                      [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] →
                                                                        (M₁ ≃ₛₗ[σ₁₂] M₂) →
                                                                          (M₁' ≃ₛₗ[σ₁'₂'] M₂') →
                                                                            (M₁ →ₛₗ[σ₁₁'] M₁') ≃+ (M₂ →ₛₗ[σ₂₂'] M₂')

A linear isomorphism between the domains and codomains of two spaces of linear maps gives an additive isomorphism between the two function spaces. See also LinearEquiv.arrowCongr for the linear version of this isomorphism.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

SemiringSemiringSemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTriple