Partially defined linear maps

A LinearPMap σ E F or E →ₛₗ.[σ] F is a semilinear map from a submodule of E to F with a ring homomorphism σ between the scalars. This reduces to a linear map when σ is the identity. 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. TODO: This should be also generalized to semilinear maps, but one has to define a new type where R acts on E normally while R acts on F through σ.

Partially defined maps are currently used in Mathlib to prove the 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_1} {S : Type u_2} [Ring R] [Ring S] (σ : R →+* S) (E : Type u_3) [AddCommGroup E] [Module R E] (F : Type u_4) [AddCommGroup F] [Module S F] : Type (max u_3 u_4)

A LinearPMap σ E F or E →ₛₗ.[σ] F is a (semi)linear map from a submodule of E to F.

• domain : Submodule R E

  The domain of the (semi)linear map.

• toFun : ↥self.domain →ₛₗ[σ] F

  The (semi)linear map itself.

def «term_→ₛₗ.[_]_» : Lean.TrailingParserDescr

A LinearPMap σ E F or E →ₛₗ.[σ] F is a (semi)linear map from a submodule of E to F.

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

E →ₗ.[R] F is the notation for E →ₛₗ.[RingHom.id R] F.

def LinearPMap.toFun' {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) : ↥f.domain → F

The (semi)linear map as just a function.

@[implicit_reducible]

instance LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : CoeFun (E →ₛₗ.[σ] F) fun (f : E →ₛₗ.[σ] F) => ↥f.domain → F

@[simp]

theorem LinearPMap.toFun_eq_coe {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) (x : ↥f.domain) : f.toFun x = ↑f x

theorem LinearPMap.ext {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩) : f = g

theorem LinearPMap.dExt {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y) : f = g

A dependent version of ext.

@[simp]

theorem LinearPMap.map_zero {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) : ↑f 0 = 0

theorem LinearPMap.ext_iff {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] F} : f = g ↔ f.domain = g.domain ∧ ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩

theorem LinearPMap.dExt_iff {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {s : Submodule R E} {f g : ↥s →ₛₗ[σ] F} (h : f = g) : { domain := s, toFun := f } = { domain := s, toFun := g }

theorem LinearPMap.map_add {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) (x y : ↥f.domain) : ↑f (x + y) = ↑f x + ↑f y

theorem LinearPMap.map_neg {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) (x : ↥f.domain) : ↑f (-x) = -↑f x

theorem LinearPMap.map_sub {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] 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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (c : R) (x : ↥f.domain) : ↑f (c • x) = c • ↑f x

theorem LinearPMap.map_smulₛₗ {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) (c : R) (x : ↥f.domain) : ↑f (c • x) = σ c • ↑f x

@[simp]

theorem LinearPMap.mk_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (p : Submodule R E) (f : ↥p →ₛₗ[σ] F) (x : ↥p) : ↑{ domain := p, toFun := f } x = f x

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

@[simp]

theorem LinearPMap.domain_mkSpanSingleton {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → σ c • y = 0) : (mkSpanSingleton' x y H).domain = R ∙ x

@[simp]

theorem LinearPMap.mkSpanSingleton'_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → σ c • y = 0) (c : R) (h : c • x ∈ (mkSpanSingleton' x y H).domain) : ↑(mkSpanSingleton' x y H) ⟨c • x, h⟩ = σ c • y

@[simp]

theorem LinearPMap.mkSpanSingleton'_apply_self {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → σ c • y = 0) (h : x ∈ (mkSpanSingleton' x y H).domain) : ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = y

@[reducible, inline]

noncomputable abbrev LinearPMap.mkSpanSingleton {K : Type u_7} {L : Type u_8} {E : Type u_9} {F : Type u_10} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [AddCommGroup E] [Module K E] [AddCommGroup F] [Module L F] (x : E) (y : F) (hx : x ≠ 0) : E →ₛₗ.[σ] 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.

theorem LinearPMap.mkSpanSingleton_apply (K : Type u_7) (L : Type u_8) {E : Type u_9} {F : Type u_10} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [AddCommGroup E] [Module K E] [AddCommGroup F] [Module L F] {x : E} (hx : x ≠ 0) (y : F) : ↑(mkSpanSingleton x y hx) ⟨x, ⋯⟩ = y

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

@[simp]

