# Partially defined linear maps #

A LinearPMap R E F or E →ₗ.[R] F is a linear map from a submodule of E to F. We define a SemilatticeInf with OrderBot instance on this, and define three operations:

• mkSpanSingleton defines a partial linear map defined on the span of a singleton.
• sup takes two partial linear maps f, g that agree on the intersection of their domains, and returns the unique partial linear map on f.domain ⊔ g.domain that extends both f and g.
• sSup takes a DirectedOn (· ≤ ·) set of partial linear maps, and returns the unique partial linear map on the sSup of their domains that extends all these maps.

Moreover, we define

• LinearPMap.graph is the graph of the partial linear map viewed as a submodule of E × F.

Partially defined maps are currently used in Mathlib to prove Hahn-Banach theorem and its variations. Namely, LinearPMap.sSup implies that every chain of LinearPMaps is bounded above. They are also the basis for the theory of unbounded operators.

structure LinearPMap (R : Type u) [Ring R] (E : Type v) [] [Module R E] (F : Type w) [] [Module R F] :
Type (max v w)

A LinearPMap R E F or E →ₗ.[R] F is a linear map from a submodule of E to F.

• domain :
• toFun : { x : E // x self.domain } →ₗ[R] F
Instances For

A LinearPMap R E F or E →ₗ.[R] F is a linear map from a submodule of E to F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LinearPMap.toFun' {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
{ x : E // x f.domain }F
Equations
• f = f.toFun
Instances For
instance LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
CoeFun (E →ₗ.[R] F) fun (f : E →ₗ.[R] F) => { x : E // x f.domain }F
Equations
• LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain = { coe := LinearPMap.toFun' }
@[simp]
theorem LinearPMap.toFun_eq_coe {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (x : { x : E // x f.domain }) :
f.toFun x = f x
theorem LinearPMap.ext {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : { x : E // x f.domain }⦄ ⦃y : { x : E // x g.domain }⦄, x = yf x = g y) :
f = g
@[simp]
theorem LinearPMap.map_zero {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
f 0 = 0
theorem LinearPMap.ext_iff {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} :
f = g ∃ (_ : f.domain = g.domain), ∀ ⦃x : { x : E // x f.domain }⦄ ⦃y : { x : E // x g.domain }⦄, x = yf x = g y
theorem LinearPMap.ext' {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {s : } {f : { x : E // x s } →ₗ[R] F} {g : { x : E // x s } →ₗ[R] F} (h : f = g) :
{ domain := s, toFun := f } = { domain := s, toFun := g }
theorem LinearPMap.map_add {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (x : { x : E // x f.domain }) (y : { x : E // x f.domain }) :
f (x + y) = f x + f y
theorem LinearPMap.map_neg {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (x : { x : E // x f.domain }) :
f (-x) = -f x
theorem LinearPMap.map_sub {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (x : { x : E // x f.domain }) (y : { x : E // x f.domain }) :
f (x - y) = f x - f y
theorem LinearPMap.map_smul {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (c : R) (x : { x : E // x f.domain }) :
f (c x) = c f x
@[simp]
theorem LinearPMap.mk_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (p : ) (f : { x : E // x p } →ₗ[R] F) (x : { x : E // x p }) :
{ domain := p, toFun := f } x = f x
noncomputable def LinearPMap.mkSpanSingleton' {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) :

The unique LinearPMap on R ∙ x that sends x to y. This version works for modules over rings, and requires a proof of ∀ c, c • x = 0 → c • y = 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearPMap.domain_mkSpanSingleton {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) :
.domain = Submodule.span R {x}
@[simp]
theorem LinearPMap.mkSpanSingleton'_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) (c : R) (h : c x .domain) :
c x, h = c y
@[simp]
theorem LinearPMap.mkSpanSingleton'_apply_self {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) (h : x .domain) :
x, h = y
@[reducible, inline]
noncomputable abbrev LinearPMap.mkSpanSingleton {K : Type u_5} {E : Type u_6} {F : Type u_7} [] [] [Module K E] [] [Module K F] (x : E) (y : F) (hx : x 0) :

The unique LinearPMap on span R {x} that sends a non-zero vector x to y. This version works for modules over division rings.

Equations
Instances For
theorem LinearPMap.mkSpanSingleton_apply (K : Type u_5) {E : Type u_6} {F : Type u_7} [] [] [Module K E] [] [Module K F] {x : E} (hx : x 0) (y : F) :
x, = y
def LinearPMap.fst {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (p : ) (p' : ) :
E × F →ₗ.[R] E

Projection to the first coordinate as a LinearPMap

Equations
• = { domain := p.prod p', toFun := ∘ₗ (p.prod p').subtype }
Instances For
@[simp]
theorem LinearPMap.fst_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (p : ) (p' : ) (x : { x : E × F // x p.prod p' }) :
(LinearPMap.fst p p') x = (↑x).1
def LinearPMap.snd {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (p : ) (p' : ) :
E × F →ₗ.[R] F

Projection to the second coordinate as a LinearPMap

Equations
• = { domain := p.prod p', toFun := ∘ₗ (p.prod p').subtype }
Instances For
@[simp]
theorem LinearPMap.snd_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (p : ) (p' : ) (x : { x : E × F // x p.prod p' }) :
(LinearPMap.snd p p') x = (↑x).2
instance LinearPMap.le {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
LE (E →ₗ.[R] F)
Equations
• LinearPMap.le = { le := fun (f g : E →ₗ.[R] F) => f.domain g.domain ∀ ⦃x : { x : E // x f.domain }⦄ ⦃y : { x : E // x g.domain }⦄, x = yf x = g y }
theorem LinearPMap.apply_comp_inclusion {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {T : E →ₗ.[R] F} {S : E →ₗ.[R] F} (h : T S) (x : { x : E // x T.domain }) :
T x = S ( x)
theorem LinearPMap.exists_of_le {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {T : E →ₗ.[R] F} {S : E →ₗ.[R] F} (h : T S) (x : { x : E // x T.domain }) :
∃ (y : { x : E // x S.domain }), x = y T x = S y
theorem LinearPMap.eq_of_le_of_domain_eq {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (hle : f g) (heq : f.domain = g.domain) :
f = g
def LinearPMap.eqLocus {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) :

Given two partial linear maps f, g, the set of points x such that both f and g are defined at x and f x = g x form a submodule.

Equations
• f.eqLocus g = { carrier := {x : E | ∃ (hf : x f.domain) (hg : x g.domain), f x, hf = g x, hg}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
instance LinearPMap.inf {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Inf (E →ₗ.[R] F)
Equations
• LinearPMap.inf = { inf := fun (f g : E →ₗ.[R] F) => { domain := f.eqLocus g, toFun := f.toFun ∘ₗ } }
instance LinearPMap.bot {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Bot (E →ₗ.[R] F)
Equations
• LinearPMap.bot = { bot := { domain := , toFun := 0 } }
instance LinearPMap.inhabited {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.inhabited = { default := }
instance LinearPMap.semilatticeInf {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.semilatticeInf =
instance LinearPMap.orderBot {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.orderBot =
theorem LinearPMap.le_of_eqLocus_ge {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (H : f.domain f.eqLocus g) :
f g
theorem LinearPMap.domain_mono {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
StrictMono LinearPMap.domain
noncomputable def LinearPMap.sup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : { x : E // x f.domain }) (y : { x : E // x g.domain }), x = yf x = g y) :

Given two partial linear maps that agree on the intersection of their domains, f.sup g h is the unique partial linear map on f.domain ⊔ g.domain that agrees with f and g.

Equations
• f.sup g h = { domain := f.domain g.domain, toFun := }
Instances For
@[simp]
theorem LinearPMap.domain_sup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : { x : E // x f.domain }) (y : { x : E // x g.domain }), x = yf x = g y) :
(f.sup g h).domain = f.domain g.domain
theorem LinearPMap.sup_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (H : ∀ (x : { x : E // x f.domain }) (y : { x : E // x g.domain }), x = yf x = g y) (x : { x : E // x f.domain }) (y : { x : E // x g.domain }) (z : { x : E // x f.domain g.domain }) (hz : x + y = z) :
(f.sup g H) z = f x + g y
theorem LinearPMap.left_le_sup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : { x : E // x f.domain }) (y : { x : E // x g.domain }), x = yf x = g y) :
f f.sup g h
theorem LinearPMap.right_le_sup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : { x : E // x f.domain }) (y : { x : E // x g.domain }), x = yf x = g y) :
g f.sup g h
theorem LinearPMap.sup_le {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} {h : E →ₗ.[R] F} (H : ∀ (x : { x : E // x f.domain }) (y : { x : E // x g.domain }), x = yf x = g y) (fh : f h) (gh : g h) :
f.sup g H h
theorem LinearPMap.sup_h_of_disjoint {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : Disjoint f.domain g.domain) (x : { x : E // x f.domain }) (y : { x : E // x g.domain }) (hxy : x = y) :
f x = g y

Hypothesis for LinearPMap.sup holds, if f.domain is disjoint with g.domain.

### Algebraic operations #

instance LinearPMap.instZero {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.instZero = { zero := { domain := , toFun := 0 } }
@[simp]
theorem LinearPMap.zero_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
@[simp]
theorem LinearPMap.zero_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (x : { x : E // x }) :
0 x = 0
instance LinearPMap.instSMul {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} [] [] [] :
SMul M (E →ₗ.[R] F)
Equations
• LinearPMap.instSMul = { smul := fun (a : M) (f : E →ₗ.[R] F) => { domain := f.domain, toFun := a f.toFun } }
@[simp]
theorem LinearPMap.smul_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} [] [] [] (a : M) (f : E →ₗ.[R] F) :
(a f).domain = f.domain
theorem LinearPMap.smul_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} [] [] [] (a : M) (f : E →ₗ.[R] F) (x : { x : E // x (a f).domain }) :
(a f) x = a f x
@[simp]
theorem LinearPMap.coe_smul {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} [] [] [] (a : M) (f : E →ₗ.[R] F) :
(a f) = a f
instance LinearPMap.instSMulCommClass {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} {N : Type u_6} [] [] [] [] [] [] [] :
Equations
• =
instance LinearPMap.instIsScalarTower {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} {N : Type u_6} [] [] [] [] [] [] [SMul M N] [] :
Equations
• =
instance LinearPMap.instMulAction {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} [] [] [] :
Equations
• LinearPMap.instMulAction =
instance LinearPMap.instNeg {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Neg (E →ₗ.[R] F)
Equations
• LinearPMap.instNeg = { neg := fun (f : E →ₗ.[R] F) => { domain := f.domain, toFun := -f.toFun } }
@[simp]
theorem LinearPMap.neg_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
(-f).domain = f.domain
@[simp]
theorem LinearPMap.neg_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (x : { x : E // x (-f).domain }) :
(-f) x = -f x
instance LinearPMap.instInvolutiveNeg {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.instInvolutiveNeg =
instance LinearPMap.instAdd {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.instAdd = { add := fun (f g : E →ₗ.[R] F) => { domain := f.domain g.domain, toFun := f.toFun ∘ₗ + g.toFun ∘ₗ } }
theorem LinearPMap.add_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) :
(f + g).domain = f.domain g.domain
theorem LinearPMap.add_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (x : { x : E // x f.domain g.domain }) :
(f + g) x = f x, + g x,
instance LinearPMap.instAddSemigroup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
instance LinearPMap.instAddZeroClass {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
instance LinearPMap.instAddMonoid {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
instance LinearPMap.instAddCommMonoid {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
instance LinearPMap.instVAdd {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
VAdd (E →ₗ[R] F) (E →ₗ.[R] F)
Equations
• LinearPMap.instVAdd = { vadd := fun (f : E →ₗ[R] F) (g : E →ₗ.[R] F) => { domain := g.domain, toFun := f ∘ₗ g.domain.subtype + g.toFun } }
@[simp]
theorem LinearPMap.vadd_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) :
(f +ᵥ g).domain = g.domain
theorem LinearPMap.vadd_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) (x : { x : E // x (f +ᵥ g).domain }) :
(f +ᵥ g) x = f x + g x
@[simp]
theorem LinearPMap.coe_vadd {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) :
(f +ᵥ g) = (f ∘ₗ g.domain.subtype) + g
instance LinearPMap.instAddAction {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
instance LinearPMap.instSub {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Sub (E →ₗ.[R] F)
Equations
• LinearPMap.instSub = { sub := fun (f g : E →ₗ.[R] F) => { domain := f.domain g.domain, toFun := f.toFun ∘ₗ - g.toFun ∘ₗ } }
theorem LinearPMap.sub_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) :
(f - g).domain = f.domain g.domain
theorem LinearPMap.sub_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (x : { x : E // x f.domain g.domain }) :
(f - g) x = f x, - g x,
instance LinearPMap.instSubtractionCommMonoid {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] :
Equations
• LinearPMap.instSubtractionCommMonoid =
noncomputable def LinearPMap.supSpanSingleton {E : Type u_2} [] {F : Type u_3} [] {K : Type u_5} [] [Module K E] [Module K F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : xf.domain) :

Extend a LinearPMap to f.domain ⊔ K ∙ x.

Equations
• f.supSpanSingleton x y hx = f.sup
Instances For
@[simp]
theorem LinearPMap.domain_supSpanSingleton {E : Type u_2} [] {F : Type u_3} [] {K : Type u_5} [] [Module K E] [Module K F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : xf.domain) :
(f.supSpanSingleton x y hx).domain = f.domain Submodule.span K {x}
@[simp]
theorem LinearPMap.supSpanSingleton_apply_mk {E : Type u_2} [] {F : Type u_3} [] {K : Type u_5} [] [Module K E] [Module K F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : xf.domain) (x' : E) (hx' : x' f.domain) (c : K) :
(f.supSpanSingleton x y hx) x' + c x, = f x', hx' + c y
noncomputable def LinearPMap.sSup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (c : Set (E →ₗ.[R] F)) (hc : DirectedOn (fun (x1 x2 : E →ₗ.[R] F) => x1 x2) c) :
Equations
• = { domain := sSup (LinearPMap.domain '' c), toFun := }
Instances For
theorem LinearPMap.le_sSup {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (fun (x1 x2 : E →ₗ.[R] F) => x1 x2) c) {f : E →ₗ.[R] F} (hf : f c) :
f
theorem LinearPMap.sSup_le {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (fun (x1 x2 : E →ₗ.[R] F) => x1 x2) c) {g : E →ₗ.[R] F} (hg : fc, f g) :
g
theorem LinearPMap.sSup_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (fun (x1 x2 : E →ₗ.[R] F) => x1 x2) c) {l : E →ₗ.[R] F} (hl : l c) (x : { x : E // x l.domain }) :
(LinearPMap.sSup c hc) x, = l x
def LinearMap.toPMap {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ[R] F) (p : ) :

Restrict a linear map to a submodule, reinterpreting the result as a LinearPMap.

Equations
• f.toPMap p = { domain := p, toFun := f ∘ₗ p.subtype }
Instances For
@[simp]
theorem LinearMap.toPMap_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ[R] F) (p : ) (x : { x : E // x p }) :
(f.toPMap p) x = f x
@[simp]
theorem LinearMap.toPMap_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ[R] F) (p : ) :
(f.toPMap p).domain = p
def LinearMap.compPMap {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {G : Type u_4} [] [Module R G] (g : F →ₗ[R] G) (f : E →ₗ.[R] F) :

Compose a linear map with a LinearPMap

Equations
• g.compPMap f = { domain := f.domain, toFun := g ∘ₗ f.toFun }
Instances For
@[simp]
theorem LinearMap.compPMap_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {G : Type u_4} [] [Module R G] (g : F →ₗ[R] G) (f : E →ₗ.[R] F) (x : { x : E // x (g.compPMap f).domain }) :
(g.compPMap f) x = g (f x)
def LinearPMap.codRestrict {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (p : ) (H : ∀ (x : { x : E // x f.domain }), f x p) :
E →ₗ.[R] { x : F // x p }

Restrict codomain of a LinearPMap

Equations
Instances For
def LinearPMap.comp {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {G : Type u_4} [] [Module R G] (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) (H : ∀ (x : { x : E // x f.domain }), f x g.domain) :

Compose two LinearPMaps

Equations
• g.comp f H = g.toFun.compPMap (f.codRestrict g.domain H)
Instances For
def LinearPMap.coprod {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {G : Type u_4} [] [Module R G] (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) :
E × F →ₗ.[R] G

f.coprod g is the partially defined linear map defined on f.domain × g.domain, and sending p to f p.1 + g p.2.

Equations
• f.coprod g = { domain := f.domain.prod g.domain, toFun := (f.comp (LinearPMap.fst f.domain g.domain) ).toFun + (g.comp (LinearPMap.snd f.domain g.domain) ).toFun }
Instances For
@[simp]
theorem LinearPMap.coprod_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {G : Type u_4} [] [Module R G] (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) (x : { x : E × F // x (f.coprod g).domain }) :
(f.coprod g) x = f (↑x).1, + g (↑x).2,
def LinearPMap.domRestrict {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (S : ) :

Restrict a partially defined linear map to a submodule of E contained in f.domain.

Equations
• f.domRestrict S = { domain := S f.domain, toFun := f.toFun ∘ₗ }
Instances For
@[simp]
theorem LinearPMap.domRestrict_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) {S : } :
(f.domRestrict S).domain = S f.domain
theorem LinearPMap.domRestrict_apply {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {S : } ⦃x : { x : E // x S f.domain } ⦃y : { x : E // x f.domain } (h : x = y) :
(f.domRestrict S) x = f y
theorem LinearPMap.domRestrict_le {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {S : } :
f.domRestrict S f

### Graph #

def LinearPMap.graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
Submodule R (E × F)

The graph of a LinearPMap viewed as a submodule on E × F.

Equations
• f.graph = Submodule.map (f.domain.subtype.prodMap LinearMap.id) f.toFun.graph
Instances For
theorem LinearPMap.mem_graph_iff' {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) {x : E × F} :
x f.graph ∃ (y : { x : E // x f.domain }), (y, f y) = x
@[simp]
theorem LinearPMap.mem_graph_iff {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) {x : E × F} :
x f.graph ∃ (y : { x : E // x f.domain }), y = x.1 f y = x.2
theorem LinearPMap.mem_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) (x : { x : E // x f.domain }) :
(x, f x) f.graph

The tuple (x, f x) is contained in the graph of f.

theorem LinearPMap.graph_map_fst_eq_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
Submodule.map (LinearMap.fst R E F) f.graph = f.domain
theorem LinearPMap.graph_map_snd_eq_range {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
theorem LinearPMap.smul_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {M : Type u_5} [] [] [] (f : E →ₗ.[R] F) (z : M) :
(z f).graph = Submodule.map (LinearMap.id.prodMap (z LinearMap.id)) f.graph

The graph of z • f as a pushforward.

theorem LinearPMap.neg_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :
(-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

The graph of -f as a pushforward.

theorem LinearPMap.mem_graph_snd_inj {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) {x : E} {y : E} {x' : F} {y' : F} (hx : (x, x') f.graph) (hy : (y, y') f.graph) (hxy : x = y) :
x' = y'
theorem LinearPMap.mem_graph_snd_inj' {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) {x : E × F} {y : E × F} (hx : x f.graph) (hy : y f.graph) (hxy : x.1 = y.1) :
x.2 = y.2
theorem LinearPMap.graph_fst_eq_zero_snd {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) {x : E} {x' : F} (h : (x, x') f.graph) (hx : x = 0) :
x' = 0

The property that f 0 = 0 in terms of the graph.

theorem LinearPMap.mem_domain_iff {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {x : E} :
x f.domain ∃ (y : F), (x, y) f.graph
theorem LinearPMap.mem_domain_of_mem_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {x : E} {y : F} (h : (x, y) f.graph) :
x f.domain
theorem LinearPMap.image_iff {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {x : E} {y : F} (hx : x f.domain) :
y = f x, hx (x, y) f.graph
theorem LinearPMap.mem_range_iff {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {y : F} :
y ∃ (x : E), (x, y) f.graph
theorem LinearPMap.mem_domain_iff_of_eq_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : f.graph = g.graph) {x : E} :
x f.domain x g.domain
theorem LinearPMap.le_of_le_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : f.graph g.graph) :
f g
theorem LinearPMap.le_graph_of_le {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : f g) :
f.graph g.graph
theorem LinearPMap.le_graph_iff {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} :
f.graph g.graph f g
theorem LinearPMap.eq_of_eq_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : f.graph = g.graph) :
f = g
theorem Submodule.existsUnique_from_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {g : Submodule R (E × F)} (hg : ∀ {x : E × F}, x gx.1 = 0x.2 = 0) {a : E} (ha : a Submodule.map (LinearMap.fst R E F) g) :
∃! b : F, (a, b) g
noncomputable def Submodule.valFromGraph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {g : Submodule R (E × F)} (hg : xg, x.1 = 0x.2 = 0) {a : E} (ha : a Submodule.map (LinearMap.fst R E F) g) :
F

Auxiliary definition to unfold the existential quantifier.

Equations
• = .choose
Instances For
theorem Submodule.valFromGraph_mem {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {g : Submodule R (E × F)} (hg : xg, x.1 = 0x.2 = 0) {a : E} (ha : a Submodule.map (LinearMap.fst R E F) g) :
(a, ) g
noncomputable def Submodule.toLinearPMapAux {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (g : Submodule R (E × F)) (hg : xg, x.1 = 0x.2 = 0) :
{ x : E // x Submodule.map (LinearMap.fst R E F) g } →ₗ[R] F

Define a LinearMap from its graph.

Helper definition for LinearPMap.

Equations
Instances For
noncomputable def Submodule.toLinearPMap {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (g : Submodule R (E × F)) :

Define a LinearPMap from its graph.

In the case that the submodule is not a graph of a LinearPMap then the underlying linear map is just the zero map.

Equations
• g.toLinearPMap = { domain := Submodule.map (LinearMap.fst R E F) g, toFun := if hg : xg, x.1 = 0x.2 = 0 then g.toLinearPMapAux hg else 0 }
Instances For
theorem Submodule.toLinearPMap_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (g : Submodule R (E × F)) :
g.toLinearPMap.domain = Submodule.map (LinearMap.fst R E F) g
theorem Submodule.toLinearPMap_apply_aux {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {g : Submodule R (E × F)} (hg : xg, x.1 = 0x.2 = 0) (x : { x : E // x Submodule.map (LinearMap.fst R E F) g }) :
g.toLinearPMap x =
theorem Submodule.mem_graph_toLinearPMap {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {g : Submodule R (E × F)} (hg : xg, x.1 = 0x.2 = 0) (x : { x : E // x Submodule.map (LinearMap.fst R E F) g }) :
(x, g.toLinearPMap x) g
@[simp]
theorem Submodule.toLinearPMap_graph_eq {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (g : Submodule R (E × F)) (hg : xg, x.1 = 0x.2 = 0) :
g.toLinearPMap.graph = g
theorem Submodule.toLinearPMap_range {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (g : Submodule R (E × F)) (hg : xg, x.1 = 0x.2 = 0) :
LinearMap.range g.toLinearPMap.toFun = Submodule.map (LinearMap.snd R E F) g
noncomputable def LinearPMap.inverse {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] (f : E →ₗ.[R] F) :

The inverse of a LinearPMap.

Equations
Instances For
theorem LinearPMap.inverse_domain {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} :
f.inverse.domain = LinearMap.range f.toFun
theorem LinearPMap.mem_inverse_graph_snd_eq_zero {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ) (x : F × E) (hv : x Submodule.map (LinearEquiv.prodComm R E F) f.graph) (hv' : x.1 = 0) :
x.2 = 0

The graph of the inverse generates a LinearPMap.

theorem LinearPMap.inverse_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ) :
f.inverse.graph = Submodule.map (LinearEquiv.prodComm R E F) f.graph
theorem LinearPMap.inverse_range {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ) :
LinearMap.range f.inverse.toFun = f.domain
theorem LinearPMap.mem_inverse_graph {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ) (x : { x : E // x f.domain }) :
(f x, x) f.inverse.graph
theorem LinearPMap.inverse_apply_eq {R : Type u_1} [Ring R] {E : Type u_2} [] [Module R E] {F : Type u_3} [] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ) {y : { x : F // x f.inverse.domain }} {x : { x : E // x f.domain }} (hxy : f x = y) :
f.inverse y = x