Documentation

Mathlib.LinearAlgebra.LinearPMap

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) [AddCommGroup E] [Module R E] (F : Type w) [AddCommGroup F] [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 : Submodule R E
toFun : ↥self.domain →ₗ[R] F

Instances For

def «term_→ₗ.[_]_» :

Lean.TrailingParserDescr

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.

def LinearPMap.toFun' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :

↥f.domain → F

Equations

↑f = ⇑f.toFun

instance LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

CoeFun (E →ₗ.[R] F) fun (f : E →ₗ.[R] F) => ↥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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x : ↥f.domain) :

f.toFun x = ↑f x

theorem LinearPMap.ext {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y) :

f = g

@[simp]

theorem LinearPMap.map_zero {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :

↑f 0 = 0

theorem LinearPMap.ext_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} :

f = g ↔ ∃ (_ : f.domain = g.domain), ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

theorem LinearPMap.ext' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {s : Submodule R E} {f g : ↥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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x y : ↥f.domain) :

↑f (x + y) = ↑f x + ↑f y

theorem LinearPMap.map_neg {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x : ↥f.domain) :

↑f (-x) = -↑f x

theorem LinearPMap.map_sub {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x y : ↥f.domain) :

↑f (x - y) = ↑f x - ↑f y

theorem LinearPMap.map_smul {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (c : R) (x : ↥f.domain) :

↑f (c • x) = c • ↑f x

@[simp]

theorem LinearPMap.mk_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (f : ↥p →ₗ[R] F) (x : ↥p) :

↑{ domain := p, toFun := f } x = f x

noncomputable def LinearPMap.mkSpanSingleton' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → c • 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.

@[simp]

theorem LinearPMap.domain_mkSpanSingleton {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → c • y = 0) :

(LinearPMap.mkSpanSingleton' x y H).domain = Submodule.span R {x}

@[simp]

theorem LinearPMap.mkSpanSingleton'_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → c • y = 0) (c : R) (h : c • x ∈ (LinearPMap.mkSpanSingleton' x y H).domain) :

↑(LinearPMap.mkSpanSingleton' x y H) ⟨c • x, h⟩ = c • y

@[simp]

theorem LinearPMap.mkSpanSingleton'_apply_self {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → c • y = 0) (h : x ∈ (LinearPMap.mkSpanSingleton' x y H).domain) :

