The free product of $R$-algebras

We define the free product of an indexed collection of (noncommutative) $R$-algebras (i : ι) → A i, with Algebra R (A i) for all i and R a commutative semiring, as the quotient of the tensor algebra on the direct sum ⨁ (i : ι), A i by the relation generated by extending the relation

• aᵢ ⊗ₜ aᵢ' ~ aᵢ aᵢ' for all i : ι and aᵢ aᵢ' : A i
• 1ᵢ ~ 1ⱼ for 1ᵢ := One.one (A i) and for all i, j : ι.

to the whole tensor algebra in an R-linear way.

The main result of this file is the universal property of the free product, which establishes the free product as the coproduct in the category of general $R$-algebras. (In the category of commutative $R$-algebras, the coproduct is just PiTensorProduct.)

Main definitions

• FreeProduct R A is the free product of the R-algebras A i, defined as a quotient of the tensor algebra on the direct sum of the A i.
• FreeProduct_ofPowers R A is the free product of the R-algebras A i, defined as a quotient of the (infinite) direct sum of tensor powers of the A i.
• lift is the universal property of the free product.

Main results

• equivPowerAlgebra establishes an equivalence between FreeProduct R A and FreeProduct_ofPowers R A.
• FreeProduct is the coproduct in the category of R-algebras.

TODO

• Induction principle for FreeProduct

theorem DirectSum.induction_lon {R : Type u_1} [Semiring R] {ι : Type u_2} [DecidableEq ι] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {C : (DirectSum ι fun (i : ι) => M i) → Prop} (x : DirectSum ι fun (i : ι) => M i) (H_zero : C 0) (H_basic : ∀ (i : ι) (x : M i), C ((DirectSum.lof R ι M i) x)) (H_plus : ∀ (x y : DirectSum ι fun (i : ι) => M i), C x → C y → C (x + y)) : C x

A variant of DirectSum.induction_on that uses DirectSum.lof instead of .of

def RingQuot.algEquiv_quot_algEquiv {R : Type u} [CommSemiring R] {A : Type v} {B : Type v} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (rel : A → A → Prop) : RingQuot rel ≃ₐ[R] RingQuot (rel on ⇑f.symm)

If two R-algebras are R-equivalent and their quotients by a relation rel are defined, then their quotients are also R-equivalent.

(Special case of the third isomorphism theorem.)

Equations

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

def RingQuot.equiv_quot_equiv {A : Type v} {B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : A → A → Prop) : RingQuot rel ≃+* RingQuot (rel on ⇑f.symm)

If two (semi)rings are equivalent and their quotients by a relation rel are defined, then their quotients are also equivalent.

(Special case of algEquiv_quot_algEquiv when R = ℕ, which in turn is a special case of the third isomorphism theorem.)

Equations

• RingQuot.equiv_quot_equiv f rel = (RingQuot.algEquiv_quot_algEquiv (AlgEquiv.ofRingEquiv ⋯) rel).toRingEquiv

instance LinearAlgebra.FreeProduct.instModuleDirectSum {I : Type u} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Module R (DirectSum I fun (i : I) => A i)

Equations

• LinearAlgebra.FreeProduct.instModuleDirectSum R A = inferInstance

@[reducible, inline]

abbrev LinearAlgebra.FreeProduct.FreeTensorAlgebra {I : Type u} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Type (max v w u)

The free tensor algebra over a direct sum of R-algebras, before taking the quotient by the free product relation.

Equations

• LinearAlgebra.FreeProduct.FreeTensorAlgebra R A = TensorAlgebra R (DirectSum I fun (i : I) => A i)

@[reducible, inline]

abbrev LinearAlgebra.FreeProduct.PowerAlgebra {I : Type u} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Type (max (max w u) v)

The direct sum of tensor powers of a direct sum of R-algebras, before taking the quotient by the free product relation.

Equations

• LinearAlgebra.FreeProduct.PowerAlgebra R A = DirectSum ℕ fun (n : ℕ) => TensorPower R n (DirectSum I fun (i : I) => A i)

@[reducible]

noncomputable def LinearAlgebra.FreeProduct.powerAlgebra_equiv_freeAlgebra {I : Type u} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : LinearAlgebra.FreeProduct.PowerAlgebra R A ≃ₐ[R] LinearAlgebra.FreeProduct.FreeTensorAlgebra R A

The free tensor algebra and its representation as an infinite direct sum of tensor powers are (noncomputably) equivalent as R-algebras.

Equations

• LinearAlgebra.FreeProduct.powerAlgebra_equiv_freeAlgebra R A = TensorAlgebra.equivDirectSum.symm

inductive LinearAlgebra.FreeProduct.rel {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : LinearAlgebra.FreeProduct.FreeTensorAlgebra R A → LinearAlgebra.FreeProduct.FreeTensorAlgebra R A → Prop

The generating equivalence relation for elements of the free tensor algebra that are identified in the free product.

• id: ∀ {I : Type u} [inst : DecidableEq I] {R : Type v} [inst_1 : CommSemiring R] {A : I → Type w} [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {i : I}, LinearAlgebra.FreeProduct.rel R A ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1
• prod: ∀ {I : Type u} [inst : DecidableEq I] {R : Type v} [inst_1 : CommSemiring R] {A : I → Type w} [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {i : I} {a₁ a₂ : A i}, LinearAlgebra.FreeProduct.rel R A ((TensorAlgebra.tprod R (DirectSum I fun (i : I) => A i) 2) fun (x : Fin 2) => match x with | 0 => (DirectSum.lof R I A i) a₁ | 1 => (DirectSum.lof R I A i) a₂) ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) (a₁ * a₂)))

@[reducible]

def LinearAlgebra.FreeProduct.rel' {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : (DirectSum ℕ fun (n : ℕ) => TensorPower R n (DirectSum I fun (i : I) => A i)) → (DirectSum ℕ fun (n : ℕ) => TensorPower R n (DirectSum I fun (i : I) => A i)) → Prop

The generating equivalence relation for elements of the power algebra that are identified in the free product.

Equations

• LinearAlgebra.FreeProduct.rel' R A = (LinearAlgebra.FreeProduct.rel R A on ⇑TensorAlgebra.ofDirectSum)

theorem LinearAlgebra.FreeProduct.rel_id {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) : LinearAlgebra.FreeProduct.rel R A ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1

@[reducible]

