Documentation

Mathlib.LinearAlgebra.FreeProduct.Basic

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

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 #

Main results #

TODO #

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 xC yC (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 : AAProp) :
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.
Instances For
    def RingQuot.equiv_quot_equiv {A : Type v} {B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : AAProp) :
    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
    Instances For
      instance LinearAlgebra.FreeProduct.instModuleDirectSum {I : Type u} (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :
      Module R (DirectSum I fun (i : I) => A i)
      Equations
      @[reducible, inline]
      abbrev LinearAlgebra.FreeProduct.FreeTensorAlgebra {I : Type u} (R : Type v) [CommSemiring R] (A : IType 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
      Instances For
        @[reducible, inline]
        abbrev LinearAlgebra.FreeProduct.PowerAlgebra {I : Type u} (R : Type v) [CommSemiring R] (A : IType 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
        Instances For
          @[reducible]

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

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

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

            Instances For
              @[reducible]
              def LinearAlgebra.FreeProduct.rel' {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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
              Instances For
                theorem LinearAlgebra.FreeProduct.rel_id {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) :
                @[reducible]
                def LinearAlgebra.FreeProduct {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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
                Instances For
                  @[reducible]
                  def LinearAlgebra.FreeProduct_ofPowers {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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
                  Instances For
                    noncomputable def LinearAlgebra.FreeProduct.equivPowerAlgebra {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :

                    The R-algebra equivalence relating FreeProduct and FreeProduct_ofPowers

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      instance LinearAlgebra.FreeProduct.instSemiring {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :
                      Equations
                      instance LinearAlgebra.FreeProduct.instAlgebra {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :
                      Equations
                      @[reducible, inline]
                      abbrev LinearAlgebra.FreeProduct.mkAlgHom {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :

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

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev LinearAlgebra.FreeProduct.ι' {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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
                        Instances For
                          @[simp]
                          theorem LinearAlgebra.FreeProduct.ι_apply {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : DirectSum I fun (i : I) => A i) :
                          theorem LinearAlgebra.FreeProduct.identify_one {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) :

                          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 : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (a₁ : A i) (a₂ : A i) :

                          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 : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) :

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

                          Equations
                          Instances For
                            theorem LinearAlgebra.FreeProduct.lof_map_one {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) :

                            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 : IType u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) :
                            @[irreducible]
                            def LinearAlgebra.FreeProduct.ι {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : IType u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (i : I) :

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

                            Equations
                            Instances For
                              @[irreducible]
                              def LinearAlgebra.FreeProduct.of {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : IType u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {i : I} :

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

                              Equations
                              Instances For
                                theorem LinearAlgebra.FreeProduct.of_def {I : Type u_1} [DecidableEq I] (R : Type u_2) [CommSemiring R] (A : IType u_3) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] {i : I} :
                                @[simp]
                                theorem LinearAlgebra.FreeProduct.lift_symm_apply {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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) :
                                @[simp]
                                theorem LinearAlgebra.FreeProduct.lift_apply {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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),
                                def LinearAlgebra.FreeProduct.lift {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : IType 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.
                                Instances For
                                  theorem LinearAlgebra.FreeProduct.lift_comp_ι {I : Type u} [DecidableEq I] {i : I} (R : Type v) [CommSemiring R] (A : IType 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 : IType 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