Revision #1211 → #1824 · back to history
modifiedExterior algebra89c4a6321207
| Field | From #1211 | To #1824 |
|---|
| note | `ExteriorAlgebra R M` is defined as `CliffordAlgebra (0 : QuadraticForm R M)` for a commutative semiring `R` and module `M`, which generalizes the vector-space definition. | `ExteriorAlgebra R M` is defined as `CliffordAlgebra (0 : QuadraticForm R M)` for a commutative semiring `R` and module `M`, generalizing the vector-space definition. |
modifiedSimple k-vector / bladef0569d029702
| Field | From #1211 | To #1824 |
|---|
| note | Searching Mathlib for `blade`, `simple k-vector`, or analogous definitions returned no result; only the image of `ιMulti` is named (not the concept of a blade). | Searching Mathlib for `blade`/`simple k-vector` predicates returned no results; only the image of `ιMulti` is named. |
modifiedk-vector and multivector48ac57f98f26
| Field | From #1211 | To #1824 |
|---|
| mathlib.decl | exteriorPower | ExteriorAlgebra.exteriorPower |
| note | Elements of `⋀[R]^n M` play the role of `k`-vectors, but Mathlib has no dedicated `kVector`/`multivector` definitions for the sum-of-blades vocabulary. | Elements of `⋀[R]^n M` play the role of `k`-vectors, but Mathlib has no dedicated `kVector`/`multivector` names for the sum-of-blades vocabulary. |
modifiedk-th exterior powerd1d5c6a62e8e
| Field | From #1211 | To #1824 |
|---|
| mathlib.decl | exteriorPower | ExteriorAlgebra.exteriorPower |
| note | `exteriorPower R n M` is defined as `LinearMap.range (ExteriorAlgebra.ι R) ^ n`, with notation `⋀[R]^n M`. | `ExteriorAlgebra.exteriorPower R n M` is defined as `LinearMap.range (ExteriorAlgebra.ι R) ^ n`, with notation `⋀[R]^n M`. |
modifiedUniversal property (informal)ef3cd6a24d37
| Field | From #1211 | To #1824 |
|---|
| note | `ExteriorAlgebra.lift` is the equiv between linear maps `M →ₗ A` whose image squares to zero and algebra maps `ExteriorAlgebra R M →ₐ A`, witnessing the universal property. | `ExteriorAlgebra.lift` is the equiv between linear maps `M →ₗ A` with image squaring to zero and algebra maps `ExteriorAlgebra R M →ₐ A`, witnessing the universal property. |
modifiedArea of parallelogram via determinantaf50dbdaaa76
| Field | From #1211 | To #1824 |
|---|
| anchors | [{"section":"Areas in the plane","snippet":"The area of this parallelogram is given by the standard determinant formula"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {v} ={\\begin{bmatrix}a\\\\b\\end{bmatrix}}=a\\,\\mathbf {e} _{1}+b\\,\\mathbf {e} _{2},\\quad \\mathbf {w} ={\\begin{bmatrix}c\\\\d\\end{bmatrix}}=c\\,\\mathbf {e} _{1}+d\\,\\mathbf {e} _{2}}"},{"type":"math_alttext","value":"{\\displaystyle {\\text{Area}}=\\left|\\det {\\begin{bmatrix}\\mathbf {v} &\\mathbf {w} \\end{bmatrix}}\\right|=\\left|\\det {\\begin{bmatrix}a&c\\\\b&d\\end{bmatrix}}\\right|=\\left|ad-bc\\right|.}"}] | — |
| note | No Mathlib lemma states the parallelogram area = |det| in the geometric formulation; only the general `Matrix.det` is available. | No Mathlib lemma states the parallelogram area = |det| geometrically; only the general `Matrix.det` is available. |
modifiedExterior product yields signed area6993b36c45c5
| Field | From #1211 | To #1824 |
|---|
| anchors | [{"section":"Areas in the plane","snippet":"Consider now the exterior product of"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\mathbf {v} \\wedge \\mathbf {w} &=(a\\,\\mathbf {e} _{1}+b\\,\\mathbf {e} _{2})\\wedge (c\\,\\mathbf {e} _{1}+d\\,\\mathbf {e} _{2})\\\\&=ac\\,\\mathbf {e} _{1}\\wedge \\mathbf {e} _{1}+ad\\,\\mathbf {e} _{1}\\wedge \\mathbf {e} _{2}+bc\\,\\mathbf {e} _{2}\\wedge \\mathbf {e} _{1}+bd\\,\\mathbf {e} _{2}\\wedge \\mathbf {e} _{2}\\\\&=ad\\,\\mathbf {e} _{1}\\wedge \\mathbf {e} _{2}+bc\\,\\mathbf {e} _{2}\\wedge \\mathbf {e} _{1}\\\\&=\\left(ad-bc\\right)\\mathbf {e} _{1}\\wedge \\mathbf {e} _{2},\\end{aligned}}}"}] | — |
modifiedAxiomatic properties of signed areab6a1dd774a1c
| Field | From #1211 | To #1824 |
|---|
| note | The bilinear/alternating axiomatization of signed area is not explicitly stated for `R^2` in Mathlib. | The bilinear/alternating axiomatization of signed area on `R^2` is not stated explicitly in Mathlib. |
modifiedExterior product and cross product in R^39e96da334778
| Field | From #1211 | To #1824 |
|---|
| anchors | [{"section":"Cross and triple products","snippet":"the exterior algebra is closely related to the cross product and triple product"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {u} =u_{1}\\mathbf {e} _{1}+u_{2}\\mathbf {e} _{2}+u_{3}\\mathbf {e} _{3}}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {v} =v_{1}\\mathbf {e} _{1}+v_{2}\\mathbf {e} _{2}+v_{3}\\mathbf {e} _{3}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\mathbf {u} \\wedge \\mathbf {v} \\,&=(u_{1}v_{2}-u_{2}v_{1})(\\mathbf {e} _{1}\\wedge \\mathbf {e} _{2})\\\\&+(u_{3}v_{1}-u_{1}v_{3})(\\mathbf {e} _{3}\\wedge \\mathbf {e} _{1})\\\\&+(u_{2}v_{3}-u_{3}v_{2})(\\mathbf {e} _{2}\\wedge \\mathbf {e} _{3})\\end{aligned}}}"}] | — |
| note | `crossProduct` exists in `Mathlib.LinearAlgebra.CrossProduct` but there is no lemma linking it to the wedge product / exterior square. | `crossProduct` exists in `Mathlib.LinearAlgebra.CrossProduct` but no lemma links it to the wedge product / exterior square. |
modifiedTriple product as exterior product of three vectors0f3f152a1b0f
| Field | From #1211 | To #1824 |
|---|
| anchors | [{"section":"Cross and triple products","snippet":"the exterior product of three vectors is"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {w} =w_{1}\\mathbf {e} _{1}+w_{2}\\mathbf {e} _{2}+w_{3}\\mathbf {e} _{3},}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {u} \\wedge \\mathbf {v} \\wedge \\mathbf {w} =(u_{1}v_{2}w_{3}+u_{2}v_{3}w_{1}+u_{3}v_{1}w_{2}-u_{1}v_{3}w_{2}-u_{2}v_{1}w_{3}-u_{3}v_{2}w_{1})(\\mathbf {e} _{1}\\wedge \\mathbf {e} _{2}\\wedge \\mathbf {e} _{3})}"}] | — |
modifiedFormal definition of exterior algebrae9c69d0f7e77
| Field | From #1211 | To #1824 |
|---|
| note | Mathlib defines `ExteriorAlgebra` as `CliffordAlgebra 0`, not as a quotient of the tensor algebra; only `TensorAlgebra.toExterior` connects the two presentations. | Mathlib defines `ExteriorAlgebra` as `CliffordAlgebra 0`, not as a tensor-algebra quotient; `TensorAlgebra.toExterior` only connects the two presentations. |
modifiedExterior product on Lambda(V)be9205d83f96
| Field | From #1211 | To #1824 |
|---|
| note | Multiplication in `ExteriorAlgebra R M` is the wedge product, with `ExteriorAlgebra.ιMulti` packaging the multilinear wedge of `ι R`-images as an alternating map. | Multiplication in `ExteriorAlgebra R M` is the wedge product, packaged via `ExteriorAlgebra.ιMulti` as the alternating multilinear wedge. |
modifiedPermutation sign formula1e61c5e6c419
| Field | From #1211 | To #1824 |
|---|
| note | `AlternatingMap.map_perm` (specialized to `ExteriorAlgebra.ιMulti`) yields `ιMulti R n (v ∘ σ) = sign σ • ιMulti R n v`. | `AlternatingMap.map_perm`, specialized to `ExteriorAlgebra.ιMulti`, yields `ιMulti R n (v ∘ σ) = sign σ • ιMulti R n v`. |
modifiedk-th exterior power (formal)e413b2f6c400
| Field | From #1211 | To #1824 |
|---|
| mathlib.decl | exteriorPower | ExteriorAlgebra.exteriorPower |
| note | `exteriorPower R n M` is `LinearMap.range (ι R) ^ n`, the submodule of `n`-fold products in `ExteriorAlgebra R M`. | `ExteriorAlgebra.exteriorPower R n M` is `LinearMap.range (ι R) ^ n`, the submodule of `n`-fold products in `ExteriorAlgebra R M`. |
modifiedDecomposable k-vector (blade)0ba21659520b
| Field | From #1211 | To #1824 |
|---|
| note | No predicate `IsDecomposable` / `IsBlade` for elements of `⋀[R]^n M` appears in Mathlib. | No predicate `IsDecomposable`/`IsBlade` for elements of `⋀[R]^n M` appears in Mathlib. |
modifiedDirect sum decomposition of exterior algebraf218c53eeb9e
| Field | From #1211 | To #1824 |
|---|
| mathlib.decl | ExteriorAlgebra.instDecompositionExteriorPower | ExteriorAlgebra.gradedAlgebra |
| mathlib.match_kind | exact | invocation |
| note | The `DirectSum.Decomposition (fun n ↦ ⋀[R]^n M)` instance gives `ExteriorAlgebra R M ≃ ⨁ n, ⋀[R]^n M` as `R`-modules. | An (anonymous) `DirectSum.Decomposition (fun n ↦ ⋀[R]^n M)` instance is derived from `ExteriorAlgebra.gradedAlgebra` in `ExteriorAlgebra/Basis.lean`, yielding `ExteriorAlgebra R M ≃ ⨁ n, ⋀[R]^n M`. |
modifiedGraded algebra structure1dedf30ebefe
| Field | From #1211 | To #1824 |
|---|
| note | Same `ExteriorAlgebra.gradedAlgebra` instance witnesses the `ℕ`-grading by powers of `LinearMap.range (ι R)`. | The same `ExteriorAlgebra.gradedAlgebra` instance witnesses the `ℕ`-grading by powers of `LinearMap.range (ι R)`. |
modifiedGraded anticommutativitydf483ce218f3
| Field | From #1211 | To #1824 |
|---|
| note | The identity `α ∧ β = (-1)^{pq} β ∧ α` for homogeneous `α, β` is not recorded as a lemma in Mathlib (only the degree-1 case `ι_add_mul_swap` is). | The identity `α ∧ β = (-1)^{pq} β ∧ α` for homogeneous `α, β` is not a Mathlib lemma (only the degree-1 case `ι_add_mul_swap` is). |
modifiedUniversal property of exterior algebra46b9c0157332
| Field | From #1211 | To #1824 |
|---|
| note | `ExteriorAlgebra.lift`, with companion `ι_comp_lift` and `lift_unique`, gives the universal property statement and its uniqueness. | `ExteriorAlgebra.lift`, with `ι_comp_lift` and `lift_unique`, gives the universal property statement and uniqueness. |
modifiedAntisymmetrization of a decomposable tensor1634df6423bc
| Field | From #1211 | To #1824 |
|---|
| note | `MultilinearMap.alternatization` sends a multilinear map to `∑ σ, sign σ • m.domDomCongr σ`, which is the skew-symmetrization formula. | `MultilinearMap.alternatization` sends a multilinear map to `∑ σ, sign σ • m.domDomCongr σ`, the skew-symmetrization formula. |
modifiedIsomorphism via antisymmetrization (char 0)45f1e239744c
| Field | From #1211 | To #1824 |
|---|
| note | `AlternatingMap.coe_alternatization` shows alternatization of an alternating map is `n!` times itself, the key ingredient, but the resulting characteristic-0 isomorphism `⋀^n M ≅ Λ^n M ⊆ ⨂^n M` is not packaged. | `AlternatingMap.coe_alternatization` gives the key ingredient (alternatization of an alternating map is `n!` times itself), but the characteristic-0 iso `⋀^n M ≅ Λ^n M ⊆ ⨂^n M` is not packaged. |
modifiedAlternating tensor in index notation8989b612557a
| Field | From #1211 | To #1824 |
|---|
| note | Mathlib does not use the antisymmetric component-index notation for alternating tensors. | Mathlib does not use antisymmetric component-index notation for alternating tensors. |
modifiedInterior product in index notation1fd2a1ce4852
| Field | From #1211 | To #1824 |
|---|
| note | The interior product itself is not defined on `ExteriorAlgebra` in Mathlib; no index-notation lemma exists. | The interior product on `ExteriorAlgebra` is not defined in Mathlib, so no index-notation lemma exists. |
modifiedInterior product (antiderivation)bc0b0b3fdc85
| Field | From #1211 | To #1824 |
|---|
| anchors | [{"section":"Interior product","snippet":"it is possible to define an antiderivation on the algebra"},{"type":"math_alttext","value":"{\\displaystyle \\iota _{\\alpha }\\colon {\\textstyle \\bigwedge ^{\\!k}}(V)\\to {\\textstyle \\bigwedge ^{\\!k-1}}(V).}"}] | — |
modifiedInner product on exterior algebra5aef24b0c05f
| Field | From #1211 | To #1824 |
|---|
| note | No induced inner product on `⋀[R]^k M` (Gram-determinant formula) is defined. | No induced inner product on `⋀[R]^k M` (Gram-determinant formula) is defined in Mathlib. |
modifiedBialgebra/Hopf structure on exterior algebra31fbcc09f597
| Field | From #1211 | To #1824 |
|---|
| note | No `Bialgebra` / `HopfAlgebra` instance on `ExteriorAlgebra R M` is provided in Mathlib. | No `Bialgebra`/`HopfAlgebra` instance on `ExteriorAlgebra R M` is provided in Mathlib. |
modifiedCounit of exterior algebrace13fbc48bca
| Field | From #1211 | To #1824 |
|---|
| note | `ExteriorAlgebra.algebraMapInv : ExteriorAlgebra R M →ₐ R` is the natural augmentation that would play the role of the counit, though it is not labeled as such. | `ExteriorAlgebra.algebraMapInv : ExteriorAlgebra R M →ₐ R` is the natural augmentation that plays the role of a counit, though it is not labeled as such. |
modifiedFunctoriality of exterior algebra5829d58aa5fc
| Field | From #1211 | To #1824 |
|---|
| note | `ExteriorAlgebra.map` lifts a linear map `M →ₗ N` to an algebra map of exterior algebras, with `map_id` and `map_comp_map` showing functoriality. | `ExteriorAlgebra.map` lifts a linear map `M →ₗ N` to an algebra map of exterior algebras, with `map_id`/`map_comp_map` showing functoriality. |
modifiedExactness of induced exterior sequence272aa43e5fc6
| Field | From #1211 | To #1824 |
|---|
| note | `exteriorPower.map_surjective` proves preservation of surjectivity (and `map_injective_field` covers injectivity), but the full short-exact-sequence statement is not formalized. | `exteriorPower.map_surjective` proves preservation of surjectivity (with companion injectivity over a field), but the full short-exact-sequence statement is not formalized. |
modifiedDifferential forms via exterior algebra19d148ebae49
| Field | From #1211 | To #1824 |
|---|
| note | Mathlib has `Mathlib.Analysis.Calculus.DifferentialForm.VectorField` but no general definition of differential forms as sections of the exterior power of the cotangent bundle. | Mathlib has scattered differential-form material but no general definition of differential forms as sections of the exterior power of the cotangent bundle. |
modifiedde Rham cohomology from exterior algebrab9d92794591d
| Field | From #1211 | To #1824 |
|---|
| note | Mathlib's only `DeRham` file (`BDeRham`) is `p`-adic Hodge theory; classical de Rham cohomology via differential forms is not formalized. | Classical de Rham cohomology via differential forms is not formalized in Mathlib. |
addedSerre–Swan theorem (algebraic equivalence)3d8fc2b086c1
addedCauchy–Binet formula for inner products on exterior powers712de1f12d63
addedGrassmann number / supernumberc8a1e674d6e6
addedExterior algebra as a superalgebra6009b103e74f
addedExterior and symmetric algebras as Schur functors27b48625015f
addedKoszul complex from exterior algebrad75a77ac9900