Documentation

Mathlib.Algebra.FreeAlgebra

Free Algebras #

Given a commutative semiring R, and a type X, we construct the free unital, associative R-algebra on X.

Notation #

  1. FreeAlgebra R X is the free algebra itself. It is endowed with an R-algebra structure.
  2. FreeAlgebra.ι R is the function X → FreeAlgebra R X.
  3. Given a function f : X → A to an R-algebra A, lift R f is the lift of f to an R-algebra morphism FreeAlgebra R X → A.

Theorems #

  1. ι_comp_lift states that the composition (lift R f) ∘ (ι R) is identical to f.
  2. lift_unique states that whenever an R-algebra morphism g : FreeAlgebra R X → A is given whose composition with ι R is f, then one has g = lift R f.
  3. hom_ext is a variant of lift_unique in the form of an extensionality theorem.
  4. lift_comp_ι is a combination of ι_comp_lift and lift_unique. It states that the lift of the composition of an algebra morphism with ι is the algebra morphism itself.
  5. equivMonoidAlgebraFreeMonoid : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)
  6. An inductive principle induction.

Implementation details #

We construct the free algebra on X as a quotient of an inductive type FreeAlgebra.Pre by an inductively defined relation FreeAlgebra.Rel. Explicitly, the construction involves three steps:

  1. We construct an inductive type FreeAlgebra.Pre R X, the terms of which should be thought of as representatives for the elements of FreeAlgebra R X. It is the free type with maps from R and X, and with two binary operations add and mul.
  2. We construct an inductive relation FreeAlgebra.Rel R X on FreeAlgebra.Pre R X. This is the smallest relation for which the quotient is an R-algebra where addition resp. multiplication are induced by add resp. mul from 1., and for which the map from R is the structure map for the algebra.
  3. The free algebra FreeAlgebra R X is the quotient of FreeAlgebra.Pre R X by the relation FreeAlgebra.Rel R X.
inductive FreeAlgebra.Pre (R : Type u_1) (X : Type u_2) :
Type (max u_1 u_2)

This inductive type is used to express representatives of the free algebra.

