Theorems · Theorem · commutative algebra

TensorProduct.congr_trans

∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M] [inst_10 : Module R N] [inst_11 : Module R₂ M₂]
  [inst_12 : Module R₂ N₂] [inst_13 : Module R₃ M₃] [inst_14 : Module R₃ N₃] {σ₂₁ : R₂ →+* R}
  [inst_15 : RingHomInvPair σ₁₂ σ₂₁] [inst_16 : RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂}
  [inst_17 : RingHomInvPair σ₂₃ σ₃₂] [inst_18 : RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R}
  [inst_19 : RingHomInvPair σ₁₃ σ₃₁] [inst_20 : RingHomInvPair σ₃₁ σ₁₃] [inst_21 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_22 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂)
  (g₁ : N ≃ₛₗ[σ₁₂] N₂),
  TensorProduct.congr (f₁.trans f₂) (g₁.trans g₂) = (TensorProduct.congr f₁ g₁).trans (TensorProduct.congr f₂ g₂)

Defined in

Mathlib.LinearAlgebra.TensorProduct.Map

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleModuleModuleRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTriple