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.

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)] {motive : (DirectSum ι fun (i : ι) => M i) → Prop} (x : DirectSum ι fun (i : ι) => M i) (zero : motive 0) (lof : ∀ (i : ι) (x : M i), motive ((lof R ι M i) x)) (add : ∀ (x y : DirectSum ι fun (i : ι) => M i), motive x → motive y → motive (x + y)) : motive x

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

def RingQuot.algEquivQuotAlgEquiv {R : Type u} [CommSemiring R] {A 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 (Function.onFun rel ⇑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.

@[deprecated RingQuot.algEquivQuotAlgEquiv (since := "2024-12-07")]

def RingQuot.algEquiv_quot_algEquiv {R : Type u} [CommSemiring R] {A 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 (Function.onFun rel ⇑f.symm)

Alias of RingQuot.algEquivQuotAlgEquiv.

---

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

• @RingQuot.algEquiv_quot_algEquiv = @RingQuot.algEquivQuotAlgEquiv

def RingQuot.equivQuotEquiv {A B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : A → A → Prop) : RingQuot rel ≃+* RingQuot (Function.onFun rel ⇑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.equivQuotEquiv f rel = (RingQuot.algEquivQuotAlgEquiv (AlgEquiv.ofRingEquiv ⋯) rel).toRingEquiv

@[deprecated RingQuot.equivQuotEquiv (since := "2024-12-07")]

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

Alias of RingQuot.equivQuotEquiv.

---

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 = @RingQuot.equivQuotEquiv

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.powerAlgebraEquivFreeTensorAlgebra {I : Type u} (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] : PowerAlgebra R A ≃ₐ[R] 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.powerAlgebraEquivFreeTensorAlgebra R A = TensorAlgebra.equivDirectSum.symm

@[deprecated LinearAlgebra.FreeProduct.powerAlgebraEquivFreeTensorAlgebra (since := "2025-05-05")]

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)] : PowerAlgebra R A ≃ₐ[R] FreeTensorAlgebra R A

Alias of LinearAlgebra.FreeProduct.powerAlgebraEquivFreeTensorAlgebra.

---

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 = @LinearAlgebra.FreeProduct.powerAlgebraEquivFreeTensorAlgebra

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)] : FreeTensorAlgebra R A → 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} [DecidableEq I] {R : Type v} [CommSemiring R] {A : I → Type w} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {i : I} : rel R A ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1
• prod {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₁ a₂ : A i} : 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 = Function.onFun (LinearAlgebra.FreeProduct.rel R A) ⇑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) : 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.asPowers {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.asPowers R A = RingQuot (LinearAlgebra.FreeProduct.rel' R A)

@[deprecated LinearAlgebra.FreeProduct.asPowers (since := "2024-12-07")]

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)

Alias of LinearAlgebra.FreeProduct.asPowers.

---

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

Equations

• @LinearAlgebra.FreeProduct_ofPowers = @LinearAlgebra.FreeProduct.asPowers

@[deprecated LinearAlgebra.FreeProduct.asPowers (since := "2025-05-01")]

def LinearAlgebra.FreeProductOfPowers {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)

Alias of LinearAlgebra.FreeProduct.asPowers.

---

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

Equations

• @LinearAlgebra.FreeProductOfPowers = @LinearAlgebra.FreeProduct.asPowers

noncomputable def LinearAlgebra.FreeProduct.asPowersEquiv {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)] : asPowers R A ≃ₐ[R] FreeProduct R A

The R-algebra equivalence relating FreeProduct and FreeProduct.asPowers.

Equations

• LinearAlgebra.FreeProduct.asPowersEquiv R A = (RingQuot.algEquivQuotAlgEquiv (LinearAlgebra.FreeProduct.powerAlgebraEquivFreeTensorAlgebra R A).symm (LinearAlgebra.FreeProduct.rel R A)).symm

@[deprecated LinearAlgebra.FreeProduct.asPowersEquiv (since := "2025-05-01")]

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)] : asPowers R A ≃ₐ[R] FreeProduct R A

Alias of LinearAlgebra.FreeProduct.asPowersEquiv.

---

The R-algebra equivalence relating FreeProduct and FreeProduct.asPowers.

Equations

• @LinearAlgebra.FreeProduct.equivPowerAlgebra = @LinearAlgebra.FreeProduct.asPowersEquiv

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 (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 (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)] : FreeTensorAlgebra R A →ₐ[R] 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] 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 (rel R A)) ((TensorAlgebra.ι R) x) } = (ι' 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) : (ι' 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₂ : A i) : (ι' R A) ((DirectSum.lof R I A i) a₁) * (ι' R A) ((DirectSum.lof R I A i) a₂) = (ι' 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] 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) : (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) : ι R A i = AlgHom.ofLinearMap (ι' 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] FreeProduct R A

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

Equations

• LinearAlgebra.FreeProduct.ι R A i = AlgHom.ofLinearMap (LinearAlgebra.FreeProduct.ι' R A ∘ₗ DirectSum.lof R I A i) ⋯ ⋯

@[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] FreeProduct R A

The family of canonical injection maps, with i left implicit

Equations

• LinearAlgebra.FreeProduct.of R A = LinearAlgebra.FreeProduct.ι R A i

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} : of R A = ι 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) ≃ (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_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] (π : FreeProduct R A →ₐ[R] B) (i : I) : (lift R A).symm π = π.comp (ι R A i)

@[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) : (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_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) : ((lift R A) fun {i : I} => maps).comp (ι 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.

@[simp]

theorem LinearAlgebra.FreeProduct.lift_algebraMap {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) (r : R) : ((lift R A) fun {i : I} => maps) ((algebraMap R (FreeProduct R A)) r) = (algebraMap R B) r

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 : FreeProduct R A →ₐ[R] B) (h : ∀ (i : I), f.comp (ι R A i) = maps) : f = (lift R A) fun {i : I} => maps