LeanPool.BrauerGroupNew.Azumaya.Mul

Imported Lean Pool material for LeanPool.BrauerGroupNew.Azumaya.Mul.

@[reducible, inline]

noncomputable abbrev nn (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : ℕ

The rank of a finite free module used to split a finite projective module.

Equations

• nn R M = ⋯.choose

@[reducible, inline]

noncomputable abbrev f0 (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : (Fin (nn R M) → R) →ₗ[R] M

The surjective map from a finite free module onto a finite projective module.

Equations

• f0 R M = ⋯.choose

@[reducible, inline]

noncomputable abbrev g0 (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : M →ₗ[R] Fin (nn R M) → R

The injective splitting map from a finite projective module into a finite free module.

Equations

• g0 R M = ⋯.choose

theorem f0_surj (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Function.Surjective ⇑(f0 R M)

theorem g0_inj (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Function.Injective ⇑(g0 R M)

theorem fg (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : f0 R M ∘ₗ g0 R M = LinearMap.id

@[reducible, inline]

noncomputable abbrev inclusion1 (R : Type u) [CommRing R] (M : Type u_1) (P : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [AddCommGroup P] [Module R P] : (M →ₗ[R] P) →ₗ[R] (Fin (nn R M) → R) →ₗ[R] P

Precomposition with f0, embedding maps out of M into maps out of a finite free module.

Equations

• inclusion1 R M P = { toFun := fun (f : M →ₗ[R] P) => f ∘ₗ f0 R M, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev projection1 (R : Type u) [CommRing R] (M : Type u_1) (P : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [AddCommGroup P] [Module R P] : ((Fin (nn R M) → R) →ₗ[R] P) →ₗ[R] M →ₗ[R] P

Precomposition with g0, projecting maps from the finite free cover back to maps out of M.

Equations

• projection1 R M P = { toFun := fun (f : (Fin (nn R M) → R) →ₗ[R] P) => f ∘ₗ g0 R M, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev tensorInclusion1 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q) →ₗ[R] TensorProduct R ((Fin (nn R M) → R) →ₗ[R] P) ((Fin (nn R N) → R) →ₗ[R] Q)

Hom(M, P) ⊗ Hom(N, Q) →ₗ[R] Hom(Rⁿ, P) ⊗ Hom(Rᵐ, Q)

Equations

• tensorInclusion1 R M N P Q = TensorProduct.map (inclusion1 R M P) (inclusion1 R N Q)

@[reducible, inline]

noncomputable abbrev tensorProjection1 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : TensorProduct R ((Fin (nn R M) → R) →ₗ[R] P) ((Fin (nn R N) → R) →ₗ[R] Q) →ₗ[R] TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)

Tensor product of the two first projection maps.

Equations

• tensorProjection1 R M N P Q = TensorProduct.map (projection1 R M P) (projection1 R N Q)

theorem projection_inlusion1 (R : Type u) [CommRing R] (M : Type u_1) (P : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [AddCommGroup P] [Module R P] : projection1 R M P ∘ₗ inclusion1 R M P = LinearMap.id

theorem tensorInclusion1_projection1 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : tensorProjection1 R M N P Q ∘ₗ tensorInclusion1 R M N P Q = LinearMap.id

theorem tensorInclusion1_projection1_apply (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] (x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)) : (tensorProjection1 R M N P Q) ((tensorInclusion1 R M N P Q) x) = x

theorem tensorInclusion1_inj (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : Function.Injective ⇑(tensorInclusion1 R M N P Q)

theorem Tensor_isDirectSummand (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] : ∃ (s0 : TensorProduct R M N →ₗ[R] TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R)) (s1 : TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R) →ₗ[R] TensorProduct R M N), s1 ∘ₗ s0 = LinearMap.id

@[reducible, inline]

noncomputable abbrev inclusion2 {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] : TensorProduct R M N →ₗ[R] TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R)

The tensor-product inclusion induced by the free-module splittings of M and N.

Equations

• inclusion2 = TensorProduct.map (g0 R M) (g0 R N)

@[reducible, inline]

noncomputable abbrev projection2 {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] : TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R) →ₗ[R] TensorProduct R M N

The tensor-product projection induced by the free-module covers of M and N.

Equations

• projection2 = TensorProduct.map (f0 R M) (f0 R N)

@[reducible, inline]

noncomputable abbrev tensorInclusion2 (R : Type u) [CommRing R] {M : Type u_1} {N : Type u_2} (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : (TensorProduct R M N →ₗ[R] TensorProduct R P Q) →ₗ[R] TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R) →ₗ[R] TensorProduct R P Q

Precomposition with projection2 on homs out of M ⊗ N.

Equations

• tensorInclusion2 R P Q = { toFun := fun (f : TensorProduct R M N →ₗ[R] TensorProduct R P Q) => f ∘ₗ projection2, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev tensorProjection2 (R : Type u) [CommRing R] {M : Type u_1} {N : Type u_2} (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : (TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R) →ₗ[R] TensorProduct R P Q) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P Q

Precomposition with inclusion2 on homs out of the finite free tensor product.

Equations

• tensorProjection2 R P Q = { toFun := fun (f : TensorProduct R (Fin (nn R M) → R) (Fin (nn R N) → R) →ₗ[R] TensorProduct R P Q) => f ∘ₗ inclusion2, map_add' := ⋯, map_smul' := ⋯ }

theorem projection2_inclusion2 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] : projection2 ∘ₗ inclusion2 = LinearMap.id

theorem projection2_inclusion2_apply (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (x : TensorProduct R M N) : projection2 (inclusion2 x) = x

theorem tensorProjection2_inclusion2 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : tensorProjection2 R P Q ∘ₗ tensorInclusion2 R P Q = LinearMap.id

theorem tensorInclusion2_inj (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : Function.Injective ⇑(tensorInclusion2 R P Q)

theorem comm_square2 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : ↑(homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q) ∘ₗ tensorInclusion1 R M N P Q = tensorInclusion2 R P Q ∘ₗ TensorProduct.homTensorHomMap (RingHom.id R) M N P Q

This proves the following square commutes: TensorProduct.homTensorHomMap Hom(M, P) ⊗ Hom(N, Q) ---------------> Hom(M ⊗ N, P ⊗ Q) | | | | i | | j i' | | j' | | | | | | | | Hom(Rⁿ, P) ⊗ Hom(Rᵐ, Q) -------------> Hom(Rⁿ ⊗ Rᵐ, P ⊗ Q)

theorem comm_square2_apply (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] (f : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)) : ↑(homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q) ((tensorInclusion1 R M N P Q) f) = (tensorInclusion2 R P Q) ((TensorProduct.homTensorHomMap (RingHom.id R) M N P Q) f)

theorem homTensorHomMap_inj (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : Function.Injective ⇑(TensorProduct.homTensorHomMap (RingHom.id R) M N P Q)

theorem comm_square3 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : ↑(homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q) ∘ₗ tensorInclusion1 R M N P Q ∘ₗ tensorProjection1 R M N P Q = tensorInclusion2 R P Q ∘ₗ tensorProjection2 R P Q ∘ₗ ↑(homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q)

theorem comm_square3_apply (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] (f : TensorProduct R ((Fin (nn R M) → R) →ₗ[R] P) ((Fin (nn R N) → R) →ₗ[R] Q)) : (homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q) ((tensorInclusion1 R M N P Q) ((tensorProjection1 R M N P Q) f)) = (tensorInclusion2 R P Q) ((tensorProjection2 R P Q) ((homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q) f))

theorem comm_square1 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : tensorProjection1 R M N P Q ∘ₗ ↑(homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q).symm ∘ₗ tensorInclusion2 R P Q ∘ₗ TensorProduct.homTensorHomMap (RingHom.id R) M N P Q = LinearMap.id

theorem comm_square4 (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : TensorProduct.homTensorHomMap (RingHom.id R) M N P Q ∘ₗ tensorProjection1 R M N P Q ∘ₗ ↑(homTensorHomEquiv R (Fin (nn R M) → R) (Fin (nn R N) → R) P Q).symm ∘ₗ tensorInclusion2 R P Q = LinearMap.id

theorem homTensorHomMap_surj (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) (P : Type u_3) (Q : Type u_4) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] [AddCommGroup P] [AddCommGroup Q] [Module R P] [Module R Q] : Function.Surjective ⇑(TensorProduct.homTensorHomMap (RingHom.id R) M N P Q)

structure Azumaya (R : Type u) [CommRing R] extends AlgCat R : Type (max u (u_1 + 1))

An Azumaya algebra over a commutative base ring, bundled as an algebra object.

• carrier : Type u_1
• isRing : Ring ↑self.toAlgCat
• isAlgebra : Algebra R ↑self.toAlgCat
• isAzumaya : IsAzumaya R ↑self.toAlgCat

@[implicit_reducible]

noncomputable instance instCoeSortAzumayaType (R : Type u) [CommRing R] : CoeSort (Azumaya R) (Type v)

Equations

• ↑R = { coe := fun (s : Azumaya R) => ↑s.toAlgCat }

noncomputable def Azumaya.IsMoritaEquivalent (R : Type u) [CommRing R] : Azumaya R → Azumaya R → Prop

Morita equivalence of the carrier algebras of two bundled Azumaya algebras.

Equations

• Azumaya.IsMoritaEquivalent R A B = IsMoritaEquivalent R ↑A.toAlgCat ↑B.toAlgCat

theorem Azumaya.IsMoritaEquivalent.iff (R : Type u) [CommRing R] {A : Azumaya R} {B : Azumaya R} : IsMoritaEquivalent R A B ↔ _root_.IsMoritaEquivalent R ↑A.toAlgCat ↑B.toAlgCat

theorem AzuMorita.equiv (R : Type u) [CommRing R] : Equivalence (Azumaya.IsMoritaEquivalent R)

@[reducible, inline]

noncomputable abbrev AzumayaSetoid (R : Type u) [CommRing R] : Setoid (Azumaya R)

The setoid on Azumaya algebras induced by Morita equivalence.

Equations

• AzumayaSetoid R = { r := Azumaya.IsMoritaEquivalent R, iseqv := ⋯ }

instance Azumaya.instFiniteTensorProduct (R : Type u) [CommRing R] (A B : Type v) [Ring A] [Ring B] [Algebra R A] [Algebra R B] [Module.Finite R A] [Module.Finite R B] : Module.Finite R (TensorProduct R A B)

instance Azumaya.faithfulSMulTensor {R : Type u} [CommRing R] {A B : Type v} [Ring A] [Ring B] [Algebra R A] [Algebra R B] [Module.Projective R A] [Module.Projective R B] [FaithfulSMul R A] [FaithfulSMul R B] : FaithfulSMul R (TensorProduct R A B)

@[reducible, inline]

noncomputable abbrev Azumaya.e {R : Type u} [CommRing R] {A B : Type v} [Ring A] [Ring B] [Algebra R A] [Algebra R B] : TensorProduct R (TensorProduct R A Aᵐᵒᵖ) (TensorProduct R B Bᵐᵒᵖ) ≃ₐ[R] TensorProduct R (TensorProduct R A B) (TensorProduct R A B)ᵐᵒᵖ

Rebracketing equivalence used to compare mulLeftRight with tensor products.

Equations

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

theorem Azumaya.e_apply (R : Type u) [CommRing R] (A B : Type v) [Ring A] [Ring B] [Algebra R A] [Algebra R B] (a : A) (b : B) (a' : Aᵐᵒᵖ) (b' : Bᵐᵒᵖ) : e (a ⊗ₜ[R] a' ⊗ₜ[R] (b ⊗ₜ[R] b')) = a ⊗ₜ[R] b ⊗ₜ[R] MulOpposite.op (MulOpposite.unop a' ⊗ₜ[R] MulOpposite.unop b')

theorem Azumaya.top_square_comm'' (R : Type u) [CommRing R] (A B : Azumaya R) : TensorProduct.homTensorHomMap (RingHom.id R) ↑A.toAlgCat ↑B.toAlgCat ↑A.toAlgCat ↑B.toAlgCat ∘ₗ (Algebra.TensorProduct.congr (AlgEquiv.ofBijective (AlgHom.mulLeftRight R ↑A.toAlgCat) ⋯) (AlgEquiv.ofBijective (AlgHom.mulLeftRight R ↑B.toAlgCat) ⋯)).toLinearMap = (AlgHom.mulLeftRight R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat)).toLinearMap ∘ₗ ↑↑e

theorem Azumaya.top_square_comm (R : Type u) [CommRing R] (A B : Azumaya R) : ⇑(TensorProduct.homTensorHomMap (RingHom.id R) ↑A.toAlgCat ↑B.toAlgCat ↑A.toAlgCat ↑B.toAlgCat) ∘ ⇑(Algebra.TensorProduct.congr (AlgEquiv.ofBijective (AlgHom.mulLeftRight R ↑A.toAlgCat) ⋯) (AlgEquiv.ofBijective (AlgHom.mulLeftRight R ↑B.toAlgCat) ⋯)) = ⇑(AlgHom.mulLeftRight R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat)) ∘ ⇑e

theorem Azumaya.bij_homtensorhom (R : Type u) [CommRing R] (A B : Azumaya R) : Function.Bijective ⇑(TensorProduct.homTensorHomMap (RingHom.id R) ↑A.toAlgCat ↑B.toAlgCat ↑A.toAlgCat ↑B.toAlgCat)

A ⊗ Aᵐᵒᵖ ⊗ B ⊗ B ᵐᵒᵖ --------> (A ⊗ B) ⊗ (A ⊗ B)ᵐᵒᵖ | | | | | | | | f ⊗ g ----> f ⊗ g End R A ⊗ End R B ---------------> End R (A ⊗ B) | | | | i | | j i' | | j' | | | | | | homTensorHomEquiv | | End R Rⁿ ⊗ End R Rᵐ -------------> End R (Rⁿ ⊗ Rᵐ)

@[reducible, inline]

noncomputable abbrev Azumaya.e1 (R : Type u) [CommRing R] (A B : Azumaya R) : TensorProduct R (Module.End R ↑A.toAlgCat) (Module.End R ↑B.toAlgCat) ≃ₗ[R] Module.End R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat)

The hom-tensor-hom equivalence for the carriers of two Azumaya algebras.

Equations

• Azumaya.e1 R A B = LinearEquiv.ofBijective (TensorProduct.homTensorHomMap (RingHom.id R) ↑A.toAlgCat ↑B.toAlgCat ↑A.toAlgCat ↑B.toAlgCat) ⋯

@[reducible, inline]

noncomputable abbrev Azumaya.e2 (R : Type u) [CommRing R] (A : Azumaya R) (B : Azumaya R) : TensorProduct R (TensorProduct R (↑A.toAlgCat) (↑A.toAlgCat)ᵐᵒᵖ) (TensorProduct R (↑B.toAlgCat) (↑B.toAlgCat)ᵐᵒᵖ) ≃ₐ[R] TensorProduct R (Module.End R ↑A.toAlgCat) (Module.End R ↑B.toAlgCat)

The tensor-product equivalence induced by the two mulLeftRight bijections.

Equations

• Azumaya.e2 R A B = Algebra.TensorProduct.congr (AlgEquiv.ofBijective (AlgHom.mulLeftRight R ↑A.toAlgCat) ⋯) (AlgEquiv.ofBijective (AlgHom.mulLeftRight R ↑B.toAlgCat) ⋯)

theorem Azumaya.top_square_comm_apply (R : Type u) [CommRing R] (A B : Azumaya R) (x : TensorProduct R (TensorProduct R (↑A.toAlgCat) (↑A.toAlgCat)ᵐᵒᵖ) (TensorProduct R (↑B.toAlgCat) (↑B.toAlgCat)ᵐᵒᵖ)) : (e1 R A B) ((e2 R A B) x) = (AlgHom.mulLeftRight R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat)) (↑e x)

theorem Azumaya.bij_mulLeftRight (R : Type u) [CommRing R] (A B : Azumaya R) : Function.Bijective ⇑(AlgHom.mulLeftRight R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat))

@[reducible, inline]

noncomputable abbrev Azumaya.mul (R : Type u) [CommRing R] (A B : Azumaya R) : Azumaya R

Tensor product of bundled Azumaya algebras.

Equations

• Azumaya.mul R A B = { toAlgCat := AlgCat.of R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat), isAzumaya := ⋯ }

