LeanPool.BrauerGroupNew.Morita.ChangeOfRings

Imported Lean Pool material for LeanPool.BrauerGroupNew.Morita.ChangeOfRings.

@[implicit_reducible]

instance ModuleCat.instLinearOfAlgebraLeanPool {R₀ : Type u_1} {S : Type u_2} [CommRing R₀] [Ring S] [Algebra R₀ S] : CategoryTheory.Linear R₀ (ModuleCat S)

Equations

• ModuleCat.instLinearOfAlgebraLeanPool = ModuleCat.Algebra.instLinear

instance ModuleCat.MoritaEquivalence.instAdditiveMatrixFinFunctorMoritaEquivalentToMatrix (A : Type u) [Ring A] (n : ℕ) [NeZero n] : (moritaEquivalentToMatrix A (Fin n)).functor.Additive

instance ModuleCat.MoritaEquivalence.instLinearMatrixFinFunctorMoritaEquivalentToMatrix (R : Type u₀) [CommRing R] (A : Type u) [Ring A] [Algebra R A] (n : ℕ) [NeZero n] : CategoryTheory.Functor.Linear R (moritaEquivalentToMatrix A (Fin n)).functor

noncomputable def ModuleCat.MoritaEquivalence.matrix (R : Type u₀) [CommRing R] (A : Type u) [Ring A] [Algebra R A] (n : ℕ) : MoritaEquivalence R A (Matrix (Fin (n + 1)) (Fin (n + 1)) A)

The Morita equivalence between a ring and a positive-size matrix ring over it.

Equations

• ModuleCat.MoritaEquivalence.matrix R A n = { eqv := moritaEquivalentToMatrix A (Fin (n + 1)), linear := ⋯ }

noncomputable def ModuleCat.MoritaEquivalence.matrix' (R : Type u₀) [CommRing R] (A : Type u) [Ring A] [Algebra R A] (n : ℕ) [hn : NeZero n] : MoritaEquivalence R A (Matrix (Fin n) (Fin n) A)

The Morita equivalence between a ring and an n × n matrix ring, for nonzero n.

Equations

• ModuleCat.MoritaEquivalence.matrix' R A n = { eqv := moritaEquivalentToMatrix A (Fin n), linear := ⋯ }

@[implicit_reducible]

noncomputable instance ModuleCat.MoritaEquivalence.instAlgebraEndOfLeanPool (R : Type u₀) [CommRing R] (A : Type u) [DivisionRing A] [Algebra R A] : Algebra R (CategoryTheory.End (of A A))

Equations

• ModuleCat.MoritaEquivalence.instAlgebraEndOfLeanPool R A = inferInstance

noncomputable def ModuleCat.MoritaEquivalence.mopToEnd (R : Type u₀) [CommRing R] (A : Type u) [DivisionRing A] [Algebra R A] : Aᵐᵒᵖ →ₐ[R] CategoryTheory.End (of A A)

Right multiplication identifies the opposite division ring with endomorphisms of its regular module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.MoritaEquivalence.mopToEnd_apply (R : Type u₀) [CommRing R] (A : Type u) [DivisionRing A] [Algebra R A] (a : Aᵐᵒᵖ) : (mopToEnd R A) a = ofHom { toFun := fun (x : A) => x * MulOpposite.unop a, map_add' := ⋯, map_smul' := ⋯ }

theorem ModuleCat.MoritaEquivalence.moptoend_bij (R : Type u₀) [CommRing R] (A : Type u) [DivisionRing A] [Algebra R A] : Function.Bijective ⇑(mopToEnd R A)

noncomputable def ModuleCat.MoritaEquivalence.mopAlgEquivEnd (R : Type u₀) [CommRing R] (A : Type u) [DivisionRing A] [Algebra R A] : Aᵐᵒᵖ ≃ₐ[R] CategoryTheory.End (of A A)

The opposite division ring is equivalent to endomorphisms of its regular module.

Equations

• ModuleCat.MoritaEquivalence.mopAlgEquivEnd R A = AlgEquiv.ofBijective (ModuleCat.MoritaEquivalence.mopToEnd R A) ⋯

noncomputable def ModuleCat.MoritaEquivalence.aux1 (R : Type u₀) [CommRing R] (A B : Type u) [DivisionRing A] [DivisionRing B] [Algebra R A] [Algebra R B] (e : MoritaEquivalence R A B) : CategoryTheory.End (of A A) ≃ₐ[R] CategoryTheory.End (e.eqv.functor.obj (of A A))

Transport endomorphism algebras along the functor of a Morita equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.MoritaEquivalence.aux20 (R : Type u₀) [CommRing R] (A B : Type u) [DivisionRing A] [DivisionRing B] [Algebra R A] [Algebra R B] (e : MoritaEquivalence R A B) : e.eqv.functor.obj (of A A) ≅ of B B

The target simple module associated to the source regular module under a Morita equivalence.

Equations

• ModuleCat.MoritaEquivalence.aux20 R A B e = ⋯.some.toModuleIso

noncomputable def ModuleCat.MoritaEquivalence.aux2 (R : Type u₀) [CommRing R] (B : Type u) [DivisionRing B] [Algebra R B] (M N : ModuleCat B) (f : M ≅ N) : CategoryTheory.End M ≃ₐ[R] CategoryTheory.End N

Conjugation by a module isomorphism gives an equivalence of endomorphism algebras.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.MoritaEquivalence.toRingMopEquiv (R : Type u₀) [CommRing R] (A B : Type u) [DivisionRing A] [DivisionRing B] [Algebra R A] [Algebra R B] (e : MoritaEquivalence R A B) : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ

A Morita equivalence between division rings induces an equivalence of opposite rings.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.MoritaEquivalence.toRingEquiv (R : Type u₀) [CommRing R] (A B : Type u) [DivisionRing A] [DivisionRing B] [Algebra R A] [Algebra R B] (e : MoritaEquivalence R A B) : A ≃ₐ[R] B

A Morita equivalence between division rings induces an algebra equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.MoritaEquivalence.algEquivOfDivisionRing (R : Type u) [CommRing R] (D₁ D₂ : Type v) [DivisionRing D₁] [DivisionRing D₂] [Algebra R D₁] [Algebra R D₂] (e : MoritaEquivalence R D₁ D₂) : D₁ ≃ₐ[R] D₂

Morita-equivalent division algebras over a commutative ring are algebra equivalent.

Equations

• ModuleCat.MoritaEquivalence.algEquivOfDivisionRing R D₁ D₂ e = ModuleCat.MoritaEquivalence.toRingEquiv R D₁ D₂ e