Instances For

    Coercion from X to Pre R X. Note: Used for notation only.

    Equations
    Instances For

      Coercion from R to Pre R X. Note: Used for notation only.

      Equations
      Instances For
        def FreeAlgebra.Pre.hasMul (R : Type u_1) (X : Type u_2) :

        Multiplication in Pre R X defined as Pre.mul. Note: Used for notation only.

        Equations
        Instances For
          def FreeAlgebra.Pre.hasAdd (R : Type u_1) (X : Type u_2) :

          Addition in Pre R X defined as Pre.add. Note: Used for notation only.

          Equations
          Instances For

            Zero in Pre R X defined as the image of 0 from R. Note: Used for notation only.

            Equations
            Instances For
              def FreeAlgebra.Pre.hasOne (R : Type u_1) [CommSemiring R] (X : Type u_2) :

              One in Pre R X defined as the image of 1 from R. Note: Used for notation only.

              Equations
              Instances For
                def FreeAlgebra.Pre.hasSMul (R : Type u_1) (X : Type u_2) :

                Scalar multiplication defined as multiplication by the image of elements from R. Note: Used for notation only.

                Equations
                Instances For
                  def FreeAlgebra.liftFun (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [Semiring A] [Algebra R A] (f : XA) :
                  FreeAlgebra.Pre R XA

                  Given a function from X to an R-algebra A, lift_fun provides a lift of f to a function from Pre R X to A. This is mainly used in the construction of FreeAlgebra.lift.

                  Equations
                  Instances For
                    inductive FreeAlgebra.Rel (R : Type u_1) [CommSemiring R] (X : Type u_2) :

                    An inductively defined relation on Pre R X used to force the initial algebra structure on the associated quotient.

                    Instances For
                      def FreeAlgebra (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                      Type (max u_1 u_2)

                      The free algebra for the type X over the commutative semiring R.

                      Equations
                      Instances For

                        Define the basic operations

                        instance FreeAlgebra.instSMul (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [CommSemiring A] [Algebra R A] :
                        Equations
                        instance FreeAlgebra.instZero (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations
                        instance FreeAlgebra.instOne (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations
                        instance FreeAlgebra.instAdd (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations
                        instance FreeAlgebra.instMul (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations

                        Build the semiring structure. We do this one piece at a time as this is convenient for proving the nsmul fields.

                        instance FreeAlgebra.instDistrib (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations
                        instance FreeAlgebra.instSemiring (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations
                        instance FreeAlgebra.instInhabited (R : Type u_1) [CommSemiring R] (X : Type u_2) :
                        Equations
                        instance FreeAlgebra.instAlgebra (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [CommSemiring A] [Algebra R A] :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        instance FreeAlgebra.instIsScalarTower (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring A] [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] :
                        Equations
                        • =
                        instance FreeAlgebra.instSMulCommClass (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] :
                        Equations
                        • =
                        @[irreducible]
                        def FreeAlgebra.ι (R : Type u_3) [CommSemiring R] {X : Type u_4} :
                        XFreeAlgebra R X

                        The canonical function X → FreeAlgebra R X.

                        Equations
                        Instances For
                          @[simp]
                          @[irreducible]
                          def FreeAlgebra.lift (R : Type u_1) [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] :
                          (XA) (FreeAlgebra R X →ₐ[R] A)

                          Given a function f : X → A where A is an R-algebra, lift R f is the unique lift of f to a morphism of R-algebras FreeAlgebra R X → A.

                          Equations
                          Instances For
                            @[simp]
                            theorem FreeAlgebra.liftAux_eq (R : Type u_1) [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : XA) :
                            @[simp]
                            theorem FreeAlgebra.lift_symm_apply (R : Type u_1) [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (F : FreeAlgebra R X →ₐ[R] A) :
                            @[simp]
                            theorem FreeAlgebra.ι_comp_lift {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : XA) :
                            @[simp]
                            theorem FreeAlgebra.lift_ι_apply {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : XA) (x : X) :
                            @[simp]
                            theorem FreeAlgebra.lift_unique {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : XA) (g : FreeAlgebra R X →ₐ[R] A) :

                            Since we have set the basic definitions as @[Irreducible], from this point onwards one should only use the universal properties of the free algebra, and consider the actual implementation as a quotient of an inductive type as completely hidden.

                            @[simp]
                            theorem FreeAlgebra.lift_comp_ι {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (g : FreeAlgebra R X →ₐ[R] A) :
                            theorem FreeAlgebra.hom_ext_iff {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] {f : FreeAlgebra R X →ₐ[R] A} {g : FreeAlgebra R X →ₐ[R] A} :
                            theorem FreeAlgebra.hom_ext {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] {f : FreeAlgebra R X →ₐ[R] A} {g : FreeAlgebra R X →ₐ[R] A} (w : f FreeAlgebra.ι R = g FreeAlgebra.ι R) :
                            f = g

                            See note [partially-applied ext lemmas].

                            The free algebra on X is "just" the monoid algebra on the free monoid on X.

                            This would be useful when constructing linear maps out of a free algebra, for example.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              FreeAlgebra R X is nontrivial when R is.

                              Equations
                              • =

                              FreeAlgebra R X has no zero-divisors when R has no zero-divisors.

                              Equations
                              • =
                              instance FreeAlgebra.instIsDomain {R : Type u_4} {X : Type u_5} [CommRing R] [IsDomain R] :

                              FreeAlgebra R X is a domain when R is an integral domain.

                              Equations
                              • =

                              The left-inverse of algebraMap.

                              Equations
                              Instances For
                                theorem FreeAlgebra.algebraMap_leftInverse {R : Type u_1} [CommSemiring R] {X : Type u_2} :
                                Function.LeftInverse FreeAlgebra.algebraMapInv (algebraMap R (FreeAlgebra R X))
                                @[simp]
                                theorem FreeAlgebra.algebraMap_inj {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : R) (y : R) :
                                (algebraMap R (FreeAlgebra R X)) x = (algebraMap R (FreeAlgebra R X)) y x = y
                                @[simp]
                                theorem FreeAlgebra.algebraMap_eq_zero_iff {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : R) :
                                (algebraMap R (FreeAlgebra R X)) x = 0 x = 0
                                @[simp]
                                theorem FreeAlgebra.algebraMap_eq_one_iff {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : R) :
                                (algebraMap R (FreeAlgebra R X)) x = 1 x = 1
                                @[simp]
                                theorem FreeAlgebra.ι_inj {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) (y : X) :
                                @[simp]
                                theorem FreeAlgebra.ι_ne_algebraMap {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) (r : R) :
                                @[simp]
                                theorem FreeAlgebra.ι_ne_zero {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) :
                                @[simp]
                                theorem FreeAlgebra.ι_ne_one {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) :
                                theorem FreeAlgebra.induction (R : Type u_1) [CommSemiring R] (X : Type u_2) {C : FreeAlgebra R XProp} (h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)) (h_grade1 : ∀ (x : X), C (FreeAlgebra.ι R x)) (h_mul : ∀ (a b : FreeAlgebra R X), C aC bC (a * b)) (h_add : ∀ (a b : FreeAlgebra R X), C aC bC (a + b)) (a : FreeAlgebra R X) :
                                C a

                                An induction principle for the free algebra.

                                If C holds for the algebraMap of r : R into FreeAlgebra R X, the ι of x : X, and is preserved under addition and multiplication, then it holds for all of FreeAlgebra R X.

                                theorem Algebra.adjoin_range_eq_range_freeAlgebra_lift (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [Semiring A] [Algebra R A] (f : XA) :

                                Noncommutative version of Algebra.adjoin_range_eq_range_aeval.

                                theorem Algebra.adjoin_eq_range_freeAlgebra_lift (R : Type u_1) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] (s : Set A) :
                                Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range

                                Noncommutative version of Algebra.adjoin_range_eq_range.