@[implicit_reducible]

noncomputable instance Azumaya.instMul (R : Type u) [CommRing R] : Mul (Azumaya R)

Equations

• Azumaya.instMul R = { mul := fun (A B : Azumaya R) => Azumaya.mul R A B }

theorem Azumaya.mul_coe (R : Type u) [CommRing R] (A B : Azumaya R) : A * B = { toAlgCat := AlgCat.of R (TensorProduct R ↑A.toAlgCat ↑B.toAlgCat), isAzumaya := ⋯ }

@[implicit_reducible]

noncomputable instance Azumaya.instOne (R : Type u) [CommRing R] : One (Azumaya R)

Equations

• Azumaya.instOne R = { one := { toAlgCat := AlgCat.of R R, isAzumaya := ⋯ } }

instance Azumaya.instFaithfulSMulMulOpposite (R : Type u) [CommRing R] : FaithfulSMul R Rᵐᵒᵖ

theorem Azumaya.small_comm_square (R : Type u) [CommRing R] (A B : Type v) [Ring A] [Ring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) = (↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)

A ⊗ Aᵐᵒᵖ ------------> B ⊗ Bᵐᵒᵖ | | | | | | | | End R A ------------> End R B

theorem IsAzumaya.ofAlgEquiv (R : Type u) [CommRing R] (A B : Type v) [Ring A] [Ring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (hA : IsAzumaya R A) : IsAzumaya R B

@[reducible, inline]

noncomputable abbrev Azumaya.inclusion' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.End R M →ₗ[R] Module.End R (Fin (nn R M) → R)

Inclusion of endomorphisms induced by a finite free cover of a projective module.

Equations

• Azumaya.inclusion' R M = { toFun := fun (f : Module.End R M) => g0 R M ∘ₗ f ∘ₗ f0 R M, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev Azumaya.projection' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.End R (Fin (nn R M) → R) →ₗ[R] Module.End R M

Projection of endomorphisms induced by a splitting of the finite free cover.

Equations

• Azumaya.projection' R M = { toFun := fun (f : Module.End R (Fin (nn R M) → R)) => f0 R M ∘ₗ f ∘ₗ g0 R M, map_add' := ⋯, map_smul' := ⋯ }

theorem Azumaya.projection'_inclusion' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : projection' R M ∘ₗ inclusion' R M = LinearMap.id

theorem Azumaya.projection'_surj (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Function.Surjective ⇑(projection' R M)

