Theorems · Definition · ring theory

MoritaEquivalence.mk.noConfusion

{R : Type u₀} →
  {inst : CommSemiring R} →
    {A : Type u₁} →
      {inst_1 : Ring A} →
        {inst_2 : Algebra R A} →
          {B : Type u₂} →
            {inst_3 : Ring B} →
              {inst_4 : Algebra R B} →
                {P : Sort u} →
                  {eqv : ModuleCat A ≌ ModuleCat B} →
                    {linear :
                        autoParam (CategoryTheory.Functor.Linear R eqv.functor) MoritaEquivalence.linear._autoParam} →
                      {eqv' : ModuleCat A ≌ ModuleCat B} →
                        {linear' :
                            autoParam (CategoryTheory.Functor.Linear R eqv'.functor)
                              MoritaEquivalence.linear._autoParam} →
                          { eqv := eqv, linear := linear } = { eqv := eqv', linear := linear' } → (eqv ≍ eqv' → P) → P

Defined in

Mathlib.RingTheory.Morita.Basic

Cited by

1 results in Mathlib

Foundations

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