def LinearAlgebra.FreeProduct {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Type (max (max u v) w)

The free product of the collection of R-algebras A i, as a quotient of FreeTensorAlgebra R A.

Equations

• LinearAlgebra.FreeProduct R A = RingQuot (LinearAlgebra.FreeProduct.rel R A)

@[reducible]

def LinearAlgebra.FreeProduct_ofPowers {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Type (max (max u v) w)

The free product of the collection of R-algebras A i, as a quotient of PowerAlgebra R A

Equations

• LinearAlgebra.FreeProduct_ofPowers R A = RingQuot (LinearAlgebra.FreeProduct.rel' R A)

noncomputable def LinearAlgebra.FreeProduct.equivPowerAlgebra {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : LinearAlgebra.FreeProduct_ofPowers R A ≃ₐ[R] LinearAlgebra.FreeProduct R A

The R-algebra equivalence relating FreeProduct and FreeProduct_ofPowers

Equations

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

instance LinearAlgebra.FreeProduct.instSemiring {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Semiring (LinearAlgebra.FreeProduct R A)

Equations

• LinearAlgebra.FreeProduct.instSemiring R A = inferInstance

instance LinearAlgebra.FreeProduct.instAlgebra {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : Algebra R (LinearAlgebra.FreeProduct R A)

Equations

• LinearAlgebra.FreeProduct.instAlgebra R A = inferInstance

@[reducible, inline]

abbrev LinearAlgebra.FreeProduct.mkAlgHom {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : LinearAlgebra.FreeProduct.FreeTensorAlgebra R A →ₐ[R] LinearAlgebra.FreeProduct R A

The canonical quotient map FreeTensorAlgebra R A →ₐ[R] FreeProduct R A, as an R-algebra homomorphism.

Equations

• LinearAlgebra.FreeProduct.mkAlgHom R A = RingQuot.mkAlgHom R (LinearAlgebra.FreeProduct.rel R A)

@[reducible, inline]

abbrev LinearAlgebra.FreeProduct.ι' {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : (DirectSum I fun (i : I) => A i) →ₗ[R] LinearAlgebra.FreeProduct R A

The canonical linear map from the direct sum of the A i to the free product.

Equations

• LinearAlgebra.FreeProduct.ι' R A = (LinearAlgebra.FreeProduct.mkAlgHom R A).toLinearMap ∘ₗ TensorAlgebra.ι R

@[simp]

theorem LinearAlgebra.FreeProduct.ι_apply {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : DirectSum I fun (i : I) => A i) : { toQuot := Quot.mk (RingQuot.Rel (LinearAlgebra.FreeProduct.rel R A)) ((TensorAlgebra.ι R) x) } = (LinearAlgebra.FreeProduct.ι' R A) x

theorem LinearAlgebra.FreeProduct.identify_one {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) : (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) 1) = 1

The injection into the free product of any 1 : A i is the 1 of the free product.

theorem LinearAlgebra.FreeProduct.mul_injections {I : Type u} [DecidableEq I] {i : I} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (a₁ : A i) (a₂ : A i) : (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) a₁) * (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) a₂) = (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) (a₁ * a₂))

Multiplication in the free product of the injections of any two aᵢ aᵢ': A i for the same i is just the injection of multiplication aᵢ * aᵢ' in A i.

@[reducible, inline]

abbrev LinearAlgebra.FreeProduct.lof {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) : A i →ₗ[R] LinearAlgebra.FreeProduct R A

The ith canonical injection, from A i to the free product, as a linear map.

Equations

• LinearAlgebra.FreeProduct.lof R A i = LinearAlgebra.FreeProduct.ι' R A ∘ₗ DirectSum.lof R I A i

theorem LinearAlgebra.FreeProduct.lof_map_one {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) : (LinearAlgebra.FreeProduct.lof R A i) 1 = 1

lof R A i 1 = 1 for all i.

theorem LinearAlgebra.FreeProduct.ι_def {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : I → Type u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) : LinearAlgebra.FreeProduct.ι R A i = AlgHom.ofLinearMap (LinearAlgebra.FreeProduct.ι' R A ∘ₗ DirectSum.lof R I A i) ⋯ ⋯

@[irreducible]

def LinearAlgebra.FreeProduct.ι {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : I → Type u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) : A i →ₐ[R] LinearAlgebra.FreeProduct R A

The ith canonical injection, from A i to the free product.

Equations

• @LinearAlgebra.FreeProduct.ι = LinearAlgebra.FreeProduct.wrapped✝.1

@[irreducible]

def LinearAlgebra.FreeProduct.of {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : I → Type u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {i : I} : A i →ₐ[R] LinearAlgebra.FreeProduct R A

The family of canonical injection maps, with i left implicit.

Equations

• @LinearAlgebra.FreeProduct.of = LinearAlgebra.FreeProduct.wrapped✝.1

theorem LinearAlgebra.FreeProduct.of_def {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : I → Type u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {i : I} : LinearAlgebra.FreeProduct.of R A = LinearAlgebra.FreeProduct.ι R A i

def LinearAlgebra.FreeProduct.lift {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {B : Type w'} [Semiring B] [Algebra R B] : ({i : I} → A i →ₐ[R] B) ≃ (LinearAlgebra.FreeProduct R A →ₐ[R] B)

Universal property of the free product of algebras: for every R-algebra B, every family of maps maps : (i : I) → (A i →ₐ[R] B) lifts to a unique arrow π from FreeProduct R A such that π ∘ ι i = maps i.

Equations

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

@[simp]

theorem LinearAlgebra.FreeProduct.lift_apply {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {B : Type w'} [Semiring B] [Algebra R B] (maps : {i : I} → A i →ₐ[R] B) : (LinearAlgebra.FreeProduct.lift R A) maps = (RingQuot.liftAlgHom R) ⟨(TensorAlgebra.lift R) (DirectSum.toModule R I B fun (x : I) => maps.toLinearMap), ⋯⟩

@[simp]

theorem LinearAlgebra.FreeProduct.lift_symm_apply {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {B : Type w'} [Semiring B] [Algebra R B] (π : LinearAlgebra.FreeProduct R A →ₐ[R] B) (i : I) : (LinearAlgebra.FreeProduct.lift R A).symm π = π.comp (LinearAlgebra.FreeProduct.ι R A i)

theorem LinearAlgebra.FreeProduct.lift_comp_ι {I : Type u} [DecidableEq I] {i : I} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {B : Type w'} [Semiring B] [Algebra R B] (maps : {i : I} → A i →ₐ[R] B) : ((LinearAlgebra.FreeProduct.lift R A) fun {i : I} => maps).comp (LinearAlgebra.FreeProduct.ι R A i) = maps

Universal property of the free product of algebras, property: for every R-algebra B, every family of maps maps : (i : I) → (A i →ₐ[R] B) lifts to a unique arrow π from FreeProduct R A such that π ∘ ι i = maps i.

theorem LinearAlgebra.FreeProduct.lift_unique {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {B : Type w'} [Semiring B] [Algebra R B] (maps : {i : I} → A i →ₐ[R] B) (f : LinearAlgebra.FreeProduct R A →ₐ[R] B) (h : ∀ (i : I), f.comp (LinearAlgebra.FreeProduct.ι R A i) = maps) : f = (LinearAlgebra.FreeProduct.lift R A) fun {i : I} => maps