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.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 : 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
    @[deprecated RingQuot.algEquivQuotAlgEquiv]
    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 : AAProp) :
    RingQuot rel ≃ₐ[R] RingQuot (rel on 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
    Instances For
      def RingQuot.equivQuotEquiv {A 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
        @[deprecated RingQuot.equivQuotEquiv]
        def RingQuot.equiv_quot_equiv {A B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : AAProp) :
        RingQuot rel ≃+* RingQuot (rel on 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
        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.FreeProductOfPowers {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
                        @[deprecated LinearAlgebra.FreeProductOfPowers]
                        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)

                        Alias of LinearAlgebra.FreeProductOfPowers.


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

                        Equations
                        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₂ : 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} :
                                    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
                                      @[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),
                                      @[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) :
                                      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