theorem LinearPMap.fst_apply {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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

@[simp]

theorem LinearPMap.snd_apply {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R F) (x : ↥(p.prod p')) : ↑(LinearPMap.snd p p') x = (↑x).2

@[implicit_reducible]

instance LinearPMap.le {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : LE (E →ₛₗ.[σ] F)

theorem LinearPMap.apply_comp_inclusion {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {T S✝ : E →ₛₗ.[σ] F} (h : T ≤ S✝) (x : ↥T.domain) : ↑T x = ↑S✝ ((Submodule.inclusion ⋯) x)

theorem LinearPMap.exists_of_le {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {T S✝ : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] F} (hle : f ≤ g) (heq : f.domain = g.domain) : f = g

def LinearPMap.eqLocus {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] 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.

@[implicit_reducible]

instance LinearPMap.bot {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : Bot (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.inhabited {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : Inhabited (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.semilatticeInf {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : SemilatticeInf (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.orderBot {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : OrderBot (E →ₛₗ.[σ] F)

theorem LinearPMap.le_of_eqLocus_ge {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] F} (H : f.domain ≤ f.eqLocus g) : f ≤ g

theorem LinearPMap.domain_mono {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : StrictMono domain

noncomputable def LinearPMap.sup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] F) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) : E →ₛₗ.[σ] 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.

@[simp]

theorem LinearPMap.domain_sup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f g h : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] 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

@[implicit_reducible]

instance LinearPMap.instZero {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : Zero (E →ₛₗ.[σ] F)

@[simp]

theorem LinearPMap.zero_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : domain 0 = ⊤

@[simp]

theorem LinearPMap.zero_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (x : ↥⊤) : ↑0 x = 0

@[implicit_reducible]

instance LinearPMap.instSMul {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] : SMul M (E →ₛₗ.[σ] F)

@[simp]

theorem LinearPMap.smul_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] (a : M) (f : E →ₛₗ.[σ] F) : (a • f).domain = f.domain

theorem LinearPMap.smul_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] (a : M) (f : E →ₛₗ.[σ] F) (x : ↥(a • f).domain) : ↑(a • f) x = a • ↑f x

@[simp]

theorem LinearPMap.coe_smul {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] (a : M) (f : E →ₛₗ.[σ] F) : ↑(a • f) = a • ↑f

instance LinearPMap.instSMulCommClass {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} {N : Type u_8} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] [Monoid N] [DistribMulAction N F] [SMulCommClass S N F] [SMulCommClass M N F] : SMulCommClass M N (E →ₛₗ.[σ] F)

instance LinearPMap.instIsScalarTower {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} {N : Type u_8} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] [Monoid N] [DistribMulAction N F] [SMulCommClass S N F] [SMul M N] [IsScalarTower M N F] : IsScalarTower M N (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instMulAction {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass S M F] : MulAction M (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instNeg {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : Neg (E →ₛₗ.[σ] F)

@[simp]

theorem LinearPMap.neg_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) : (-f).domain = f.domain

@[simp]

theorem LinearPMap.neg_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) (x : ↥(-f).domain) : ↑(-f) x = -↑f x

@[implicit_reducible]

instance LinearPMap.instInvolutiveNeg {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : InvolutiveNeg (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instAdd {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : Add (E →ₛₗ.[σ] F)

theorem LinearPMap.add_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] F) : (f + g).domain = f.domain ⊓ g.domain

theorem LinearPMap.add_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] F) (x : ↥(f.domain ⊓ g.domain)) : ↑(f + g) x = ↑f ⟨↑x, ⋯⟩ + ↑g ⟨↑x, ⋯⟩

@[implicit_reducible]

instance LinearPMap.instAddSemigroup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : AddSemigroup (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instAddZeroClass {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : AddZeroClass (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instAddMonoid {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : AddMonoid (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instAddCommMonoid {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : AddCommMonoid (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instVAdd {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : VAdd (E →ₛₗ[σ] F) (E →ₛₗ.[σ] F)

@[simp]

theorem LinearPMap.vadd_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ[σ] F) (g : E →ₛₗ.[σ] F) : (f +ᵥ g).domain = g.domain

theorem LinearPMap.vadd_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ[σ] F) (g : E →ₛₗ.[σ] F) (x : ↥(f +ᵥ g).domain) : ↑(f +ᵥ g) x = f ↑x + ↑g x

@[simp]

theorem LinearPMap.coe_vadd {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ[σ] F) (g : E →ₛₗ.[σ] F) : ↑(f +ᵥ g) = ⇑(f ∘ₛₗ g.domain.subtype) + ↑g

@[implicit_reducible]

instance LinearPMap.instAddAction {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : AddAction (E →ₛₗ[σ] F) (E →ₛₗ.[σ] F)

@[implicit_reducible]

instance LinearPMap.instSub {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : Sub (E →ₛₗ.[σ] F)

theorem LinearPMap.sub_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] F) : (f - g).domain = f.domain ⊓ g.domain

theorem LinearPMap.sub_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f g : E →ₛₗ.[σ] F) (x : ↥(f.domain ⊓ g.domain)) : ↑(f - g) x = ↑f ⟨↑x, ⋯⟩ - ↑g ⟨↑x, ⋯⟩

@[implicit_reducible]

instance LinearPMap.instSubtractionCommMonoid {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] : SubtractionCommMonoid (E →ₛₗ.[σ] F)

noncomputable def LinearPMap.supSpanSingleton {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] F) (x : E) (y : F) (hx : x ∉ f.domain) : E →ₛₗ.[σ] F

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

@[simp]

theorem LinearPMap.domain_supSpanSingleton {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] F) (x : E) (y : F) (hx : x ∉ f.domain) : (f.supSpanSingleton x y hx).domain = f.domain ⊔ K ∙ x

@[simp]

theorem LinearPMap.supSpanSingleton_apply_mk {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] 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

@[simp]

theorem LinearPMap.supSpanSingleton_apply_smul_self {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) (c : K) : ↑(f.supSpanSingleton x y hx) ⟨c • x, ⋯⟩ = σ c • y

@[simp]

theorem LinearPMap.supSpanSingleton_apply_self {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) : ↑(f.supSpanSingleton x y hx) ⟨x, ⋯⟩ = y

theorem LinearPMap.supSpanSingleton_apply_of_mem {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) (x' : ↥(f.supSpanSingleton x y hx).domain) (hx' : ↑x' ∈ f.domain) : ↑(f.supSpanSingleton x y hx) x' = ↑f ⟨↑x', hx'⟩

theorem LinearPMap.supSpanSingleton_apply_mk_of_mem {E : Type u_4} [AddCommGroup E] {F : Type u_5} [AddCommGroup F] {K : Type u_7} {L : Type u_8} [DivisionRing K] [DivisionRing L] {σ : K →+* L} [Module K E] [Module L F] (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) {x' : E} (hx' : x' ∈ f.domain) : ↑(f.supSpanSingleton x y hx) ⟨x', ⋯⟩ = ↑f ⟨x', hx'⟩

noncomputable def LinearPMap.sSup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (c : Set (E →ₛₗ.[σ] F)) (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) => x1 ≤ x2) c) : E →ₛₗ.[σ] F

For a family of (semi)linear maps with a directed domains such that the one defined on a larger domain restricts to the one defined on the smaller domain, this defines the (semi)linear map defined on the union of the domains extending all the (semi)linear maps in the family.

theorem LinearPMap.domain_sSup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {c : Set (E →ₛₗ.[σ] F)} (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) => x1 ≤ x2) c) : (LinearPMap.sSup c hc).domain = sSup (domain '' c)

theorem LinearPMap.mem_domain_sSup_iff {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {c : Set (E →ₛₗ.[σ] F)} (hnonempty : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) => x1 ≤ x2) c) {x : E} : x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain

theorem LinearPMap.le_sSup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {c : Set (E →ₛₗ.[σ] F)} (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) => x1 ≤ x2) c) {f : E →ₛₗ.[σ] F} (hf : f ∈ c) : f ≤ LinearPMap.sSup c hc

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

theorem LinearPMap.sSup_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {c : Set (E →ₛₗ.[σ] F)} (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) => x1 ≤ x2) c) {l : E →ₛₗ.[σ] F} (hl : l ∈ c) (x : ↥l.domain) : ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩ = ↑l x