theorem Module.Projective.ofEnd (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : Projective R (End R M)

instance Module.Finite.End (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : Module.Finite R (Module.End R M)

instance Azumaya.instFaithfulSMulEnd (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [FaithfulSMul R M] : FaithfulSMul R (Module.End R M)

@[reducible, inline]

noncomputable abbrev Azumaya.MatrixAlg (R : Type u) [CommRing R] (n : ℕ) [NeZero n] : Azumaya R

The matrix algebra as a bundled Azumaya algebra.

Equations

• Azumaya.MatrixAlg R n = { toAlgCat := AlgCat.of R (Matrix (Fin n) (Fin n) R), isAzumaya := ⋯ }

@[reducible, inline]

noncomputable abbrev Azumaya.EndRn (R : Type u) [CommRing R] (n : ℕ) [NeZero n] : Azumaya R

The endomorphism algebra of R^n as a bundled Azumaya algebra.

Equations

• Azumaya.EndRn R n = { toAlgCat := AlgCat.of R (Module.End R (Fin n → R)), isAzumaya := ⋯ }

@[reducible, inline]

noncomputable abbrev Azumaya.tensorInclusion1' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : TensorProduct R (Module.End R M) (Module.End R M)ᵐᵒᵖ →ₗ[R] TensorProduct R (Module.End R (Fin (nn R M) → R)) (Module.End R (Fin (nn R M) → R))ᵐᵒᵖ

Tensor inclusion on endomorphism algebras induced by inclusion'.

Equations

• Azumaya.tensorInclusion1' R M = TensorProduct.map (Azumaya.inclusion' R M) (↑(MulOpposite.opLinearEquiv R) ∘ₗ Azumaya.inclusion' R M ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm)

@[reducible, inline]

noncomputable abbrev Azumaya.tensorProjection1' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : TensorProduct R (Module.End R (Fin (nn R M) → R)) (Module.End R (Fin (nn R M) → R))ᵐᵒᵖ →ₗ[R] TensorProduct R (Module.End R M) (Module.End R M)ᵐᵒᵖ

Tensor projection on endomorphism algebras induced by projection'.

Equations

• Azumaya.tensorProjection1' R M = TensorProduct.map (Azumaya.projection' R M) (↑(MulOpposite.opLinearEquiv R) ∘ₗ Azumaya.projection' R M ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm)

theorem Azumaya.tensor_projection_inclusion1' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : tensorProjection1' R M ∘ₗ tensorInclusion1' R M = LinearMap.id

theorem Azumaya.tensorInclusion1'_inj (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Function.Injective ⇑(tensorInclusion1' R M)

@[reducible, inline]

noncomputable abbrev Azumaya.inclusion2' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.End R (Module.End R M) →ₗ[R] Module.End R (Module.End R (Fin (nn R M) → R))

Inclusion between second endomorphism algebras induced by the free-module splitting.

Equations

• Azumaya.inclusion2' R M = { toFun := fun (f : Module.End R (Module.End R M)) => Azumaya.inclusion' R M ∘ₗ f ∘ₗ Azumaya.projection' R M, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev Azumaya.projection2' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.End R (Module.End R (Fin (nn R M) → R)) →ₗ[R] Module.End R (Module.End R M)

Projection between second endomorphism algebras induced by the free-module splitting.

Equations

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

theorem Azumaya.projection2'_inclusion2' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : projection2' R M ∘ₗ inclusion2' R M = LinearMap.id

theorem Azumaya.projection2'_surj (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Function.Surjective ⇑(projection2' R M)

theorem Azumaya.comm_square_endend (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : inclusion2' R M ∘ₗ (AlgHom.mulLeftRight R (Module.End R M)).toLinearMap = (AlgHom.mulLeftRight R (Module.End R (Fin (nn R M) → R))).toLinearMap ∘ₗ tensorInclusion1' R M

End R M ⊗ (End R M)ᵐᵒᵖ ------------> End R (End R M) | | | | | | | | | | | | | | | | End R Rⁿ ⊗ (End R Rⁿ)ᵐᵒᵖ ----------> End R (End R Rⁿ)

theorem Azumaya.comm_square_endend' (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : (AlgHom.mulLeftRight R (Module.End R M)).toLinearMap ∘ₗ tensorProjection1' R M = projection2' R M ∘ₗ (AlgHom.mulLeftRight R (Module.End R (Fin (nn R M) → R))).toLinearMap

instance Azumaya.instNeZeroNatNn (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial M] : NeZero (nn R M)

theorem Azumaya.inj_endM (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial M] : Function.Injective ⇑(AlgHom.mulLeftRight R (Module.End R M))

theorem Azumaya.surj_endM (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial M] : Function.Surjective ⇑(AlgHom.mulLeftRight R (Module.End R M))

theorem Azumaya.bij_endM (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial M] : Function.Bijective ⇑(AlgHom.mulLeftRight R (Module.End R M))

@[reducible, inline]

noncomputable abbrev Azumaya.ofEnd (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial M] [FaithfulSMul R M] : Azumaya R

The endomorphism algebra of a faithful finite projective module is Azumaya.

Equations

• Azumaya.ofEnd R M = { toAlgCat := AlgCat.of R (Module.End R M), isAzumaya := ⋯ }