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

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.instCoeFunLinearPMapForAllSubtypeMemSubmoduleToSemiringToAddCommMonoidInstMembershipSetLikeDomain {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.instCoeFunLinearPMapForAllSubtypeMemSubmoduleToSemiringToAddCommMonoidInstMembershipSetLikeDomain = { 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 : E →ₗ.[R] 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 : E →ₗ.[R] 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 : ↥s →ₗ[R] 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 : ↥f.domain) (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 : ↥f.domain) (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) : E →ₗ.[R] F

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) { val := c • x, property := 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) { val := x, property := h } = y

@[reducible]

noncomputable def 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) : E →ₗ.[K] F

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 (_ : ∀ (c : K), c • x = 0 → c • y = 0)

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) { val := x, property := (_ : x ∈ Submodule.span K {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 := Submodule.prod p p', toFun := LinearMap.comp (LinearMap.fst R E F) (Submodule.subtype (Submodule.prod p p')) }

@[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 : ↥(Submodule.prod p 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 := Submodule.prod p p', toFun := LinearMap.comp (LinearMap.snd R E F) (Submodule.subtype (Submodule.prod p p')) }

@[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 : ↥(Submodule.prod p 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 : E →ₗ.[R] F} {S : E →ₗ.[R] F} (h : T ≤ S) (x : ↥T.domain) : ↑T x = ↑S ((Submodule.inclusion (_ : T.domain ≤ S.domain)) 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 : E →ₗ.[R] F} {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 : 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) : Submodule R E

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

• One or more equations did not get rendered due to their size.

instance LinearPMap.inf {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] : Inf (E →ₗ.[R] F)

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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 (_ : ∀ (f : E →ₗ.[R] F), ⊥.domain ≤ f.domain ∧ ∀ ⦃x : ↥⊥.domain⦄ ⦃y : ↥f.domain⦄, ↑x = ↑y → ↑⊥ x = ↑f y)

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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} (H : f.domain ≤ LinearPMap.eqLocus f 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 : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) : E →ₗ.[R] F

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

• One or more equations did not get rendered due to their size.

@[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 : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) : (LinearPMap.sup f 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 : E →ₗ.[R] 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) : ↑(LinearPMap.sup f 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 : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) : f ≤ LinearPMap.sup f 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 : E →ₗ.[R] F) (g : E →ₗ.[R] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) : g ≤ LinearPMap.sup f 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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} {h : E →ₗ.[R] F} (H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) (fh : f ≤ h) (gh : g ≤ h) : LinearPMap.sup f 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 : E →ₗ.[R] 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] : 0.domain = ⊤

@[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

• (_ : SMulCommClass M N (E →ₗ.[R] F)) = (_ : SMulCommClass M N (E →ₗ.[R] F))

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

• (_ : IsScalarTower M N (E →ₗ.[R] F)) = (_ : IsScalarTower M N (E →ₗ.[R] F))

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

• One or more equations did not get rendered due to their size.

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 (_ : ∀ (f : E →ₗ.[R] F), - -f = f)

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

• One or more equations did not get rendered due to their size.

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 : 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (x : ↥(f.domain ⊓ g.domain)) : ↑(f + g) x = ↑f { val := ↑x, property := (_ : ↑x ∈ ↑f.domain) } + ↑g { val := ↑x, property := (_ : ↑x ∈ ↑g.domain) }

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 (_ : ∀ (f g h : E →ₗ.[R] F), f + g + h = f + (g + h))

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 (_ : ∀ (f : E →ₗ.[R] F), 0 + f = f) (_ : ∀ (f : E →ₗ.[R] F), f + 0 = f)

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 (_ : ∀ (f : E →ₗ.[R] F), 0 + f = f) (_ : ∀ (a : E →ₗ.[R] F), a + 0 = a) 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 (_ : ∀ (f g : E →ₗ.[R] F), f + g = g + f)

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 := LinearMap.comp f (Submodule.subtype g.domain) + 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 ∘ₗ Submodule.subtype g.domain) + ↑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 (_ : ∀ (x : E →ₗ.[R] F), 0 +ᵥ x = x) (_ : ∀ (_f₁ _f₂ : E →ₗ[R] F) (x : E →ₗ.[R] F), _f₁ + _f₂ +ᵥ x = _f₁ +ᵥ (_f₂ +ᵥ x))

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

• One or more equations did not get rendered due to their size.

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 : 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} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (g : E →ₗ.[R] F) (x : ↥(f.domain ⊓ g.domain)) : ↑(f - g) x = ↑f { val := ↑x, property := (_ : ↑x ∈ ↑f.domain) } - ↑g { val := ↑x, property := (_ : ↑x ∈ ↑g.domain) }

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 (_ : ∀ (a b : E →ₗ.[R] F), a + b = b + a)

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) : E →ₗ.[K] F

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

Equations

• One or more equations did not get rendered due to their size.

