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 alli : ι
andaᵢ aᵢ' : A i
1ᵢ ~ 1ⱼ
for1ᵢ := One.one (A i)
and for alli, 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 theR
-algebrasA i
, defined as a quotient of the tensor algebra on the direct sum of theA i
.FreeProduct_ofPowers R A
is the free product of theR
-algebrasA i
, defined as a quotient of the (infinite) direct sum of tensor powers of theA i
.lift
is the universal property of the free product.
Main results #
equivPowerAlgebra
establishes an equivalence betweenFreeProduct R A
andFreeProduct_ofPowers R A
.FreeProduct
is the coproduct in the category ofR
-algebras.
TODO #
- Induction principle for
FreeProduct
A variant of DirectSum.induction_on
that uses DirectSum.lof
instead of .of
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.
Instances For
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.)
Instances For
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
Instances For
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.)
Instances For
Equations
- LinearAlgebra.FreeProduct.instModuleDirectSum R A = inferInstance
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)
Instances For
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)
Instances For
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
Instances For
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} : LinearAlgebra.FreeProduct.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} : 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₂)))
Instances For
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)
Instances For
The free product of the collection of R
-algebras A i
, as a quotient of
FreeTensorAlgebra R A
.
Equations
Instances For
The free product of the collection of R
-algebras A i
, as a quotient of PowerAlgebra R A
Equations
Instances For
Alias of LinearAlgebra.FreeProductOfPowers
.
The free product of the collection of R
-algebras A i
, as a quotient of PowerAlgebra R A
Instances For
The R
-algebra equivalence relating FreeProduct
and FreeProduct_ofPowers
Equations
Instances For
Equations
- LinearAlgebra.FreeProduct.instSemiring R A = inferInstance
Equations
- LinearAlgebra.FreeProduct.instAlgebra R A = inferInstance
The canonical quotient map FreeTensorAlgebra R A →ₐ[R] FreeProduct R A
,
as an R
-algebra homomorphism.
Equations
Instances For
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
Instances For
The injection into the free product of any 1 : A i
is the 1 of the free product.
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
.
The i
th 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
Instances For
lof R A i 1 = 1
for all i
.
The i
th 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) ⋯ ⋯
Instances For
The family of canonical injection maps, with i
left implicit.
Equations
Instances For
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.
Instances For
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
.