The free product of -algebras #
We define the free product of an indexed collection of (noncommutative) (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 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
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
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} [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₂)))
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
The R
-algebra equivalence relating FreeProduct
and FreeProduct_ofPowers
Equations
- One or more equations did not get rendered due to their size.
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.
Instances For
The family of canonical injection maps, with i
left implicit.
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
.