@[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) : (LinearPMap.supSpanSingleton f 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) : ↑(LinearPMap.supSpanSingleton f x y hx) { val := x' + c • x, property := (_ : x' + c • x ∈ f.domain ⊔ (LinearPMap.mkSpanSingleton x y (_ : x = 0 → False)).domain) } = ↑f { val := x', property := 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 (x x_1 : E →ₗ.[R] F) => x ≤ x_1) c) : E →ₗ.[R] F

Equations

• One or more equations did not get rendered due to their size.

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 (x x_1 : E →ₗ.[R] F) => x ≤ x_1) 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 (x x_1 : E →ₗ.[R] F) => x ≤ x_1) 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 (x x_1 : E →ₗ.[R] F) => x ≤ x_1) c) {l : E →ₗ.[R] F} (hl : l ∈ c) (x : ↥l.domain) : ↑(LinearPMap.sSup c hc) { val := ↑x, property := (_ : ↑x ∈ (LinearPMap.sSup c hc).domain) } = ↑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) : E →ₗ.[R] F

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

Equations

• LinearMap.toPMap f p = { domain := p, toFun := LinearMap.comp f (Submodule.subtype p) }

@[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) : ↑(LinearMap.toPMap f 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) : (LinearMap.toPMap f 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) : E →ₗ.[R] G

Compose a linear map with a LinearPMap

Equations

• LinearMap.compPMap g f = { domain := f.domain, toFun := LinearMap.comp 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 : ↥(LinearMap.compPMap g f).domain) : ↑(LinearMap.compPMap g 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

• LinearPMap.codRestrict f 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) : E →ₗ.[R] G

Compose two LinearPMaps

Equations

• LinearPMap.comp g f H = LinearMap.compPMap g.toFun (LinearPMap.codRestrict f 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

• One or more equations did not get rendered due to their size.

@[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 : ↥(LinearPMap.coprod f g).domain) : ↑(LinearPMap.coprod f g) x = ↑f { val := (↑x).1, property := (_ : (↑x).1 ∈ ↑f.domain) } + ↑g { val := (↑x).2, property := (_ : (↑x).2 ∈ ↑g.domain) }

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) : E →ₗ.[R] F

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

Equations

• LinearPMap.domRestrict f S = { domain := S ⊓ f.domain, toFun := LinearMap.comp f.toFun (Submodule.inclusion (_ : S ⊓ f.domain ≤ f.domain)) }

@[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} : (LinearPMap.domRestrict f 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) : ↑(LinearPMap.domRestrict f 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} : LinearPMap.domRestrict f 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

• LinearPMap.graph f = Submodule.map (LinearMap.prodMap (Submodule.subtype f.domain) LinearMap.id) (LinearMap.graph f.toFun)

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 ∈ LinearPMap.graph f ↔ ∃ (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 ∈ LinearPMap.graph f ↔ ∃ (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) ∈ LinearPMap.graph f

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) (LinearPMap.graph f) = 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) (LinearPMap.graph f) = 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) : LinearPMap.graph (z • f) = Submodule.map (LinearMap.prodMap LinearMap.id (z • LinearMap.id)) (LinearPMap.graph f)

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) : LinearPMap.graph (-f) = Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) (LinearPMap.graph f)

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 : E} {y : E} {x' : F} {y' : F} (hx : (x, x') ∈ LinearPMap.graph f) (hy : (y, y') ∈ LinearPMap.graph f) (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 : E × F} {y : E × F} (hx : x ∈ LinearPMap.graph f) (hy : y ∈ LinearPMap.graph f) (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') ∈ LinearPMap.graph f) (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) ∈ LinearPMap.graph f

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) ∈ LinearPMap.graph f) : 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 { val := x, property := hx } ↔ (x, y) ∈ LinearPMap.graph f

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) ∈ LinearPMap.graph f

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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : LinearPMap.graph f = LinearPMap.graph g) {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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : LinearPMap.graph f ≤ LinearPMap.graph g) : 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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : f ≤ g) : LinearPMap.graph f ≤ LinearPMap.graph g

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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} : LinearPMap.graph f ≤ LinearPMap.graph g ↔ 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 : E →ₗ.[R] F} {g : E →ₗ.[R] F} (h : LinearPMap.graph f = LinearPMap.graph g) : 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 = Exists.choose (_ : ∃ (x : F), (a, x) ∈ g)

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

• One or more equations did not get rendered due to their size.

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)) : E →ₗ.[R] 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

• Submodule.toLinearPMap g = { domain := Submodule.map (LinearMap.fst R E F) g, toFun := if hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0 then Submodule.toLinearPMapAux g 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)) : (Submodule.toLinearPMap g).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)) : ↑(Submodule.toLinearPMap g) x = Submodule.valFromGraph hg (_ : ↑x ∈ Submodule.map (LinearMap.fst R E F) g)

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, ↑(Submodule.toLinearPMap g) 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) : LinearPMap.graph (Submodule.toLinearPMap g) = 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 (Submodule.toLinearPMap g).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) : F →ₗ.[R] E

The inverse of a LinearPMap.

Equations

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

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} : (LinearPMap.inverse f).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) (LinearPMap.graph f)) (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 = ⊥) : LinearPMap.graph (LinearPMap.inverse f) = Submodule.map (LinearEquiv.prodComm R E F) (LinearPMap.graph f)

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 (LinearPMap.inverse f).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) ∈ LinearPMap.graph (LinearPMap.inverse f)

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 : ↥(LinearPMap.inverse f).domain} {x : ↥f.domain} (hxy : ↑f x = ↑y) : ↑(LinearPMap.inverse f) y = ↑x