Theorems · Inductive type · ring theory

IsAzumaya

(R : Type u_1) → (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop

An Azumaya algebra is a finitely generated, projective and faithful R-algebra where AlgHom.mulLeftRight R A : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A is an isomorphism.

Defined in

Mathlib.Algebra.Azumaya.Defs

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebra