Physlib.Mathematics.ForMathlib.LinearPMap

LinearPMap

i. Overview

In this module we collect some basic results about `LinearPMap`s.

Most important is the definition of restricted composition. The composition of two partial linear maps `g : F →ₗ.[R] G` and `f : E →ₗ.[R] F` is defined only if the range of `f` is contained in the domain of `g` (c.f. `LinearPMap.comp`). `g.compRestricted f` (`g ∘ᵣ f`) is defined to be the composition of `g` with the restriction of `f` to exactly those `x : f.domain` for which `f x ∈ g.domain`. This allows one to work with the composition of partial linear maps while having the domain implicitly accounted for.

ii. Key results

- `LinearPMap.sum` : The finite sum of partial linear maps. - `LinearPMap.compRestricted` (`∘ᵣ`) : For two partial linear maps `g : F →ₗ[R] G` and `f : E →ₗ[R] F`, the composition of `g` with `f` with natural domain `{x : f.domain | f x ∈ g.domain}`. - `LinearPMap.instMonoid` : Partial linear maps `E →ₗ.[R] E` with `compRestricted` for multiplication and the identity map for `1` comprise a monoid.

iii. Table of contents

A. Inequalities
B. Zero smul
C. Finite sums
D. Restricted composition
E. Monoid
F. Inverses

iv. References

* None.

A. Inequalities

B. Zero smul

C. Finite sums

D. Restricted composition

E. Monoid

Partial linear maps `E →ₗ.[R] E` with `compRestricted` for multiplication and the identity map (domain `⊤`) for `1` comprise a monoid.

F. Inverses

1 declaration

theorem

$\ker(f.\text{toFun}) = \{0\} \iff \ker f = \{0\}$ for partial linear maps $f$

#toFun_ker_eq_bot_iff

Let $R$ be a ring, and let $E$ and $F$ be $R$ -modules. For any partial linear map $f$ from $E$ to $F$ , the kernel of its underlying linear map (defined on its domain) is the zero subspace if and only if the kernel of $f$ (viewed as a subspace of $E$ ) is the zero subspace.