NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

Forms [ca-000L]
✍️source

    definition 1. Bilinear form [ca-0003]
    BilinForm
    L∃∀N

      Let \(R\) be a ring, \(M\) an \(R\)-module.

      An bilinear form \(B\) over \(M\) is a map \(B : M \to M \to R\), satisfying:

      1. \( B(x + y, z) = B(x, z) +B(y, z) \)
      2. \( B(x, y + z) = B(x, y) +B(x, z) \)
      3. \( B(a \bullet x, y) = a * B(x, y)\)
      4. \( B(x, a \bullet y) = a * B(x, y)\)
      for all \(a \in R, x, y, z \in M\).

      definition 2. quadratic form [jadczyk2019notes, 1.9] [ca-0004]
      QuadraticFormQuadraticForm.polar
      L∃∀N

        Let \(R\) be a commutative ring, \(M\) a \(R\)-module.

        An quadratic form \(Q\) over \(M\) is a map \(Q : M \to R\), satisfying:

        1. \( Q(a \bullet x) = a * a * Q(x)\) for all \(a \in R, x \in M\).
        2. there exists a companion bilinear form \(B : M \to M \to R\), such that \(Q(x + y) = Q(x) + Q(y) + B(x, y)\)

        In [jadczyk2019notes], the bilinear form is denoted \(\Phi \), and called the polar form associated with the quadratic form \(Q\), or simply the polar form of \(Q\).

        remark 3.  [ca-0005]

          This notion generalizes to commutative semirings using the approach in [izhakian2016supertropical].

          Context

            Preliminaries [ca-000N]

              This section introduces the algebraic environment of Clifford Algebra, covering vector spaces, groups, algebras, representations, modules, multilinear algebras, quadratic forms, filtrations and graded algebras.

              The material in this section should be familiar to the readers, but it is worth reading through it to become familiar with the notation and terminology that is used, as well as their counterparts in Lean, which usually require some additional treatment, both mathematically and technically (probably applicable to other formal proof verification systems).

              Details can be found in the references in corresponding section, or you may use the L∃∀N button to check the corresponding \(\textsf {Mathlib}\) document and Lean 4 source code.

              In this section, we follow [jadczyk2019notes], with supplements from [garling2011clifford][chen2016infinitely], and extensive modifications to match the counterparts in Lean's \(\textsf {Mathlib}\).

              basics: from groups to modules [ca-000P]

                [ca-000O]

                  \card{convention}{definition style}{

                  In this document, we unify the informal mathematical language for a definition to:

                  \optional{Let \placeholder{\(X\)} be a \placeholder{\vocab{concept \(X\)}}. }

                  A \newvocab{\placeholder{concept \(Z\)}} is a set/pair/triple/tuple \((Z, \mathtt {op}, ...)\), satisfying:

                  1. \placeholder{\(Z\)} is a \placeholder{\vocab{concept \(Y\)}} \optional{ over \placeholder{\(X\)} under \placeholder{op} }.
                  2. \placeholder{formula} for all \placeholder{elements in \(Z\)} \optional{(\vocab{ \placeholder{property} })}.
                  3. \optional{for each \placeholder{element} in \placeholder{\vocab{concept \(X\)}}, } there exists \placeholder{element} such that \placeholder{formula} for all \placeholder{elements in concept \(Z\)}.
                  4. \optional{\placeholder{op} is called \placeholder{\vocab{op name}}, }for all \placeholder{elements in \(Z\)}, we have
                    1. \placeholder{formula}
                    2. \placeholder{formula}
                    \optional{(\vocab{ \placeholder{property} })}.

                  By default, \placeholder{\(X\)} is a set, \placeholder{op} is a binary operation on \placeholder{\(X\)}.

                  }

                  definition. group [garling2011clifford, 1.1] [ca-000Q]
                  GroupAddGroup
                  L∃∀N

                    A group is a pair \((G, *)\), satisfying:

                    1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in G\) (associativity).
                    2. there exists \(1 \in G\) such that \[1 * a = a * 1 = a\] for all \(a \in G\).
                    3. for each \(a \in G\), there exists \(a^{-1} \in G\) such that \[a * a^{-1} = a^{-1} * a = 1\].

                    remark.  [ca-000R]

                      It then follows that \(1\), the identity element, is unique, and that for each \(g \in G\) the inverse \(g^{-1}\) is unique. A group G is abelian, or commutative, if \(g * h = h * g\) for all \(g, h \in G\).

                      notation. product [ca-000S]

                        In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).

                        Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.

                        Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.

                        \(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\), that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).

                        Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation, see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].

                        definition. monoid [ca-000T]
                        MonoidAddMonoid
                        L∃∀N

                          A monoid is a pair \((R, *)\), satisfying:

                          1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in R\) (associativity).
                          2. there exists an element \(1 \in R\) such that \(1 * a = a * 1 = a\) for all \(a \in R\)
                            3. i.e. \(1\) is the multiplicative identity (neutral element).

                          definition. ring [jadczyk2019notes, 1.1] [ca-000U]
                          RingCommRingCommSemiring
                          L∃∀N

                            A ring is a triple \((R, +, *)\), satisfying:

                            1. \(R\) is a commutative group under \(+\).
                            2. \(R\) is a monoid under \(*\).
                            3. for all \(a, b, c \in R\), we have
                              1. \(a * (b + c) = a * b + a * c\)
                              2. \((a + b) * c = a * c + b * c\)
                              (left and right distributivity over \(+\)).

                            remark.  [ca-000V]

                              In applications to Clifford algebras \(R\) will be always assumed to be commutative.

                              definition. division ring [ca-000W]
                              DivisionRing
                              L∃∀N

                                A division ring is a ring \((R, +, *)\), satisfying:

                                1. \(R\) contains at least 2 elements.
                                2. for all \(a \neq 0\) in \(R\), there exists a multiplicative inverse \(a^{-1} \in R\) such that
                                  3. \[ a * a^{-1} = a^{-1} * a = 1 \]

                                definition. module [jadczyk2019notes, 1.3] [ca-000X]
                                Module
                                L∃∀N

                                  Let \(R\) be a commutative ring. A module over \(R\), called an \(R\)-module, is a pair \((M, \bullet )\), satisfying:

                                  1. M is a group under \(+\).
                                  2. \(\bullet : R \to M \to M\) is called scalar multiplication, for every \(a, b \in R\), \(x, y \in M\), we have
                                    1. \(a \bullet (x + y) = a \bullet x + b \bullet y\)
                                    2. \((a + b) \bullet x = a \bullet x + b \bullet x\)
                                    3. \(a * (b \bullet x)=(a * b) \bullet x\)
                                    4. \(1_R \bullet x = x\)

                                  remark.  [ca-000Y]

                                    The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in \(\textsf {Mathlib}\): \[ \bullet : \alpha \to \beta \to \gamma \] where \(\alpha \), \(\beta \), \(\gamma \) are different types.

                                    definition. vector space [jadczyk2019notes, 1.5] [ca-000Z]
                                    Module
                                    L∃∀N

                                      If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.

                                      remark.  [ca-0010]

                                        For generality, \(\textsf {Mathlib}\) uses Module throughout for vector spaces, particularly, for a vector space \(V\), it's usually declared as

                                        /-- Let $K$ be a division ring, a module $V$ over $K$ is a vector space where being a module requires $V$ to be a commutative group over $+$. -/ variable [DivisionRing K] [AddCommGroup V] [Module K V]

                                        For definitions/theorems about it, and most of them can be found under Mathlib.LinearAlgebra e.g. LinearIndependent.

                                        definition. submodule [ca-0011]

                                          A submodule \(N\) of \(M\) is a module \(N\) such that every element of \(N\) is also an element of \(M\). If \(M\) is a vector space then \(N\) is called a subspace.

                                          definition. dual module [ca-0012]
                                          Module.Dual
                                          L∃∀N

                                            The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).

                                            algebras [ca-0013]

                                              definition. ring homomorphism [chen2016infinitely, 4.5.1] [ca-0014]
                                              RingHomRingHomClassalgebraMap
                                              L∃∀N

                                                Let \((\alpha , +_\alpha , *_\alpha )\) and \((\beta , +_\beta , *_\beta )\) be rings. A ring homomorphism from \(\alpha \) to \(\beta \) is a map \(\mathit {1} : \alpha \to _{+*} \beta \) such that

                                                1. \(\mathit {1}(x +_{\alpha } y) = \mathit {1}(x) +_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
                                                2. \(\mathit {1}(x *_{\alpha } y) = \mathit {1}(x) *_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
                                                3. \(\mathit {1}(1_{\alpha }) = 1_{\beta }\).

                                                definition. isomorphism, endomorphism, automorphism [ca-0015]

                                                  Isomorphism \(A \cong B\) is a bijective homomorphism \(\phi : A \to B\) (it follows that \(\phi ^{-1} : B \to A\) is also a homomorphism).

                                                  Endomorphism is a homomorphism from an object to itself, denoted \(\operatorname {End}(A)\).

                                                  Automorphism is an endomorphism which is also an isomorphism, denoted \(\operatorname {Aut}(A)\).

                                                  definition. algebra [ca-0016]
                                                  Algebra
                                                  L∃∀N

                                                    Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((A, \bullet )\), satisfying:

                                                    1. \(A\) is a ring under \(*\).
                                                    2. there exists a ring homomorphism from \(R\) to \(A\), denoted \(\mathit {1} : R \to _{+*} A\).
                                                    3. \(\bullet : R \to M \to M\) is a scalar multiplication
                                                    4. for every \(r \in R\), \(x \in A\), we have
                                                      1. \(r * x = x * r\) (commutativity between \(R\) and \(A\))
                                                      2. \(r \bullet x = r * x\) (definition of scalar multiplication)
                                                      where we omitted that the ring homomorphism \(\mathit {1}\) is applied to \(r\) before each multiplication.

                                                    notation.  [ca-0017]

                                                      Following literatures, for \(r \in R\), usually we write \(\mathit {1}_A(r) : R \to _{+*} A\) as a product \(r \mathit {1}_A\) if not omitted, while they are written as a call to algebraMap _ _ r in \(\textsf {Mathlib}\), which is defined to be Algebra.toRingHom r.

                                                      remark.  [ca-0018]

                                                        The definition above (adopted in \(\textsf {Mathlib}\)) is more general than the definition in literature (e.g. [jadczyk2019notes, 1.6]):

                                                        Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((M, *)\), satisfying:

                                                        1. \(A\) is a module \(M\) over \(R\) under \(+\) and \(\bullet \).
                                                        2. \(A\) is a ring under \(*\).
                                                        3. For \(x, y \in A, a \in R\), we have
                                                          4. \[ a \bullet (x * y) = (a \bullet x) * y = x * (a \bullet y) \]

                                                        See Implementation notes in Algebra for details.

                                                        remark.  [ca-0019]

                                                          What's simply called algebra is actually associative algebra with identity, a.k.a. associative unital algebra. See the red herring principle for more about such phenomenon for naming, particularly the example of (possibly) nonassociative algebra.

                                                          definition. algebra homomorphism [ca-001A]
                                                          AlgHom
                                                          L∃∀N

                                                            Let \(A\) and \(B\) be \(R\)-algebras. \(\mathit {1}_A\) and \(\mathit {1}_B\) are ring homomorphisms from \(R\) to \(A\) and \(B\), respectively. A algebra homomorphism from \(A\) to \(B\) is a map \(f : \alpha \to _{a} \beta \) such that

                                                            1. \(f\) is a ring homomorphism
                                                            2. \(f(\mathit {1}_{A}(r)) = \mathit {1}_{B}(r)\) for each \(r \in R\)

                                                            definition. ring quotient [ca-001B]
                                                            RingQuot
                                                            L∃∀N

                                                              Let \(R\) be a non-commutative ring, \(r\) an arbitrary equivalence relation on \(R\). The ring quotient of \(R\) by \(r\) is the quotient of \(R\) by the strengthen equivalence relation of \(r\) such that for all \(a, b, c\) in \(R\):

                                                              1. \(a + c \sim b + c\) if \(a \sim b\)
                                                              2. \(a * c \sim b * c\) if \(a \sim b\)
                                                              3. \(a * b \sim a * c\) if \(b \sim c\)
                                                              i.e. the equivalence relation is compatible with the ring operations \(+\) and \(*\).

                                                              remark.  [ca-001C]

                                                                As ideals haven't been formalized for the non-commutative case, \(\textsf {Mathlib}\) uses RingQuot in places where the quotient of non-commutative rings by ideal is needed. The universal properties of the quotient are proven, and should be used instead of the definition that is subject to change.

                                                                definition. free algebra [ca-001D]
                                                                FreeAlgebra FreeAlgebra.Pre FreeAlgebra.Rel
                                                                L∃∀N

                                                                  Let \(X\) be an arbitrary set. An free \(R\)-algebra on \(X\) (or "generated by \(X\)"), named \(A\), is the ring quotient of the following inductively constructed set \(A_{\mathtt {pre}}\)

                                                                  1. for all \(x\) in \(X\), there exists a map \(X \to A_{\mathtt {pre}}\).
                                                                  2. for all \(r\) in \(R\), there exists a map \(R \to A_{\mathtt {pre}}\).
                                                                  3. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a + b\) is in \(A_{\mathtt {pre}}\).
                                                                  4. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a * b\) is in \(A_{\mathtt {pre}}\).
                                                                  by that equivalence relation that makes \(A\) an \(R\)-algebra, namely:
                                                                  1. there exists a ring homomorphism from \(R\) to \(A_{\mathtt {pre}}\), denoted \(R \to _{+*} A_{\mathtt {pre}}\).
                                                                  2. \(A\) is a commutative group under \(+\).
                                                                  3. \(A\) is a monoid under \(*\).
                                                                  4. left and right distributivity under \(*\) over \(+\).
                                                                  5. \(0 * a \sim a * 0 \sim 0\).
                                                                  6. for all \(a, b, c\) in \(A\), if \(a \sim b\), we have
                                                                    1. \(a + c \sim b + c\)
                                                                    2. \(c + a \sim c + b\)
                                                                    3. \(a * c \sim b * c\)
                                                                    4. \(c * a \sim c * b\)
                                                                    (compatibility with the ring operations \(+\) and \(*\))

                                                                  remark.  [ca-001E]

                                                                    Similar to remark [ca-0019], what we defined here is the free (associative, unital) \(R\)-algebra on \(X\), it can be denoted \(R\langle X \rangle \), expressing that it's freely generated by \(R\) and \(X\), where \(X\) is the set of generators.

                                                                    definition. linear map [ca-001F]
                                                                    LinearMap
                                                                    L∃∀N

                                                                      Let \(R, S\) be rings, \(M\) an \(R\)-module, \(N\) an \(S\)-module. A linear map from \(M\) to \(N\) is a function \(f : M \to _{l} N\) over a ring homomorphism \(\sigma : R \to _{+*} S\), satisfying:

                                                                      1. \(f(x + y) = f(x) + f(y)\) for all \(x, y \in M\).
                                                                      2. \(f(r \bullet x) = \sigma (r) \bullet f(x)\) for all \(r \in R\), \(x \in M\).

                                                                      remark. Lin [ca-001G]

                                                                        The set of all linear maps from \(M\) to \(M'\) is denoted \(\operatorname {Lin}(M, M')\), and \(\operatorname {Lin}(M)\) for mapping from \(M\) to itself. \(\operatorname {Lin}(M)\) is an endomorphism.

                                                                        definition. tensor algebra [ca-001H]
                                                                        TensorAlgebra
                                                                        L∃∀N

                                                                          Let \(A\) be a free \(R\)-algebra generated by module \(M\), let \(\iota : M \to A\) denote the map from \(M\) to \(A\). An tensor algebra over \(M\) (or "of \(M\)") \(T\) is the ring quotient of the free \(R\)-algebra generated by \(M\), by the equivalence relation satisfying:

                                                                          1. for all \(a, b\) in \(M\), \(\iota (a + b) \sim \iota (a) + \iota (b)\).
                                                                          2. for all \(r\) in \(R\), \(a\) in \(M\), \(\iota (r \bullet a) \sim r * \iota (a)\).
                                                                          i.e. making the inclusion of \(M\) into an \(R\)-linear map.

                                                                          remark.  [ca-001I]

                                                                            The definition above is equivalent to the following definition in literature (e.g. [jadczyk2019notes, 1.7]):

                                                                            Let \(M\) be a module over \(R\). An algebra \(T\) is called a tensor algebra over \(M\) (or "of \(M\)") if it satisfies the following universal properties:

                                                                            1. \(T\) is an algebra containing \(M\) as a submodule, and it is generated by \(M\),
                                                                            2. Every linear mapping \(\lambda \) of \(M\) into an algebra \(A\) over \(R\), can be extended to
                                                                              3. a homomorphism \(\theta \) of \(T\) into \(A\).

                                                                            Forms [ca-000L]
                                                                            ✍️source

                                                                              definition. Bilinear form [ca-0003]
                                                                              BilinForm
                                                                              L∃∀N

                                                                                Let \(R\) be a ring, \(M\) an \(R\)-module.

                                                                                An bilinear form \(B\) over \(M\) is a map \(B : M \to M \to R\), satisfying:

                                                                                1. \( B(x + y, z) = B(x, z) +B(y, z) \)
                                                                                2. \( B(x, y + z) = B(x, y) +B(x, z) \)
                                                                                3. \( B(a \bullet x, y) = a * B(x, y)\)
                                                                                4. \( B(x, a \bullet y) = a * B(x, y)\)
                                                                                for all \(a \in R, x, y, z \in M\).

                                                                                definition. quadratic form [jadczyk2019notes, 1.9] [ca-0004]
                                                                                QuadraticFormQuadraticForm.polar
                                                                                L∃∀N

                                                                                  Let \(R\) be a commutative ring, \(M\) a \(R\)-module.

                                                                                  An quadratic form \(Q\) over \(M\) is a map \(Q : M \to R\), satisfying:

                                                                                  1. \( Q(a \bullet x) = a * a * Q(x)\) for all \(a \in R, x \in M\).
                                                                                  2. there exists a companion bilinear form \(B : M \to M \to R\), such that \(Q(x + y) = Q(x) + Q(y) + B(x, y)\)

                                                                                  In [jadczyk2019notes], the bilinear form is denoted \(\Phi \), and called the polar form associated with the quadratic form \(Q\), or simply the polar form of \(Q\).

                                                                                  remark.  [ca-0005]

                                                                                    This notion generalizes to commutative semirings using the approach in [izhakian2016supertropical].