def LinearMap.toPMap {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ[σ] F) (p : Submodule R E) : E →ₛₗ.[σ] F

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

@[simp]

theorem LinearMap.toPMap_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ[σ] F) (p : Submodule R E) (x : ↥p) : ↑(f.toPMap p) x = f ↑x

@[simp]

theorem LinearMap.toPMap_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ[σ] F) (p : Submodule R E) : (f.toPMap p).domain = p

def LinearMap.compPMap {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Ring T] {σ : R →+* S} {τ : S →+* T} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {G : Type u_6} [AddCommGroup G] [Module T G] {ρ : R →+* T} [RingHomCompTriple σ τ ρ] (g : F →ₛₗ[τ] G) (f : E →ₛₗ.[σ] F) : E →ₛₗ.[ρ] G

Compose a linear map with a LinearPMap

@[simp]

theorem LinearMap.compPMap_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Ring T] {σ : R →+* S} {τ : S →+* T} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {G : Type u_6} [AddCommGroup G] [Module T G] (g : F →ₛₗ[τ] G) (f : E →ₛₗ.[σ] F) (x : ↥(g.compPMap f).domain) : ↑(g.compPMap f) x = g (↑f x)

def LinearPMap.codRestrict {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) (p : Submodule S F) (H : ∀ (x : ↥f.domain), ↑f x ∈ p) : E →ₛₗ.[σ] ↥p