↑(LinearPMap.mkSpanSingleton' x y H) ⟨x, h⟩ = y

@[reducible, inline]

noncomputable abbrev LinearPMap.mkSpanSingleton {K : Type u_5} {E : Type u_6} {F : Type u_7} [DivisionRing K] [AddCommGroup E] [Module K E] [AddCommGroup F] [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

LinearPMap.mkSpanSingleton x y hx = LinearPMap.mkSpanSingleton' x y ⋯

theorem LinearPMap.mkSpanSingleton_apply (K : Type u_5) {E : Type u_6} {F : Type u_7} [DivisionRing K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] {x : E} (hx : x ≠ 0) (y : F) :

↑(LinearPMap.mkSpanSingleton x y hx) ⟨x, ⋯⟩ = y

def LinearPMap.fst {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R F) :

E × F →ₗ.[R] E

Projection to the first coordinate as a LinearPMap

Equations

LinearPMap.fst p p' = { domain := p.prod p', toFun := LinearMap.fst R E F ∘ₗ (p.prod p').subtype }

@[simp]

theorem LinearPMap.fst_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R F) :

E × F →ₗ.[R] F

Projection to the second coordinate as a LinearPMap

Equations

LinearPMap.snd p p' = { domain := p.prod p', toFun := LinearMap.snd R E F ∘ₗ (p.prod p').subtype }

@[simp]

theorem LinearPMap.snd_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

LE (E →ₗ.[R] F)

Equations

LinearPMap.le = { le := fun (f g : E →ₗ.[R] F) => f.domain ≤ g.domain ∧ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y }

theorem LinearPMap.apply_comp_inclusion {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {T S : E →ₗ.[R] F} (h : T ≤ S) (x : ↥T.domain) :

↑T x = ↑S ((Submodule.inclusion ⋯) x)

theorem LinearPMap.exists_of_le {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {T S : E →ₗ.[R] F} (h : T ≤ S) (x : ↥T.domain) :

∃ (y : ↥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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (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' := ⋯ }

instance LinearPMap.bot {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

Inhabited (E →ₗ.[R] F)

Equations

LinearPMap.inhabited = { default := ⊥ }

instance LinearPMap.semilatticeInf {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

SemilatticeInf (E →ₗ.[R] F)

Equations

LinearPMap.semilatticeInf = SemilatticeInf.mk (fun (f g : E →ₗ.[R] F) => { domain := f.eqLocus g, toFun := f.toFun ∘ₗ Submodule.inclusion ⋯ }) ⋯ ⋯ ⋯

instance LinearPMap.orderBot {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

OrderBot (E →ₗ.[R] F)

Equations

LinearPMap.orderBot = OrderBot.mk ⋯

theorem LinearPMap.le_of_eqLocus_ge {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

StrictMono LinearPMap.domain

noncomputable def LinearPMap.sup {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f 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 := Classical.choose ⋯ }

@[simp]

theorem LinearPMap.domain_sup {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} (H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) (x : ↥f.domain) (y : ↥g.domain) (z : ↥(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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) :

f ≤ f.sup g h

theorem LinearPMap.right_le_sup {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) :

g ≤ f.sup g h

theorem LinearPMap.sup_le {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g h : E →ₗ.[R] F} (H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (h : Disjoint f.domain g.domain) (x : ↥f.domain) (y : ↥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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

Zero (E →ₗ.[R] F)

Equations

LinearPMap.instZero = { zero := { domain := ⊤, toFun := 0 } }

@[simp]

theorem LinearPMap.zero_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

LinearPMap.domain 0 = ⊤

@[simp]

theorem LinearPMap.zero_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : ↥⊤) :

↑0 x = 0

instance LinearPMap.instSMul {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] :

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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] (a : M) (f : E →ₗ.[R] F) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] (a : M) (f : E →ₗ.[R] F) :

↑(a • f) = a • ↑f

instance LinearPMap.instSMulCommClass {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} {N : Type u_6} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] [Monoid N] [DistribMulAction N F] [SMulCommClass R N F] [SMulCommClass M N F] :

SMulCommClass M N (E →ₗ.[R] F)

Equations

⋯ = ⋯

instance LinearPMap.instIsScalarTower {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} {N : Type u_6} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] [Monoid N] [DistribMulAction N F] [SMulCommClass R N F] [SMul M N] [IsScalarTower M N F] :

IsScalarTower M N (E →ₗ.[R] F)

Equations

⋯ = ⋯

instance LinearPMap.instMulAction {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] :

MulAction M (E →ₗ.[R] F)

Equations

LinearPMap.instMulAction = MulAction.mk ⋯ ⋯

instance LinearPMap.instNeg {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x : ↥(-f).domain) :

↑(-f) x = -↑f x

instance LinearPMap.instInvolutiveNeg {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

InvolutiveNeg (E →ₗ.[R] F)

Equations

LinearPMap.instInvolutiveNeg = InvolutiveNeg.mk ⋯

instance LinearPMap.instAdd {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

Add (E →ₗ.[R] F)

Equations

LinearPMap.instAdd = { add := fun (f g : E →ₗ.[R] F) => { domain := f.domain ⊓ g.domain, toFun := f.toFun ∘ₗ Submodule.inclusion ⋯ + g.toFun ∘ₗ Submodule.inclusion ⋯ } }

theorem LinearPMap.add_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

AddSemigroup (E →ₗ.[R] F)

Equations

LinearPMap.instAddSemigroup = AddSemigroup.mk ⋯

instance LinearPMap.instAddZeroClass {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

AddZeroClass (E →ₗ.[R] F)

Equations

LinearPMap.instAddZeroClass = AddZeroClass.mk ⋯ ⋯

instance LinearPMap.instAddMonoid {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

AddMonoid (E →ₗ.[R] F)

Equations

LinearPMap.instAddMonoid = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

instance LinearPMap.instAddCommMonoid {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

AddCommMonoid (E →ₗ.[R] F)

Equations

LinearPMap.instAddCommMonoid = AddCommMonoid.mk ⋯

instance LinearPMap.instVAdd {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ[R] F) (g : E →ₗ.[R] F) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

AddAction (E →ₗ[R] F) (E →ₗ.[R] F)

Equations

LinearPMap.instAddAction = AddAction.mk ⋯ ⋯

instance LinearPMap.instSub {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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 ∘ₗ Submodule.inclusion ⋯ - g.toFun ∘ₗ Submodule.inclusion ⋯ } }

theorem LinearPMap.sub_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :

SubtractionCommMonoid (E →ₗ.[R] F)

Equations

LinearPMap.instSubtractionCommMonoid = SubtractionCommMonoid.mk ⋯

noncomputable def LinearPMap.supSpanSingleton {E : Type u_2} [AddCommGroup E] {F : Type u_3} [AddCommGroup F] {K : Type u_5} [DivisionRing K] [Module K E] [Module K F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) :

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

Equations

f.supSpanSingleton x y hx = f.sup (LinearPMap.mkSpanSingleton x y ⋯) ⋯

@[simp]

theorem LinearPMap.domain_supSpanSingleton {E : Type u_2} [AddCommGroup E] {F : Type u_3} [AddCommGroup F] {K : Type u_5} [DivisionRing K] [Module K E] [Module K F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) :

(f.supSpanSingleton x y hx).domain = f.domain ⊔ Submodule.span K {x}

@[simp]

theorem LinearPMap.supSpanSingleton_apply_mk {E : Type u_2} [AddCommGroup E] {F : Type u_3} [AddCommGroup F] {K : Type u_5} [DivisionRing K] [Module K E] [Module K F] (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (c : Set (E →ₗ.[R] F)) (hc : DirectedOn (fun (x1 x2 : E →ₗ.[R] F) => x1 ≤ x2) c) :

Equations

LinearPMap.sSup c hc = { domain := sSup (LinearPMap.domain '' c), toFun := Classical.choose ⋯ }

theorem LinearPMap.le_sSup {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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 ≤ LinearPMap.sSup c hc

theorem LinearPMap.sSup_le {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (fun (x1 x2 : E →ₗ.[R] F) => x1 ≤ x2) c) {g : E →ₗ.[R] F} (hg : ∀ f ∈ c, f ≤ g) :

LinearPMap.sSup c hc ≤ g

theorem LinearPMap.sSup_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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 : ↥l.domain) :

↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩ = ↑l x

def LinearMap.toPMap {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ[R] F) (p : Submodule R E) :

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

Equations

f.toPMap p = { domain := p, toFun := f ∘ₗ p.subtype }

@[simp]

theorem LinearMap.toPMap_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ[R] F) (p : Submodule R E) (x : ↥p) :

↑(f.toPMap p) x = f ↑x

@[simp]

theorem LinearMap.toPMap_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ[R] F) (p : Submodule R E) :

(f.toPMap p).domain = p

def LinearMap.compPMap {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [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 }

@[simp]

theorem LinearMap.compPMap_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] (g : F →ₗ[R] G) (f : E →ₗ.[R] F) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (p : Submodule R F) (H : ∀ (x : ↥f.domain), ↑f x ∈ p) :

E →ₗ.[R] ↥p

Restrict codomain of a LinearPMap

Equations

f.codRestrict p H = { domain := f.domain, toFun := LinearMap.codRestrict p f.toFun H }

def LinearPMap.comp {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) (H : ∀ (x : ↥f.domain), ↑f x ∈ g.domain) :

Compose two LinearPMaps

Equations

g.comp f H = g.toFun.compPMap (f.codRestrict g.domain H)

def LinearPMap.coprod {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [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 }

@[simp]

theorem LinearPMap.coprod_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (S : Submodule R E) :

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 ∘ₗ Submodule.inclusion ⋯ }

@[simp]

theorem LinearPMap.domRestrict_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) {S : Submodule R E} :

(f.domRestrict S).domain = S ⊓ f.domain

theorem LinearPMap.domRestrict_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} {S : Submodule R E} ⦃x : ↥(S ⊓ f.domain)⦄ ⦃y : ↥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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} {S : Submodule R E} :

f.domRestrict S ≤ f

Graph #

def LinearPMap.graph {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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

theorem LinearPMap.mem_graph_iff' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) {x : E × F} :

x ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y, ↑f y) = x

@[simp]

theorem LinearPMap.mem_graph_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) {x : E × F} :

x ∈ f.graph ↔ ∃ (y : ↥f.domain), ↑y = x.1 ∧ ↑f y = x.2

theorem LinearPMap.mem_graph {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :

Submodule.map (LinearMap.snd R E F) f.graph = LinearMap.range f.toFun

theorem LinearPMap.smul_graph {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) {x y : E} {x' 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) {x 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} {y : F} :

y ∈ Set.range ↑f ↔ ∃ (x : E), (x, y) ∈ f.graph

theorem LinearPMap.mem_domain_iff_of_eq_graph {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) {a : E} (ha : a ∈ Submodule.map (LinearMap.fst R E F) g) :

F

Auxiliary definition to unfold the existential quantifier.

Equations

Submodule.valFromGraph hg ha = ⋯.choose

theorem Submodule.valFromGraph_mem {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) {a : E} (ha : a ∈ Submodule.map (LinearMap.fst R E F) g) :

(a, Submodule.valFromGraph hg ha) ∈ g

noncomputable def Submodule.toLinearPMapAux {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) :

↥(Submodule.map (LinearMap.fst R E F) g) →ₗ[R] F

Define a LinearMap from its graph.

Helper definition for LinearPMap.

Equations

g.toLinearPMapAux hg = { toFun := fun (x : ↥(Submodule.map (LinearMap.fst R E F) g)) => Submodule.valFromGraph hg ⋯, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Submodule.toLinearPMap {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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 : ∀ x ∈ g, x.1 = 0 → x.2 = 0 then g.toLinearPMapAux hg else 0 }

theorem Submodule.toLinearPMap_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) (x : ↥(Submodule.map (LinearMap.fst R E F) g)) :

↑g.toLinearPMap x = Submodule.valFromGraph hg ⋯

theorem Submodule.mem_graph_toLinearPMap {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) (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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) :

g.toLinearPMap.graph = g

theorem Submodule.toLinearPMap_range {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :

The inverse of a LinearPMap.

Equations

f.inverse = (Submodule.map (LinearEquiv.prodComm R E F) f.graph).toLinearPMap

theorem LinearPMap.inverse_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) (x : ↥f.domain) :

(↑f x, ↑x) ∈ f.inverse.graph

theorem LinearPMap.inverse_apply_eq {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) {y : ↥f.inverse.domain} {x : ↥f.domain} (hxy : ↑f x = ↑y) :

↑f.inverse y = ↑x