Free modules #
We introduce a class Module.Free R M, for R a Semiring and M an R-module and we provide
several basic instances for this class.
Use Finsupp.total_id_surjective to prove that any module is the quotient of a free module.
Main definition #
Module.Free R M: the class of freeR-modules.
Module.Free R M is the statement that the R-module M is free.
Instances
- Basis.dual_free
- Module.Free.addMonoidHom
- Module.Free.dfinsupp
- Module.Free.directSum
- Module.Free.finsupp
- Module.Free.function
- Module.Free.linearMap
- Module.Free.matrix
- Module.Free.of_divisionRing
- Module.Free.of_subsingleton
- Module.Free.of_subsingleton'
- Module.Free.pi
- Module.Free.prod
- Module.Free.self
- Module.Free.tensor
- Module.Free.ulift
- Module.free_of_finite_type_torsion_free'
- NumberField.RingOfIntegers.instFreeIntSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersInstSemiringIntToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToCommRingIntModuleToAddCommGroupToRing
- NumberField.Units.instFreeIntAdditiveQuotientUnitsSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstHasQuotientSubgroupTorsionInstSemiringIntAddCommMonoidToCommMonoidCommGroupInstCommGroupUnitsToCommMonoidToCommRingToCommRingIntModuleAddCommGroup
- NumberField.instFreeIntSubtypeMemSubmoduleSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleToAlgebraToCommSemiringToSemifieldIdSetLikeCoeToSubmoduleNonZeroDivisorsToMonoidWithZeroToSemiringInstSemiringIntAddCommMonoidIntModuleAddCommGroupToRingToAddCommGroup
- instFreeSubtypeMemIdealToSemiringToCommSemiringInstMembershipSetLikeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToSemiringToCommSemiringAddCommMonoidModule'ToSMulToModuleRight
- instModuleFree__of_discrete_addSubgroup
theorem
Module.free_def
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Small.{w, v} M]
:
Module.Free R M ↔ ∃ (I : Type w), Nonempty (Basis I R M)
theorem
Module.free_iff_set
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Module.Free R M ↔ ∃ (S : Set M), Nonempty (Basis (↑S) R M)
theorem
Module.Free.of_basis
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Type w}
(b : Basis ι R M)
:
Module.Free R M
def
Module.Free.ChooseBasisIndex
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
Type v
If Module.Free R M then ChooseBasisIndex R M is the ι which indexes the basis
ι → M. Note that this is defined such that this type is finite if R is trivial.
Equations
- Module.Free.ChooseBasisIndex R M = ↑(Exists.choose ⋯)
noncomputable instance
Module.Free.instDecidableEqChooseBasisIndex
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
There is no hope of computing this, but we add the instance anyway to avoid fumbling with
open scoped Classical.
Equations
noncomputable def
Module.Free.chooseBasis
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
Basis (Module.Free.ChooseBasisIndex R M) R M
If Module.Free R M then chooseBasis : ι → M is the basis.
Here ι = ChooseBasisIndex R M.
Equations
noncomputable def
Module.Free.repr
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
M ≃ₗ[R] Module.Free.ChooseBasisIndex R M →₀ R
The isomorphism M ≃ₗ[R] (ChooseBasisIndex R M →₀ R).
Equations
- Module.Free.repr R M = (Module.Free.chooseBasis R M).repr
noncomputable def
Module.Free.constr
(R : Type u)
(M : Type v)
(N : Type z)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[AddCommMonoid N]
[Module R N]
{S : Type z}
[Semiring S]
[Module S N]
[SMulCommClass R S N]
:
(Module.Free.ChooseBasisIndex R M → N) ≃ₗ[S] M →ₗ[R] N
The universal property of free modules: giving a function (ChooseBasisIndex R M) → N, for N
an R-module, is the same as giving an R-linear map M →ₗ[R] N.
This definition is parameterized over an extra Semiring S,
such that SMulCommClass R S M' holds.
If R is commutative, you can set S := R; if R is not commutative,
you can recover an AddEquiv by setting S := ℕ.
See library note [bundled maps over different rings].
Equations
- Module.Free.constr R M N = Basis.constr (Module.Free.chooseBasis R M) S
instance
Module.Free.noZeroSMulDivisors
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[NoZeroDivisors R]
:
Equations
- ⋯ = ⋯
instance
Module.Free.instNonemptyChooseBasisIndex
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[Nontrivial M]
:
Equations
- ⋯ = ⋯
theorem
Module.Free.infinite
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[Infinite R]
[Nontrivial M]
:
Infinite M
theorem
Module.Free.of_equiv
{R : Type u}
{M : Type v}
{N : Type z}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[AddCommMonoid N]
[Module R N]
(e : M ≃ₗ[R] N)
:
Module.Free R N
theorem
Module.Free.of_equiv'
{R : Type u}
{N : Type z}
[Semiring R]
[AddCommMonoid N]
[Module R N]
{P : Type v}
[AddCommMonoid P]
[Module R P]
:
Module.Free R P → (P ≃ₗ[R] N) → Module.Free R N
A variation of of_equiv: the assumption Module.Free R P here is explicit rather than an
instance.
The module structure provided by Semiring.toModule is free.
Equations
- ⋯ = ⋯
instance
Module.Free.prod
(R : Type u)
(M : Type v)
(N : Type z)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[AddCommMonoid N]
[Module R N]
[Module.Free R N]
:
Module.Free R (M × N)
Equations
- ⋯ = ⋯
instance
Module.Free.pi
{ι : Type u_1}
(R : Type u)
[Semiring R]
(M : ι → Type u_2)
[Finite ι]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
:
Module.Free R ((i : ι) → M i)
The product of finitely many free modules is free.
Equations
- ⋯ = ⋯
instance
Module.Free.matrix
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
{m : Type u_2}
{n : Type u_3}
[Finite m]
[Finite n]
:
Module.Free R (Matrix m n M)
The module of finite matrices is free.
Equations
- ⋯ = ⋯
instance
Module.Free.ulift
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
Module.Free R (ULift.{u_2, v} M)
Equations
- ⋯ = ⋯
instance
Module.Free.function
(ι : Type u_1)
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[Finite ι]
:
Module.Free R (ι → M)
The product of finitely many free modules is free (non-dependent version to help with typeclass search).
Equations
- ⋯ = ⋯
instance
Module.Free.finsupp
(ι : Type u_1)
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
Module.Free R (ι →₀ M)
Equations
- ⋯ = ⋯
instance
Module.Free.of_subsingleton
(R : Type u)
(N : Type z)
[Semiring R]
[AddCommMonoid N]
[Module R N]
[Subsingleton N]
:
Module.Free R N
Equations
- ⋯ = ⋯
instance
Module.Free.of_subsingleton'
(R : Type u)
(N : Type z)
[Semiring R]
[AddCommMonoid N]
[Module R N]
[Subsingleton R]
:
Module.Free R N
Equations
- ⋯ = ⋯
instance
Module.Free.dfinsupp
(R : Type u)
[Semiring R]
{ι : Type u_2}
(M : ι → Type u_3)
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
:
Module.Free R (Π₀ (i : ι), M i)
Equations
- ⋯ = ⋯
instance
Module.Free.directSum
(R : Type u)
[Semiring R]
{ι : Type u_2}
(M : ι → Type u_3)
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
:
Module.Free R (DirectSum ι fun (i : ι) => M i)
Equations
- ⋯ = ⋯
instance
Module.Free.tensor
(R : Type u)
(M : Type v)
(N : Type z)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[AddCommMonoid N]
[Module R N]
[Module.Free R N]
:
Module.Free R (TensorProduct R M N)
Equations
- ⋯ = ⋯