Restrict codomain of a LinearPMap

def LinearPMap.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Ring T] {σ : R →+* S} {τ : S →+* T} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {G : Type u_6} [AddCommGroup G] [Module T G] {ρ : R →+* T} [RingHomCompTriple σ τ ρ] (g : F →ₛₗ.[τ] G) (f : E →ₛₗ.[σ] F) (H : ∀ (x : ↥f.domain), ↑f x ∈ g.domain) : E →ₛₗ.[ρ] G

Compose two LinearPMaps

def LinearPMap.coprod {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] {G : Type u_6} [AddCommGroup G] [Module R F] [Module S G] (f : E →ₛₗ.[σ] G) (g : F →ₛₗ.[σ] G) : E × F →ₛₗ.[σ] 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.

@[simp]

theorem LinearPMap.coprod_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] {G : Type u_6} [AddCommGroup G] [Module R F] [Module S G] (f : E →ₛₗ.[σ] G) (g : F →ₛₗ.[σ] G) (x : ↥(f.coprod g).domain) : ↑(f.coprod g) x = ↑f ⟨(↑x).1, ⋯⟩ + ↑g ⟨(↑x).2, ⋯⟩

def LinearPMap.domRestrict {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) : Submodule R E → E →ₛₗ.[σ] F

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

@[simp]

theorem LinearPMap.domRestrict_domain {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] (f : E →ₛₗ.[σ] F) {S✝ : Submodule R E} : (f.domRestrict S✝).domain = S✝ ⊓ f.domain

theorem LinearPMap.domRestrict_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f : E →ₛₗ.[σ] 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} {S : Type u_2} [Ring R] [Ring S] {σ : R →+* S} {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module S F] {f : E →ₛₗ.[σ] F} {S✝ : Submodule R E} : f.domRestrict S✝ ≤ f

Graph

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

theorem LinearPMap.mem_graph_iff' {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : Submodule.map (LinearMap.snd R E F) f.graph = f.toFun.range

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

Auxiliary definition to unfold the existential quantifier.

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

noncomputable def Submodule.toLinearPMapAux {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) : ↥(map (LinearMap.fst R E F) g) →ₗ[R] F

Define a LinearMap from its graph.

Helper definition for LinearPMap.

noncomputable def Submodule.toLinearPMap {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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.

theorem Submodule.toLinearPMap_domain {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) : g.toLinearPMap.domain = map (LinearMap.fst R E F) g

theorem Submodule.toLinearPMap_apply_aux {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) (x : ↥(map (LinearMap.fst R E F) g)) : ↑g.toLinearPMap x = valFromGraph hg ⋯

theorem Submodule.mem_graph_toLinearPMap {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) (x : ↥(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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) : g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g

noncomputable def LinearPMap.inverse {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : F →ₗ.[R] E

The inverse of a LinearPMap.

theorem LinearPMap.inverse_domain {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} : f.inverse.domain = f.toFun.range

theorem LinearPMap.mem_inverse_graph_snd_eq_zero {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : f.toFun.ker = ⊥) (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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : f.toFun.ker = ⊥) : 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_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : f.toFun.ker = ⊥) : f.inverse.toFun.range = f.domain

theorem LinearPMap.mem_inverse_graph {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : f.toFun.ker = ⊥) (x : ↥f.domain) : (↑f x, ↑x) ∈ f.inverse.graph

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