Theorems · Inductive type · ring theory

MoritaEquivalence

(R : Type u₀) →
  [inst : CommSemiring R] →
    (A : Type u₁) →
      [inst_1 : Ring A] →
        [Algebra R A] → (B : Type u₂) → [inst_3 : Ring B] → [Algebra R B] → Type (max (u₁ + 1) (u₂ + 1))

Let A and B be R-algebras. A Morita equivalence between A and B is an R-linear equivalence between the categories of A-modules and B-modules.

Defined in

Mathlib.RingTheory.Morita.Basic

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringRingAlgebraRingAlgebra