Theorems · Theorem · commutative algebra

LinearEquiv.arrowCongrAddEquiv_symm_apply

∀ {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 σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₂ →ₛₗ[σ₂₂'] M₂'), (e₁.arrowCongrAddEquiv e₂).symm f = (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringSemiringSemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTriple