Fundamentals

ClassModule#

A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring R and an additive monoid of "vectors" M, connected by a "scalar multiplication" operation r • x : M (where r : R and x : M) with some natural associativity and distributivity axioms similar to those on a ring.

_root_.Module.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)
Sources
MathlibModule
Uses 2 · Used by 32
Statement usesGroup action · Natural number
Used byDivergence of the Harmonic Series · Principle of Inclusion/Exclusion · Jensen's inequality (finite sum version) · Normed vector space over a normed field · Topology on a normed vector space · Local convexity · Associative algebra over a commutative ring · Clifford algebra · Exterior algebra · Free algebra of a commutative ring · Lie algebra · Tensor algebra of a commutative ring · Tensor product of algebras · Chain complex · Fractional ideal · Representation · Affine subspace · Zariski topology · Pointed cone · Positive cone · Linear map · Multilinear map · Quotient space (Fundamentals) · Tensor product · The category of modules over a ring · Convex hull of a subset of an affine real space · Maschke theorem · Generating sets · Product of vector spaces · Sum of subspaces · Vector subspace · Convergence of \(p\)-series for \(p>1\)

StructureLinear map#

A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x. Elements of LinearMap σ M M₂ (available under the notation M →ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which σ = RingHom.id R), the notation M →ₗ[R] M₂ is available. An unbundled version of plain linear maps is available with the predicate IsLinearMap, but it should be avoided most of the time.

LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S]
  (σ : R →+* S) (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂]
  [_root_.Module R M] [_root_.Module S M₂] : Type (max u_16 u_17)
Sources
MathlibLinearMap
Uses 2 · Used by 78
Statement usesModule · Ring morphism
Used bySum of kth powers · Theorem of Ceva · Bertrand’s Postulate · The Factor and Remainder Theorems · Carathéodory's theorem · Uniform integrability · Equivalence of norms in finite dimension · Weak-* topology for dualities · Erdős–Ginzburg–Ziv theorem · Clifford algebra · Exterior algebra · Lie algebra · Tensor algebra of a commutative ring · Chain complex · Category of finite-dimensional representations · Character · Representation · Affine function · Dual cone · Bilinear form · Quadratic form · Dual vector space · Existence of orthonormal basis · Structure theorem · Basis · General linear group (Fundamentals) · Determinant · Markov inequality · Conditional probability · Binomial law · Gaussian law · Probability density function · Continuous linear map · Integral root theorem · Rational root theorem · Jacobson density theorem · Lasker–Noether theorem · Vieta's formulas · Mitchell's embedding theorem · Lebesgue differentiation theorem · Radon–Nikodym theorem · Steinhaus theorem · Vitali convergence theorem · Weierstrass preparation theorem · Poincaré recurrence theorem · Closed graph theorem · Hellinger–Toeplitz theorem · M. Riesz extension theorem · Hahn embedding theorem · Radon's theorem · Lebesgue's decomposition theorem · Lebesgue's density theorem · Dirichlet's approximation theorem · Glaisher's theorem · Mahler's theorem · Ostrowski's theorem · Pentagonal number theorem · Continuous mapping theorem · Ionescu-Tulcea theorem · Slutsky's theorem · Isometries of a Euclidean affine space · Affine groups · Cross product · Maschke theorem · Annihilating polynomials · Algebra of endomorphisms of a vector space · Kernel of a linear map · Linear independence · Range of a linear map · Invariant subspaces of an endomorphism · Lagrange interpolation · Algebraic elements · Decomposition into sums of homogeneous polynomials · Newton's identities · Polynomial derivative · Rational functions · Weierstrass polynomial approximation theorem · Hilbert bases

StructureThe category of modules over a ring#

The category of R-modules and their morphisms.

Note that in the case of R = ℤ, we cannot impose here that the ℤ-multiplication field from the module structure is defeq to the one coming from the isAddCommGroup structure \(contrary to what we do for all module structures in mathlib\), which creates some difficulties down the road.

ModuleCat.{v, u} (R : Type u) [Ring R] : Type (max u (v + 1))
Sources
MathlibModuleCat
Uses 3 · Used by 3
Statement usesInteger · Module · Ring
Used byStructure theorem · Mitchell's embedding theorem · Schur's lemma (Linear representations)

InstanceQuotient space (Fundamentals)#

The quotient of a module M by a submodule p ⊆ M.

Submodule.hasQuotient.{u_1, u_2} {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M]
  [_root_.Module R M] : HasQuotient M (Submodule R M)
Sources
MathlibSubmodule.hasQuotient
Uses 3 · Used by 9
Statement usesInteger · Module · Ring
Used byFinite-dimensional normed spaces over complete normed fields are complete · Nullstellensatz · Structure theorem · Going-up and going-down theorems · Jacobson density theorem · Krull's principal ideal theorem · Rank–nullity theorem · Weierstrass preparation theorem · Fourier transform on \(\mathrm{L}^2(\R^d)\)

DefinitionTensor product#

The tensor product of two modules M and N over the same commutative semiring R. The localized notations are M ⊗ N and M ⊗[R] N, accessed by open scoped TensorProduct.

TensorProduct.{u_1, u_5, u_6} (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6)
  [AddCommMonoid M] [AddCommMonoid N] [_root_.Module R M] [_root_.Module R N] : Type (max u_5 u_6)
Sources
MathlibTensorProduct
Uses 2 · Used by 3
Statement usesList · Module
Used byTensor algebra of a commutative ring · Tensor product of algebras · Minimal tensor product

ClassNoetherian module#

IsNoetherian R M is the proposition that M is a Noetherian R-module, implemented as the predicate that all R-submodules of M are finitely generated.

IsNoetherian.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] : Prop
Sources
MathlibIsNoetherian
Uses 2 · Used by 10
Statement usesFinite set · Generating sets
Used byHilbert basis theorem · Structure theorem · Krull's principal ideal theorem · Wedderburn–Artin theorem · Lie's theorem · Ax–Grothendieck theorem · Whitney embedding theorem · Ostrowski's theorem · Schur's lemma (Linear representations) · Change of variables to polar co-ordinates

StructureBasis#

A Basis ι R M for a module M is the type of ι-indexed R-bases of M.

The basis vectors are available as DFunLike.coe (b : Basis ι R M) : ι → M. To turn a linear independent family of vectors spanning M into a basis, use Basis.mk. They are internally represented as linear equivs M ≃ₗ[R] (ι →₀ R), available as Basis.repr.

Module.Basis.{u_1, u_3, u_4} (ι : Type u_1) (R : Type u_3) (M : Type u_4) [Semiring R]
  [AddCommMonoid M] [_root_.Module R M] : Type (max (max u_1 u_3) u_4)
Sources
MathlibModule.Basis
Uses 2 · Used by 17
Statement usesFinitely supported function · Linear map
Used byHeine-Borel theorem (finite-dimensional normed spaces are proper) · Dirichlet unit theorem · Structure of finitely generated abelian groups · Dual basis · Isomorphism with \(K^n\) · Structure theorem · Existence of an eigenvalue · Dimension theorem for vector spaces · Lie's theorem · Whitney embedding theorem · Dirichlet's unit theorem · Niven's theorem · Orthonormal bases · Sylvester's law of inertia (uniqueness) · Existence of bases · Determinant of vectors · Jordan-Chevalley-Dunford decomposition

StructureMultilinear map#

Multilinear maps from the R-module Π i, M i to the S-module N over a ring homomorphism σ : R →+* S.

MultilinearMap.{uR, uS, uι, u, v} {R : Type uR} {S : Type uS} [Semiring R] [Semiring S]
  (σ : R →+* S) {ι : Type uι} (M : ι → Type u) (N : Type v) [(i : ι) → AddCommMonoid (M i)]
  [AddCommMonoid N] [(i : ι) → _root_.Module R (M i)] [_root_.Module S N] : Type (max (max u uι) v)
Sources
MathlibMultilinearMap
Uses 2 · Used by 4
Statement usesModule · Ring morphism
Used byAlternating map · Matrix exponential · Radius of convergence · Higher-order derivatives of functions

StructureAlternating map#

An alternating map from ι → M to N, denoted M [⋀^ι]→ₗ[R] N, is a multilinear map that vanishes when two of its arguments are equal.

AlternatingMap.{u_1, u_2, u_3, u_7} (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M]
  [_root_.Module R M] (N : Type u_3) [AddCommMonoid N] [_root_.Module R N] (ι : Type u_7) :
  Type (max (max u_2 u_3) u_7)
Sources
MathlibAlternatingMap
Uses 1 · Used by 2
Statement usesMultilinear map
Used byDeterminant · Orientation of a \(\R\)-vector space

AbbreviationGeneral linear group (Fundamentals)#

The group of invertible linear maps from M to itself

LinearMap.GeneralLinearGroup.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] : Type u_2
Sources
MathlibLinearMap.GeneralLinearGroup
Uses 1
Statement usesLinear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.