(Semi)linear maps #
In this file we define
LinearMap σ M M₂
,M →ₛₗ[σ] M₂
: a semilinear map between twoModule
s. Here,σ
is aRingHom
fromR
toR₂
and anf : M →ₛₗ[σ] M₂
satisfiesf (c • x) = (σ c) • (f x)
. We recover plain linear maps by choosingσ
to beRingHom.id R
. This is denoted byM →ₗ[R] M₂
. We also add the notationM →ₗ⋆[R] M₂
for star-linear maps.IsLinearMap R f
: predicate saying thatf : M → M₂
is a linear map. (Note that this was not generalized to semilinear maps.)
We then provide LinearMap
with the following instances:
LinearMap.addCommMonoid
andLinearMap.addCommGroup
: the elementwise addition structures corresponding to addition in the codomainLinearMap.distribMulAction
andLinearMap.module
: the elementwise scalar action structures corresponding to applying the action in the codomain.
Implementation notes #
To ensure that composition works smoothly for semilinear maps, we use the typeclasses
RingHomCompTriple
, RingHomInvPair
and RingHomSurjective
from
Mathlib.Algebra.Ring.CompTypeclasses
.
Notation #
- Throughout the file, we denote regular linear maps by
fₗ
,gₗ
, etc, and semilinear maps byf
,g
, etc.
TODO #
- Parts of this file have not yet been generalized to semilinear maps (i.e.
CompatibleSMul
)
Tags #
linear map
A map f
between modules over a semiring is linear if it satisfies the two properties
f (x + y) = f x + f y
and f (c • x) = c • f x
. The predicate IsLinearMap R f
asserts this
property. A bundled version is available with LinearMap
, and should be favored over
IsLinearMap
most of the time.
A linear map preserves addition.
A linear map preserves scalar multiplication.
Instances For
A linear map preserves addition.
A linear map preserves scalar multiplication.
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.
- toFun : M → M₂
The proposition that the function commutes with the actions.
Instances For
The MulActionHom
underlying a LinearMap
.
Equations
- self.toMulActionHom = { toFun := self.toFun, map_smul' := ⋯ }
Instances For
M →ₛₗ[σ] N
is the type of σ
-semilinear maps from M
to N
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
M →ₗ[R] N
is the type of R
-linear maps from M
to N
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
SemilinearMapClass F σ M M₂
asserts F
is a type of bundled σ
-semilinear maps M → M₂
.
See also LinearMapClass F R M M₂
for the case where σ
is the identity map on R
.
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
.
Instances
LinearMapClass F R M M₂
asserts F
is a type of bundled R
-linear maps M → M₂
.
This is an abbreviation for SemilinearMapClass F (RingHom.id R) M M₂
.
Equations
- LinearMapClass F R M M₂ = SemilinearMapClass F (RingHom.id R) M M₂
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Reinterpret an element of a type of semilinear maps as a semilinear map.
Equations
- ↑f = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Reinterpret an element of a type of semilinear maps as a semilinear map.
Equations
- SemilinearMapClass.instCoeToSemilinearMap = { coe := fun (f : F) => ↑f }
Reinterpret an element of a type of linear maps as a linear map.
Equations
Instances For
Reinterpret an element of a type of linear maps as a linear map.
Equations
- LinearMapClass.instCoeToLinearMap = { coe := fun (f : F) => ↑f }
Equations
- ⋯ = ⋯
The DistribMulActionHom
underlying a LinearMap
.
Equations
- f.toDistribMulActionHom = { toFun := f.toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Copy of a LinearMap
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Equations
- f.copy f' h = { toFun := f', map_add' := ⋯, map_smul' := ⋯ }
Instances For
A generalisation of LinearMap.id
that constructs the identity function
as a σ
-semilinear map for any ring homomorphism σ
which we know is the identity.
Equations
- LinearMap.id' = { toFun := fun (x : M) => x, map_add' := ⋯, map_smul' := ⋯ }
Instances For
If two linear maps are equal, they are equal at each point.
A typeclass for SMul
structures which can be moved through a LinearMap
.
This typeclass is generated automatically from an IsScalarTower
instance, but exists so that
we can also add an instance for AddCommGroup.toIntModule
, allowing z •
to be moved even if
S
does not support negation.
Scalar multiplication by
R
ofM
can be moved through linear maps.
Instances
Scalar multiplication by R
of M
can be moved through linear maps.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
convert a linear map to an additive map
Equations
- f.toAddMonoidHom = { toFun := ⇑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
If M
and M₂
are both R
-modules and S
-modules and R
-module structures
are defined by an action of R
on S
(formally, we have two scalar towers), then any S
-linear
map from M
to M₂
is R
-linear.
See also LinearMap.map_smul_of_tower
.
Equations
- ↑R fₗ = { toFun := ⇑fₗ, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equations
- LinearMap.coeIsScalarTower R = { coe := ↑R }
Composition of two linear maps is a linear map
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∘ₗ
is notation for composition of two linear (not semilinear!) maps into a linear map.
This is useful when Lean is struggling to infer the RingHomCompTriple
instance.
Equations
- LinearMap.compNotation = Lean.ParserDescr.trailingNode `LinearMap.compNotation 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ₗ ") (Lean.ParserDescr.cat `term 80))
Instances For
The linear map version of Function.Surjective.injective_comp_right
The linear map version of Function.Injective.comp_left
If a function g
is a left and right inverse of a linear map f
, then g
is linear itself.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
g : R →+* S
is R
-linear when the module structure on S
is Module.compHom S g
.
Equations
- Module.compHom.toLinearMap g = { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯ }
Instances For
A DistribMulActionHom
between two modules is a linear map.
Equations
- ↑fₗ = { toFun := fₗ.toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- DistribMulActionHom.instCoeTCSemilinearMap = { coe := DistribMulActionHom.toSemilinearMap }
A DistribMulActionHom
between two modules is a linear map.
Equations
- fₗ.toLinearMap = { toFun := fₗ.toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equations
- DistribMulActionHom.instCoeTCLinearMap = { coe := DistribMulActionHom.toLinearMap }
A DistribMulActionHom
between two modules is a linear map.
Equations
- ⋯ = ⋯
Convert an IsLinearMap
predicate to a LinearMap
Equations
- IsLinearMap.mk' f lin = { toFun := f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Reinterpret an additive homomorphism as an ℕ
-linear map.
Equations
- f.toNatLinearMap = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Reinterpret an additive homomorphism as a ℤ
-linear map.
Equations
- f.toIntLinearMap = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Arithmetic on the codomain #
The constant 0 map is linear.
Equations
- LinearMap.instZero = { zero := { toFun := 0, map_add' := ⋯, map_smul' := ⋯ } }
Equations
- LinearMap.uniqueOfLeft = { toInhabited := inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)), uniq := ⋯ }
Equations
- LinearMap.uniqueOfRight = ⋯.unique
The sum of two linear maps is linear.
The type of linear maps is an additive monoid.
Equations
- LinearMap.addCommMonoid = Function.Injective.addCommMonoid (fun (f : M →ₛₗ[σ₁₂] M₂) => ⇑f) ⋯ ⋯ ⋯ ⋯
The negation of a linear map is linear.
The subtraction of two linear maps is linear.
The type of linear maps is an additive group.
Equations
- LinearMap.addCommGroup = Function.Injective.addCommGroup (fun (f : M →ₛₗ[σ₁₂] N₂) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Evaluation of a σ₁₂
-linear map at a fixed a
, as an AddMonoidHom
.
Equations
- LinearMap.evalAddMonoidHom a = { toFun := fun (f : M →ₛₗ[σ₁₂] M₂) => f a, map_zero' := ⋯, map_add' := ⋯ }
Instances For
LinearMap.toAddMonoidHom
promoted to an AddMonoidHom
.
Equations
- LinearMap.toAddMonoidHom' = { toFun := LinearMap.toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
Instances For
If M
is the zero module, then the identity map of M
is the zero map.
Equations
- LinearMap.instDistribMulAction = DistribMulAction.mk ⋯ ⋯
LinearMap.restrictScalars
as a LinearMap
.
Equations
- LinearMap.restrictScalarsₗ R S M N R₁ = { toFun := ↑R, map_add' := ⋯, map_smul' := ⋯ }