Mathlib.LinearAlgebra.LinearPMap

LinearPMap structure

(R : Type u) [Ring R] (E : Type v) [AddCommGroup E] [Module R E] (F : Type w) [AddCommGroup F] [Module R F]

Full source

/-- A `LinearPMap R E F` or `E →ₗ.[R] F` is a linear map from a submodule of `E` to `F`. -/
structure LinearPMap (R : Type u) [Ring R] (E : Type v) [AddCommGroup E] [Module R E] (F : Type w)
  [AddCommGroup F] [Module R F] where
  domain : Submodule R E
  toFun : domain →ₗ[R] F

Partially defined linear map

Informal description

A partially defined linear map from a submodule of $E$ to $F$ over a ring $R$, where $E$ and $F$ are modules over $R$ with additive commutative group structures.

term_→ₗ.[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] notation:25 E " →ₗ.[" R:25 "] " F:0 => LinearPMap R E F

Partially defined linear maps

Informal description

The notation `E →ₗ.[R] F` represents the type of partially defined linear maps from a submodule of `E` to `F` over the ring `R`. These are linear maps that are only defined on a subspace of `E` rather than the entire space.

LinearPMap.toFun' definition

(f : E →ₗ.[R] F) : f.domain → F

Full source

@[coe]
def toFun' (f : E →ₗ.[R] F) : f.domain → F := f.toFun

Underlying function of a partially defined linear map

Informal description

For a partially defined linear map $ f : E \to_{.[R]} F $, the function $ f.\text{toFun}' $ maps an element of the domain of $ f $ to an element of $ F $.

LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain instance

: CoeFun (E →ₗ.[R] F) fun f : E →ₗ.[R] F => f.domain → F

Full source

instance : CoeFun (E →ₗ.[R] F) fun f : E →ₗ.[R] F => f.domain → F :=
  ⟨toFun'⟩

Function Representation of Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, a partially defined linear map $f : E \to_{.[R]} F$ can be treated as a function from its domain (a submodule of $E$) to $F$.

LinearPMap.toFun_eq_coe theorem

(f : E →ₗ.[R] F) (x : f.domain) : f.toFun x = f x

Full source

@[simp]
theorem toFun_eq_coe (f : E →ₗ.[R] F) (x : f.domain) : f.toFun x = f x :=
  rfl

Equality of Underlying Function and Partial Linear Map

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ and any element $x$ in the domain of $f$, the value of the underlying function $f.\text{toFun}$ at $x$ is equal to the value of $f$ at $x$, i.e., $f.\text{toFun}(x) = f(x)$.

LinearPMap.ext theorem

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

Full source

@[ext (iff := false)]
theorem ext {f g : E →ₗ.[R] 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 := by
  rcases f with ⟨f_dom, f⟩
  rcases g with ⟨g_dom, g⟩
  obtain rfl : f_dom = g_dom := h
  congr
  apply LinearMap.ext
  intro x
  apply h'

Extensionality of Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any two partially defined linear maps $f, g \colon E \to_{.[R]} F$, if their domains are equal and for every $x \in E$ in their common domain, the images $f(x)$ and $g(x)$ coincide, then $f = g$.

LinearPMap.dExt theorem

 {f g : E →ₗ.[R] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y) :
  f = g

Full source

/-- A dependent version of `ext`. -/
theorem dExt {f g : E →ₗ.[R] F} (h : f.domain = g.domain)
    (h' : ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y) : f = g :=
  ext h fun _ _ _ ↦ h' rfl

Dependent Extensionality for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any two partially defined linear maps $f, g \colon E \to_{.[R]} F$, if their domains are equal and for every $x$ in the domain of $f$ and $y$ in the domain of $g$ such that $x = y$ as elements of $E$, we have $f(x) = g(y)$, then $f = g$.

LinearPMap.map_zero theorem

(f : E →ₗ.[R] F) : f 0 = 0

Full source

@[simp]
theorem map_zero (f : E →ₗ.[R] F) : f 0 = 0 :=
  f.toFun.map_zero

Partially Defined Linear Map Preserves Zero

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ between modules $E$ and $F$ over a ring $R$, the image of the zero vector under $f$ is the zero vector in $F$, i.e., $f(0) = 0$.

LinearPMap.ext_iff theorem

 {f g : E →ₗ.[R] F} :
  f = g ↔ f.domain = g.domain ∧ ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, f ⟨x, hf⟩ = g ⟨x, hg⟩

Full source

theorem ext_iff {f g : E →ₗ.[R] F} :
    f = g ↔
      f.domain = g.domain ∧
        ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, f ⟨x, hf⟩ = g ⟨x, hg⟩ :=
  ⟨by rintro rfl; simp, fun ⟨deq, feq⟩ ↦ ext deq feq⟩

Equivalence of Equality for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any two partially defined linear maps $f, g \colon E \to_{.[R]} F$, the following are equivalent: 1. The maps $f$ and $g$ are equal. 2. The domains of $f$ and $g$ are equal, and for every $x \in E$ in their common domain, the images $f(x)$ and $g(x)$ coincide. In other words, $f = g$ if and only if $\text{domain}(f) = \text{domain}(g)$ and for all $x \in \text{domain}(f)$, $f(x) = g(x)$.

LinearPMap.dExt_iff theorem

 {f g : E →ₗ.[R] F} :
  f = g ↔ ∃ _domain_eq : f.domain = g.domain, ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y

Full source

theorem dExt_iff {f g : E →ₗ.[R] F} :
    f = g ↔
      ∃ _domain_eq : f.domain = g.domain,
        ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y :=
  ⟨fun EQ =>
    EQ ▸
      ⟨rfl, fun x y h => by
        congr
        exact mod_cast h⟩,
    fun ⟨deq, feq⟩ => dExt deq feq⟩

Equivalence of Equality for Partially Defined Linear Maps via Domain and Pointwise Equality

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any two partially defined linear maps $f, g \colon E \to_{.[R]} F$, the following are equivalent: 1. The maps $f$ and $g$ are equal. 2. There exists a proof that their domains are equal, and for every $x$ in the domain of $f$ and $y$ in the domain of $g$ such that $x = y$ as elements of $E$, we have $f(x) = g(y)$. In other words, $f = g$ if and only if $\text{domain}(f) = \text{domain}(g)$ and for all $x \in \text{domain}(f)$ and $y \in \text{domain}(g)$ with $x = y$ in $E$, the images $f(x)$ and $g(y)$ coincide.

LinearPMap.ext' theorem

{s : Submodule R E} {f g : s →ₗ[R] F} (h : f = g) : mk s f = mk s g

Full source

theorem ext' {s : Submodule R E} {f g : s →ₗ[R] F} (h : f = g) : mk s f = mk s g :=
  h ▸ rfl

Equality of Partially Defined Linear Maps from Equal Linear Maps

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $s$ be a submodule of $E$. For any two linear maps $f, g : s \to F$, if $f = g$ as functions, then the partially defined linear maps constructed from $f$ and $g$ with domain $s$ are equal.

LinearPMap.map_add theorem

(f : E →ₗ.[R] F) (x y : f.domain) : f (x + y) = f x + f y

Full source

theorem map_add (f : E →ₗ.[R] F) (x y : f.domain) : f (x + y) = f x + f y :=
  f.toFun.map_add x y

Additivity of Partially Defined Linear Maps

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ and any elements $x, y$ in the domain of $f$, we have $f(x + y) = f(x) + f(y)$.

LinearPMap.map_neg theorem

(f : E →ₗ.[R] F) (x : f.domain) : f (-x) = -f x

Full source

theorem map_neg (f : E →ₗ.[R] F) (x : f.domain) : f (-x) = -f x :=
  f.toFun.map_neg x

Negation Preservation for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$ with additive commutative group structures. For any partially defined linear map $f \colon E \to_{.[R]} F$ and any element $x$ in the domain of $f$, we have $f(-x) = -f(x)$.

LinearPMap.map_sub theorem

(f : E →ₗ.[R] F) (x y : f.domain) : f (x - y) = f x - f y

Full source

theorem map_sub (f : E →ₗ.[R] F) (x y : f.domain) : f (x - y) = f x - f y :=
  f.toFun.map_sub x y

Subtraction Preservation for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, $E$ and $F$ be modules over $R$, and let $f \colon E \to_{.[R]} F$ be a partially defined linear map. For any elements $x, y$ in the domain of $f$, we have $f(x - y) = f(x) - f(y)$.

LinearPMap.map_smul theorem

(f : E →ₗ.[R] F) (c : R) (x : f.domain) : f (c • x) = c • f x

Full source

theorem map_smul (f : E →ₗ.[R] F) (c : R) (x : f.domain) : f (c • x) = c • f x :=
  f.toFun.map_smul c x

Scalar Multiplication Preservation for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, $E$ and $F$ be modules over $R$, and let $f \colon E \to_{.[R]} F$ be a partially defined linear map. For any scalar $c \in R$ and any element $x$ in the domain of $f$, we have $f(c \cdot x) = c \cdot f(x)$.

LinearPMap.mk_apply theorem

(p : Submodule R E) (f : p →ₗ[R] F) (x : p) : mk p f x = f x

Full source

@[simp]
theorem mk_apply (p : Submodule R E) (f : p →ₗ[R] F) (x : p) : mk p f x = f x :=
  rfl

Evaluation of Constructed Partial Linear Map

Informal description

Let $R$ be a ring, $E$ and $F$ be modules over $R$, $p$ be a submodule of $E$, and $f \colon p \to F$ be a linear map. For any $x \in p$, the evaluation of the constructed partial linear map $\text{mk}\, p\, f$ at $x$ equals $f(x)$, i.e., $(\text{mk}\, p\, f)(x) = f(x)$.

LinearPMap.mkSpanSingleton' definition

(x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) : E →ₗ.[R] F

Full source

/-- 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`. -/
noncomputable def mkSpanSingleton' (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) :
    E →ₗ.[R] F where
  domain := R ∙ x
  toFun :=
    have H : ∀ c₁ c₂ : R, c₁ • x = c₂ • x → c₁ • y = c₂ • y := by
      intro c₁ c₂ h
      rw [← sub_eq_zero, ← sub_smul] at h ⊢
      exact H _ h
    { toFun z := Classical.choose (mem_span_singleton.1 z.prop) • y
      map_add' y z := by
        rw [← add_smul, H]
        have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
        simp only [add_smul, sub_smul, this, ← coe_add]
      map_smul' c z := by
        rw [smul_smul, H]
        have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
        simp only [mul_smul, this]
        apply coe_smul }

Partially defined linear map on the span of a singleton

Informal description

Given a ring $R$ and modules $E$, $F$ over $R$, for any elements $x \in E$ and $y \in F$ satisfying the condition that for all $c \in R$, $c \cdot x = 0$ implies $c \cdot y = 0$, there exists a unique partially defined linear map from $E$ to $F$ defined on the span $R \cdot x$ that sends $x$ to $y$. More precisely, this map is defined on the submodule generated by $x$ (i.e., all scalar multiples of $x$), and for any $c \in R$, it maps $c \cdot x$ to $c \cdot y$.

LinearPMap.domain_mkSpanSingleton theorem

(x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) : (mkSpanSingleton' x y H).domain = R ∙ x

Full source

@[simp]
theorem domain_mkSpanSingleton (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) :
    (mkSpanSingleton' x y H).domain = R ∙ x :=
  rfl

Domain of Partial Linear Map on Span of Singleton is Span of Singleton

Informal description

For any ring $R$ and $R$-modules $E$ and $F$, given elements $x \in E$ and $y \in F$ such that for all $c \in R$, $c \cdot x = 0$ implies $c \cdot y = 0$, the domain of the partial linear map $\text{mkSpanSingleton'}\,x\,y\,H$ is equal to the span of $\{x\}$, i.e., $(\text{mkSpanSingleton'}\,x\,y\,H).\text{domain} = R \cdot x$.

LinearPMap.mkSpanSingleton'_apply theorem

 (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (c : R) (h) : mkSpanSingleton' x y H ⟨c • x, h⟩ = c • y

Full source

@[simp]
theorem mkSpanSingleton'_apply (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (c : R) (h) :
    mkSpanSingleton' x y H ⟨c • x, h⟩ = c • y := by
  dsimp [mkSpanSingleton']
  rw [← sub_eq_zero, ← sub_smul]
  apply H
  simp only [sub_smul, one_smul, sub_eq_zero]
  apply Classical.choose_spec (mem_span_singleton.1 h)

Action of Partial Linear Map on Span of Singleton: $\text{mkSpanSingleton'}\,x\,y\,H\,(c \cdot x) = c \cdot y$

Informal description

Let $R$ be a ring and $E$, $F$ be $R$-modules. Given elements $x \in E$ and $y \in F$ such that for all $c \in R$, $c \cdot x = 0$ implies $c \cdot y = 0$, the partially defined linear map $\text{mkSpanSingleton'}\,x\,y\,H$ satisfies $\text{mkSpanSingleton'}\,x\,y\,H\,(c \cdot x) = c \cdot y$ for any $c \in R$ and any proof $h$ that $c \cdot x$ belongs to the domain of the map.

LinearPMap.mkSpanSingleton'_apply_self theorem

(x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (h) : mkSpanSingleton' x y H ⟨x, h⟩ = y

Full source

@[simp]
theorem mkSpanSingleton'_apply_self (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (h) :
    mkSpanSingleton' x y H ⟨x, h⟩ = y := by
  conv_rhs => rw [← one_smul R y]
  rw [← mkSpanSingleton'_apply x y H 1 ?_]
  · congr
    rw [one_smul]
  · rwa [one_smul]

Partial Linear Map on Span of Singleton Evaluates to Given Value: $\text{mkSpanSingleton'}\,x\,y\,H\,(x) = y$

Informal description

Let $R$ be a ring and $E$, $F$ be $R$-modules. Given elements $x \in E$ and $y \in F$ such that for all $c \in R$, $c \cdot x = 0$ implies $c \cdot y = 0$, the partially defined linear map $\text{mkSpanSingleton'}\,x\,y\,H$ satisfies $\text{mkSpanSingleton'}\,x\,y\,H\,(x) = y$ for any proof $h$ that $x$ belongs to the domain of the map.

LinearPMap.mkSpanSingleton abbrev

 {K E F : Type*} [DivisionRing K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] (x : E) (y : F)
  (hx : x ≠ 0) : E →ₗ.[K] F

Full source

/-- The unique `LinearPMap` on `span R {x}` that sends a non-zero vector `x` to `y`.
This version works for modules over division rings. -/
noncomputable abbrev mkSpanSingleton {K E F : Type*} [DivisionRing K] [AddCommGroup E] [Module K E]
    [AddCommGroup F] [Module K F] (x : E) (y : F) (hx : x ≠ 0) : E →ₗ.[K] F :=
  mkSpanSingleton' x y fun c hc =>
    (smul_eq_zero.1 hc).elim (fun hc => by rw [hc, zero_smul]) fun hx' => absurd hx' hx

Partially defined linear map on span of a nonzero singleton

Informal description

Given a division ring $K$ and $K$-modules $E$ and $F$, for any nonzero element $x \in E$ and any element $y \in F$, there exists a unique partially defined linear map from $E$ to $F$ defined on the span of $\{x\}$ that sends $x$ to $y$. More precisely, this map is defined on the submodule $K \cdot x$ (all scalar multiples of $x$), and for any $c \in K$, it maps $c \cdot x$ to $c \cdot y$.

LinearPMap.mkSpanSingleton_apply theorem

 (K : Type*) {E F : Type*} [DivisionRing K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] {x : E}
  (hx : x ≠ 0) (y : F) :
  mkSpanSingleton x y hx ⟨x, (Submodule.mem_span_singleton_self x : x ∈ Submodule.span K { x })⟩ = y

Full source

theorem mkSpanSingleton_apply (K : Type*) {E F : Type*} [DivisionRing K] [AddCommGroup E]
    [Module K E] [AddCommGroup F] [Module K F] {x : E} (hx : x ≠ 0) (y : F) :
    mkSpanSingleton x y hx ⟨x, (Submodule.mem_span_singleton_self x : x ∈ Submodule.span K {x})⟩ =
      y :=
  LinearPMap.mkSpanSingleton'_apply_self _ _ _ _

Evaluation of Partial Linear Map on Span of Singleton: $\operatorname{mkSpanSingleton}\,x\,y\,h_x(x) = y$

Informal description

Let $K$ be a division ring and $E$, $F$ be $K$-modules. For any nonzero element $x \in E$ and any element $y \in F$, the partially defined linear map $\operatorname{mkSpanSingleton}\,x\,y\,h_x$ evaluated at $x$ (which is in its domain by $\operatorname{Submodule.mem\_span\_singleton\_self}$) equals $y$.

LinearPMap.fst definition

(p : Submodule R E) (p' : Submodule R F) : E × F →ₗ.[R] E

Full source

/-- Projection to the first coordinate as a `LinearPMap` -/
protected def fst (p : Submodule R E) (p' : Submodule R F) : E × FE × F →ₗ.[R] E where
  domain := p.prod p'
  toFun := (LinearMap.fst R E F).comp (p.prod p').subtype

First projection as a partially defined linear map

Informal description

Given submodules $p$ of $E$ and $p'$ of $F$ over a ring $R$, the partially defined linear map `LinearPMap.fst` projects the first component of elements in the product submodule $p \times p' \subseteq E \times F$ back to $E$. Specifically, for any $(x,y) \in p \times p'$, the map returns $x$.

LinearPMap.fst_apply theorem

(p : Submodule R E) (p' : Submodule R F) (x : p.prod p') : LinearPMap.fst p p' x = (x : E × F).1

Full source

@[simp]
theorem fst_apply (p : Submodule R E) (p' : Submodule R F) (x : p.prod p') :
    LinearPMap.fst p p' x = (x : E × F).1 :=
  rfl

First Projection of Partially Defined Linear Map on Product Submodule

Informal description

Let $R$ be a ring, and let $E$ and $F$ be $R$-modules. For any submodules $p \subseteq E$ and $p' \subseteq F$, and any element $x \in p \times p'$, the first projection of the partially defined linear map $\operatorname{fst}_{p,p'}$ applied to $x$ equals the first component of $x$ viewed as an element of $E \times F$, i.e., $\operatorname{fst}_{p,p'}(x) = x_1$.

LinearPMap.snd definition

(p : Submodule R E) (p' : Submodule R F) : E × F →ₗ.[R] F

Full source

/-- Projection to the second coordinate as a `LinearPMap` -/
protected def snd (p : Submodule R E) (p' : Submodule R F) : E × FE × F →ₗ.[R] F where
  domain := p.prod p'
  toFun := (LinearMap.snd R E F).comp (p.prod p').subtype

Second projection as a partially defined linear map

Informal description

For submodules $p$ of $E$ and $p'$ of $F$ over a ring $R$, the partially defined linear map $\operatorname{snd}_{p,p'}$ from $E \times F$ to $F$ is defined on the product submodule $p \times p'$ and acts as the projection to the second coordinate. Specifically, it maps $(x,y) \in p \times p'$ to $y \in F$.

LinearPMap.snd_apply theorem

(p : Submodule R E) (p' : Submodule R F) (x : p.prod p') : LinearPMap.snd p p' x = (x : E × F).2

Full source

@[simp]
theorem snd_apply (p : Submodule R E) (p' : Submodule R F) (x : p.prod p') :
    LinearPMap.snd p p' x = (x : E × F).2 :=
  rfl

Second Projection of Partially Defined Linear Map on Product Submodule

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any submodules $p \subseteq E$ and $p' \subseteq F$, and any element $x \in p \times p'$, the second projection map $\operatorname{snd}_{p,p'} : E \times F \to_{.[R]} F$ satisfies $\operatorname{snd}_{p,p'}(x) = x_2$, where $x_2$ is the second component of $x$ viewed as an element of $E \times F$.

LinearPMap.le instance

: LE (E →ₗ.[R] F)

Full source

instance le : LE (E →ₗ.[R] F) :=
  ⟨fun f g => f.domain ≤ g.domain ∧ ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y⟩

Partial Order on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, the type of partially defined linear maps $E \to_{.[R]} F$ is equipped with a partial order structure.

LinearPMap.apply_comp_inclusion theorem

{T S : E →ₗ.[R] F} (h : T ≤ S) (x : T.domain) : T x = S (Submodule.inclusion h.1 x)

Full source

theorem apply_comp_inclusion {T S : E →ₗ.[R] F} (h : T ≤ S) (x : T.domain) :
    T x = S (Submodule.inclusion h.1 x) :=
  h.2 rfl

Compatibility of Partially Defined Linear Maps under Inclusion

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any two partially defined linear maps $T, S : E \to_{.[R]} F$ such that $T \leq S$ (i.e., the domain of $T$ is contained in the domain of $S$ and they agree on their common domain), and for any $x$ in the domain of $T$, we have $T(x) = S(\iota(x))$, where $\iota$ is the inclusion map from the domain of $T$ to the domain of $S$.

LinearPMap.exists_of_le theorem

{T S : E →ₗ.[R] F} (h : T ≤ S) (x : T.domain) : ∃ y : S.domain, (x : E) = y ∧ T x = S y

Full source

theorem exists_of_le {T S : E →ₗ.[R] F} (h : T ≤ S) (x : T.domain) :
    ∃ y : S.domain, (x : E) = y ∧ T x = S y :=
  ⟨⟨x.1, h.1 x.2⟩, ⟨rfl, h.2 rfl⟩⟩

Existence of Extension for Partially Defined Linear Maps Under Restriction

Informal description

Let $R$ be a ring and $E$, $F$ be modules over $R$. For any two partially defined linear maps $T, S : E \to_{.[R]} F$ such that $T \leq S$ (i.e., $T$ is a restriction of $S$), and for any $x$ in the domain of $T$, there exists an element $y$ in the domain of $S$ such that $x = y$ (as elements of $E$) and $T(x) = S(y)$.

LinearPMap.eqLocus definition

(f g : E →ₗ.[R] F) : Submodule R E

Full source

/-- 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. -/
def eqLocus (f g : E →ₗ.[R] F) : Submodule R E where
  carrier := { x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), f ⟨x, hf⟩ = g ⟨x, hg⟩ }
  zero_mem' := ⟨zero_mem _, zero_mem _, f.map_zero.trans g.map_zero.symm⟩
  add_mem' {x y} := fun ⟨hfx, hgx, hx⟩ ⟨hfy, hgy, hy⟩ ↦
    ⟨add_mem hfx hfy, add_mem hgx hgy, by
      simp_all [← AddMemClass.mk_add_mk, f.map_add, g.map_add]⟩
  smul_mem' c x := fun ⟨hfx, hgx, hx⟩ ↦
    ⟨smul_mem _ c hfx, smul_mem _ c hgx, by
      have {f : E →ₗ.[R] F} (hfx) : (⟨c • x, smul_mem _ c hfx⟩ : f.domain) = c • ⟨x, hfx⟩ := by simp
      rw [this hfx, this hgx, f.map_smul, g.map_smul, hx]⟩

Equal locus of two partially defined linear maps

Informal description

For two partially defined linear maps $ f, g : E \to_{.[R]} F $, the set of points $ x \in E $ such that both $ f $ and $ g $ are defined at $ x $ and $ f(x) = g(x) $ forms a submodule of $ E $. This submodule is called the *equal locus* of $ f $ and $ g $.

LinearPMap.bot instance

: Bot (E →ₗ.[R] F)

Full source

instance bot : Bot (E →ₗ.[R] F) :=
  ⟨⟨⊥, 0⟩⟩

Bottom Element in Partially Defined Linear Maps

Informal description

The type of partially defined linear maps $E \to_{.[R]} F$ has a bottom element $\bot$ with respect to the partial order defined by domain inclusion and agreement on common domains.

LinearPMap.inhabited instance

: Inhabited (E →ₗ.[R] F)

Full source

instance inhabited : Inhabited (E →ₗ.[R] F) :=
  ⟨⊥⟩

Inhabitedness of Partially Defined Linear Maps

Informal description

The type of partially defined linear maps $E \to_{.[R]} F$ is inhabited, meaning there exists at least one such map.

LinearPMap.semilatticeInf instance

: SemilatticeInf (E →ₗ.[R] F)

Full source

instance semilatticeInf : SemilatticeInf (E →ₗ.[R] F) where
  le := (· ≤ ·)
  le_refl f := ⟨le_refl f.domain, fun _ _ h => Subtype.eq h ▸ rfl⟩
  le_trans := fun _ _ _ ⟨fg_le, fg_eq⟩ ⟨gh_le, gh_eq⟩ =>
    ⟨le_trans fg_le gh_le, fun x _ hxz =>
      have hxy : (x : E) = inclusion fg_le x := rfl
      (fg_eq hxy).trans (gh_eq <| hxy.symm.trans hxz)⟩
  le_antisymm _ _ fg gf := eq_of_le_of_domain_eq fg (le_antisymm fg.1 gf.1)
  inf f g := ⟨f.eqLocus g, f.toFun.comp <| inclusion fun _x hx => hx.fst⟩
  le_inf := by
    intro f g h ⟨fg_le, fg_eq⟩ ⟨fh_le, fh_eq⟩
    exact ⟨fun x hx =>
      ⟨fg_le hx, fh_le hx,
      (fg_eq (x := ⟨x, hx⟩) rfl).symm.trans (fh_eq rfl)⟩,
      fun x ⟨y, yg, hy⟩ h => fg_eq h⟩
  inf_le_left f _ := ⟨fun _ hx => hx.fst, fun _ _ h => congr_arg f <| Subtype.eq <| h⟩
  inf_le_right _ g :=
    ⟨fun _ hx => hx.snd.fst, fun ⟨_, _, _, hx⟩ _ h => hx.trans <| congr_arg g <| Subtype.eq <| h⟩

Meet-Semilattice Structure on Partially Defined Linear Maps

Informal description

The set of partially defined linear maps $E \to_{.[R]} F$ forms a meet-semilattice, where the meet operation is defined by the greatest lower bound with respect to the partial order of domain inclusion and agreement on common domains.

LinearPMap.orderBot instance

: OrderBot (E →ₗ.[R] F)

Full source

instance orderBot : OrderBot (E →ₗ.[R] F) where
  bot := ⊥
  bot_le f :=
    ⟨bot_le, fun x y h => by
      have hx : x = 0 := Subtype.eq ((mem_bot R).1 x.2)
      have hy : y = 0 := Subtype.eq (h.symm.trans (congr_arg _ hx))
      rw [hx, hy, map_zero, map_zero]⟩

Partially Defined Linear Maps Form an Order with Bottom Element

Informal description

The type of partially defined linear maps $E \to_{.[R]} F$ forms an order with a bottom element, where the partial order is given by domain inclusion and agreement on common domains, and the bottom element is the zero map defined on the trivial submodule.

LinearPMap.le_of_eqLocus_ge theorem

{f g : E →ₗ.[R] F} (H : f.domain ≤ f.eqLocus g) : f ≤ g

Full source

theorem le_of_eqLocus_ge {f g : E →ₗ.[R] F} (H : f.domain ≤ f.eqLocus g) : f ≤ g :=
  suffices f ≤ f ⊓ g from le_trans this inf_le_right
  ⟨H, fun _x _y hxy => ((inf_le_left : f ⊓ g ≤ f).2 hxy.symm).symm⟩

Partial Order Condition via Equal Locus for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be $R$-modules. For any two partially defined linear maps $f, g : E \to_{.[R]} F$, if the domain of $f$ is contained in the equal locus of $f$ and $g$ (i.e., the submodule where both maps are defined and agree), then $f$ is less than or equal to $g$ in the partial order of partially defined linear maps.

LinearPMap.domain_mono theorem

: StrictMono (@domain R _ E _ _ F _ _)

Full source

theorem domain_mono : StrictMono (@domain R _ E _ _ F _ _) := fun _f _g hlt =>
  lt_of_le_of_ne hlt.1.1 fun heq => ne_of_lt hlt <| eq_of_le_of_domain_eq (le_of_lt hlt) heq

Strict Monotonicity of Domain Assignment for Partially Defined Linear Maps

Informal description

The function that assigns to each partially defined linear map $f : E \to_{.[R]} F$ its domain submodule is strictly monotone. That is, for any two such maps $f$ and $g$, if $f < g$ in the partial order of domain inclusion and agreement on common domains, then the domain of $f$ is strictly contained in the domain of $g$.

LinearPMap.sup definition

(f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : E →ₗ.[R] F

Full source

/-- 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`. -/
protected noncomputable def sup (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : E →ₗ.[R] F :=
  ⟨_, Classical.choose (sup_aux f g h)⟩

Supremum of Partially Defined Linear Maps

Informal description

Given two partially defined linear maps $ f, g : E \to_{.[R]} F $ that agree on the intersection of their domains (i.e., for any $ x \in \text{domain}(f) $ and $ y \in \text{domain}(g) $ such that $ x = y $, we have $ f(x) = g(y) $), the function $ f \sqcup g $ is the unique partially defined linear map on the supremum of their domains $ \text{domain}(f) \sqcup \text{domain}(g) $ that extends both $ f $ and $ g $.

LinearPMap.domain_sup theorem

 (f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) :
  (f.sup g h).domain = f.domain ⊔ g.domain

Full source

@[simp]
theorem domain_sup (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) :
    (f.sup g h).domain = f.domain ⊔ g.domain :=
  rfl

Domain of Supremum of Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be $R$-modules. Given two partially defined linear maps $f, g : E \to_{.[R]} F$ that agree on the intersection of their domains (i.e., for any $x \in \text{domain}(f)$ and $y \in \text{domain}(g)$ with $x = y$ in $E$, we have $f(x) = g(y)$), the domain of the supremum $f \sqcup g$ is the supremum of their domains, i.e., $\text{domain}(f \sqcup g) = \text{domain}(f) \sqcup \text{domain}(g)$.

LinearPMap.sup_apply theorem

 {f g : E →ₗ.[R] F} (H : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) (x : f.domain) (y : g.domain)
  (z : ↥(f.domain ⊔ g.domain)) (hz : (↑x : E) + ↑y = ↑z) : f.sup g H z = f x + g y

Full source

theorem sup_apply {f g : E →ₗ.[R] F} (H : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y)
    (x : f.domain) (y : g.domain) (z : ↥(f.domain ⊔ g.domain)) (hz : (↑x : E) + ↑y = ↑z) :
    f.sup g H z = f x + g y :=
  Classical.choose_spec (sup_aux f g H) x y z hz

Evaluation of Supremum of Partially Defined Linear Maps

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f, g: E \to_{.[R]} F$ be partially defined linear maps. Suppose $f$ and $g$ agree on the intersection of their domains (i.e., for any $x \in \text{dom}(f)$ and $y \in \text{dom}(g)$ with $x = y$ in $E$, we have $f(x) = g(y)$). Then for any $x \in \text{dom}(f)$, $y \in \text{dom}(g)$, and $z \in \text{dom}(f) \sqcup \text{dom}(g)$ satisfying $x + y = z$ in $E$, the value of the supremum map $f \sqcup g$ at $z$ equals $f(x) + g(y)$.

LinearPMap.left_le_sup theorem

(f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : f ≤ f.sup g h

Full source

protected theorem left_le_sup (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : f ≤ f.sup g h := by
  refine ⟨le_sup_left, fun z₁ z₂ hz => ?_⟩
  rw [← add_zero (f _), ← g.map_zero]
  refine (sup_apply h _ _ _ ?_).symm
  simpa

Left Partially Defined Linear Map is Less Than or Equal to Supremum

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f, g: E \to_{.[R]} F$ be partially defined linear maps. If $f$ and $g$ agree on the intersection of their domains (i.e., for any $x \in \text{dom}(f)$ and $y \in \text{dom}(g)$ with $x = y$ in $E$, we have $f(x) = g(y)$), then $f$ is less than or equal to the supremum $f \sqcup g$ in the partial order of partially defined linear maps.

LinearPMap.right_le_sup theorem

(f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : g ≤ f.sup g h

Full source

protected theorem right_le_sup (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : g ≤ f.sup g h := by
  refine ⟨le_sup_right, fun z₁ z₂ hz => ?_⟩
  rw [← zero_add (g _), ← f.map_zero]
  refine (sup_apply h _ _ _ ?_).symm
  simpa

Right Partial Linear Map is Less Than or Equal to Supremum

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f, g: E \to_{.[R]} F$ be partially defined linear maps that agree on the intersection of their domains (i.e., for any $x \in \text{dom}(f)$ and $y \in \text{dom}(g)$ with $x = y$ in $E$, we have $f(x) = g(y)$). Then $g$ is less than or equal to the supremum $f \sqcup g$ in the partial order of partially defined linear maps.

LinearPMap.sup_le theorem

 {f g h : E →ₗ.[R] F} (H : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) (fh : f ≤ h) (gh : g ≤ h) :
  f.sup g H ≤ h

Full source

protected theorem sup_le {f g h : E →ₗ.[R] F}
    (H : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) (fh : f ≤ h) (gh : g ≤ h) :
    f.sup g H ≤ h :=
  have Hf : f ≤ f.sup g H ⊓ h := le_inf (f.left_le_sup g H) fh
  have Hg : g ≤ f.sup g H ⊓ h := le_inf (f.right_le_sup g H) gh
  le_of_eqLocus_ge <| sup_le Hf.1 Hg.1

Supremum of Partially Defined Linear Maps is Least Upper Bound

Informal description

Let $R$ be a ring, and let $E$ and $F$ be $R$-modules. For any three partially defined linear maps $f, g, h \colon E \to_{.[R]} F$, if $f$ and $g$ agree on the intersection of their domains (i.e., for all $x \in \text{dom}(f)$ and $y \in \text{dom}(g)$ with $x = y$ in $E$, we have $f(x) = g(y)$), and if $f \leq h$ and $g \leq h$, then the supremum $f \sqcup g$ is also less than or equal to $h$.

LinearPMap.sup_h_of_disjoint theorem

(f g : E →ₗ.[R] F) (h : Disjoint f.domain g.domain) (x : f.domain) (y : g.domain) (hxy : (x : E) = y) : f x = g y

Full source

/-- Hypothesis for `LinearPMap.sup` holds, if `f.domain` is disjoint with `g.domain`. -/
theorem sup_h_of_disjoint (f g : E →ₗ.[R] F) (h : Disjoint f.domain g.domain) (x : f.domain)
    (y : g.domain) (hxy : (x : E) = y) : f x = g y := by
  rw [disjoint_def] at h
  have hy : y = 0 := Subtype.eq (h y (hxy ▸ x.2) y.2)
  have hx : x = 0 := Subtype.eq (hxy.trans <| congr_arg _ hy)
  simp [*]

Agreement of Disjointly Defined Partial Linear Maps on Intersection

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f \colon E \to_{.[R]} F$ and $g \colon E \to_{.[R]} F$ be partially defined linear maps with disjoint domains. For any $x$ in the domain of $f$ and $y$ in the domain of $g$ such that $x = y$ as elements of $E$, we have $f(x) = g(y)$.

LinearPMap.instZero instance

: Zero (E →ₗ.[R] F)

Full source

instance instZero : Zero (E →ₗ.[R] F) := ⟨⊤, 0⟩

Zero Partially Defined Linear Map

Informal description

For any ring $R$ and modules $E$, $F$ over $R$ with additive commutative group structures, the type of partially defined linear maps $E \toₗ.[R] F$ has a zero element. This zero map is defined on the entire module $E$ and maps every element to the zero element of $F$.

LinearPMap.zero_domain theorem

: (0 : E →ₗ.[R] F).domain = ⊤

Full source

@[simp]
theorem zero_domain : (0 : E →ₗ.[R] F).domain = ⊤ := rfl

Domain of Zero Partially Defined Linear Map is Entire Module

Informal description

For the zero partially defined linear map $0 \colon E \toₗ.[R] F$, its domain is equal to the entire module $E$ (denoted by $\top$ in the submodule lattice).

LinearPMap.zero_apply theorem

(x : (⊤ : Submodule R E)) : (0 : E →ₗ.[R] F) x = 0

Full source

@[simp]
theorem zero_apply (x : (⊤ : Submodule R E)) : (0 : E →ₗ.[R] F) x = 0 := rfl

Zero Partially Defined Linear Map Evaluates to Zero

Informal description

For any element $x$ in the entire module $E$ (viewed as a submodule $\top$), the zero partially defined linear map $0 \colon E \to_{.[R]} F$ evaluates to the zero element of $F$, i.e., $0(x) = 0$.

LinearPMap.instSMul instance

: SMul M (E →ₗ.[R] F)

Full source

instance instSMul : SMul M (E →ₗ.[R] F) :=
  ⟨fun a f =>
    { domain := f.domain
      toFun := a • f.toFun }⟩

Scalar Multiplication on Partially Defined Linear Maps

Informal description

For any monoid $M$ and partially defined linear maps $E \to_{.[R]} F$ between modules $E$ and $F$ over a ring $R$, there is a scalar multiplication operation that defines an action of $M$ on the space of partially defined linear maps. This operation preserves the domain of the linear maps and acts pointwise on their values.

LinearPMap.smul_domain theorem

(a : M) (f : E →ₗ.[R] F) : (a • f).domain = f.domain

Full source

@[simp]
theorem smul_domain (a : M) (f : E →ₗ.[R] F) : (a • f).domain = f.domain :=
  rfl

Domain Preservation under Scalar Multiplication of Partial Linear Maps

Informal description

For any scalar $a$ in a monoid $M$ and any partially defined linear map $f \colon E \to_{.[R]} F$ between modules $E$ and $F$ over a ring $R$, the domain of the scalar multiple $a \cdot f$ is equal to the domain of $f$.

LinearPMap.smul_apply theorem

(a : M) (f : E →ₗ.[R] F) (x : (a • f).domain) : (a • f) x = a • f x

Full source

theorem smul_apply (a : M) (f : E →ₗ.[R] F) (x : (a • f).domain) : (a • f) x = a • f x :=
  rfl

Scalar Multiplication Acts Pointwise on Partially Defined Linear Maps

Informal description

For any scalar $a$ in a monoid $M$, any partially defined linear map $f \colon E \to_{.[R]} F$ between modules $E$ and $F$ over a ring $R$, and any element $x$ in the domain of $a \cdot f$, we have $(a \cdot f)(x) = a \cdot f(x)$.

LinearPMap.coe_smul theorem

(a : M) (f : E →ₗ.[R] F) : ⇑(a • f) = a • ⇑f

Full source

@[simp]
theorem coe_smul (a : M) (f : E →ₗ.[R] F) : ⇑(a • f) = a • ⇑f :=
  rfl

Pointwise scalar multiplication of partially defined linear maps: $(a \cdot f)(x) = a \cdot f(x)$

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$ with additive commutative group structures. For any monoid $M$ acting on $F$, any element $a \in M$, and any partially defined linear map $f: E \to_{.[R]} F$, the underlying function of the scalar multiple $a \cdot f$ is equal to the pointwise scalar multiple of $f$, i.e., $(a \cdot f)(x) = a \cdot f(x)$ for all $x$ in the domain of $f$.

LinearPMap.instSMulCommClass instance

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

Full source

instance instSMulCommClass [SMulCommClass M N F] : SMulCommClass M N (E →ₗ.[R] F) :=
  ⟨fun a b f => ext' <| smul_comm a b f.toFun⟩

Commutativity of Scalar Actions on Partially Defined Linear Maps

Informal description

For any monoid $M$ and $N$, and modules $E$ and $F$ over a ring $R$, if the scalar multiplication actions of $M$ and $N$ on $F$ commute (i.e., $a \cdot (b \cdot x) = b \cdot (a \cdot x)$ for all $a \in M$, $b \in N$, $x \in F$), then the induced scalar multiplication actions on the space of partially defined linear maps $E \to_{.[R]} F$ also commute.

LinearPMap.instIsScalarTower instance

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

Full source

instance instIsScalarTower [SMul M N] [IsScalarTower M N F] : IsScalarTower M N (E →ₗ.[R] F) :=
  ⟨fun a b f => ext' <| smul_assoc a b f.toFun⟩

Scalar Tower Structure on Partially Defined Linear Maps

Informal description

For any monoid $M$ and ring $R$, and modules $E$, $F$ over $R$, if $F$ has a scalar tower structure for the actions of $M$ and $N$ (i.e., $(a \cdot b) \cdot x = a \cdot (b \cdot x)$ for all $a \in M$, $b \in N$, $x \in F$), then the space of partially defined linear maps $E \to_{.[R]} F$ also inherits this scalar tower structure. This means that for any $a \in M$, $b \in N$, and $f \in E \to_{.[R]} F$, we have $(a \cdot b) \cdot f = a \cdot (b \cdot f)$.

LinearPMap.instMulAction instance

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

Full source

instance instMulAction : MulAction M (E →ₗ.[R] F) where
  smul := (· • ·)
  one_smul := fun ⟨_s, f⟩ => ext' <| one_smul M f
  mul_smul a b f := ext' <| mul_smul a b f.toFun

Multiplicative Action on Partially Defined Linear Maps

Informal description

For any monoid $M$ and partially defined linear maps $E \to_{.[R]} F$ between modules $E$ and $F$ over a ring $R$, the space of partially defined linear maps forms a multiplicative action of $M$. This means that for any $m \in M$ and any partially defined linear map $f$, the scalar multiplication $m \cdot f$ is defined pointwise on the domain of $f$.

LinearPMap.instNeg instance

: Neg (E →ₗ.[R] F)

Full source

instance instNeg : Neg (E →ₗ.[R] F) :=
  ⟨fun f => ⟨f.domain, -f.toFun⟩⟩

Negation of Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, the set of partially defined linear maps from $E$ to $F$ has a negation operation. Specifically, for any partially defined linear map $f : E \toₗ.[R] F$, the negation $-f$ is defined pointwise as $(-f)(x) = -f(x)$ for all $x$ in the domain of $f$.

LinearPMap.neg_domain theorem

(f : E →ₗ.[R] F) : (-f).domain = f.domain

Full source

@[simp]
theorem neg_domain (f : E →ₗ.[R] F) : (-f).domain = f.domain := rfl

Domain Invariance under Negation of Partially Defined Linear Maps

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ over a ring $R$, the domain of the negation $-f$ is equal to the domain of $f$, i.e., $(-f).\text{domain} = f.\text{domain}$.

LinearPMap.neg_apply theorem

(f : E →ₗ.[R] F) (x) : (-f) x = -f x

Full source

@[simp]
theorem neg_apply (f : E →ₗ.[R] F) (x) : (-f) x = -f x :=
  rfl

Negation of Partially Defined Linear Maps Preserves Evaluation

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ and any element $x$ in its domain, the evaluation of the negation $-f$ at $x$ equals the negation of the evaluation of $f$ at $x$, i.e., $(-f)(x) = -f(x)$.

LinearPMap.instInvolutiveNeg instance

: InvolutiveNeg (E →ₗ.[R] F)

Full source

instance instInvolutiveNeg : InvolutiveNeg (E →ₗ.[R] F) :=
  ⟨fun f => by
    ext x y hxy
    · rfl
    · simp only [neg_apply, neg_neg]⟩

Involutive Negation for Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, the set of partially defined linear maps $E \toₗ.[R] F$ is equipped with an involutive negation operation. That is, for any such map $f$, the negation $-f$ satisfies $-(-f) = f$.

LinearPMap.instAdd instance

: Add (E →ₗ.[R] F)

Full source

instance instAdd : Add (E →ₗ.[R] F) :=
  ⟨fun f g =>
    { domain := f.domain ⊓ g.domain
      toFun := f.toFun.comp (inclusion (inf_le_left : f.domain ⊓ g.domain ≤ _))
        + g.toFun.comp (inclusion (inf_le_right : f.domain ⊓ g.domain ≤ _)) }⟩

Addition of Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$ and $F$ over $R$ with additive commutative group structures, the set of partially defined linear maps from $E$ to $F$ has an addition operation defined pointwise on the intersection of their domains.

LinearPMap.add_domain theorem

(f g : E →ₗ.[R] F) : (f + g).domain = f.domain ⊓ g.domain

Full source

theorem add_domain (f g : E →ₗ.[R] F) : (f + g).domain = f.domain ⊓ g.domain := rfl

Domain of Sum of Partially Defined Linear Maps is Intersection of Domains

Informal description

For any two partially defined linear maps $f, g \colon E \toₗ.[R] F$, the domain of their sum $f + g$ is equal to the intersection of their domains, i.e., $(f + g).\text{domain} = f.\text{domain} \cap g.\text{domain}$.

LinearPMap.add_apply theorem

 (f g : E →ₗ.[R] F) (x : (f.domain ⊓ g.domain : Submodule R E)) : (f + g) x = f ⟨x, x.prop.1⟩ + g ⟨x, x.prop.2⟩

Full source

theorem add_apply (f g : E →ₗ.[R] F) (x : (f.domain ⊓ g.domain : Submodule R E)) :
    (f + g) x = f ⟨x, x.prop.1⟩ + g ⟨x, x.prop.2⟩ := rfl

Pointwise Addition of Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$ with additive commutative group structures. For any two partially defined linear maps $f, g : E \to_{.[R]} F$ and any element $x$ in the intersection of their domains (i.e., $x \in f.\text{domain} \cap g.\text{domain}$), the sum $(f + g)(x)$ is equal to $f(x) + g(x)$.

LinearPMap.instAddSemigroup instance

: AddSemigroup (E →ₗ.[R] F)

Full source

instance instAddSemigroup : AddSemigroup (E →ₗ.[R] F) :=
  ⟨fun f g h => by
    ext x y hxy
    · simp only [add_domain, inf_assoc]
    · simp only [add_apply, hxy, add_assoc]⟩

Additive Semigroup Structure on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$ and $F$ over $R$ with additive commutative group structures, the set of partially defined linear maps from $E$ to $F$ forms an additive semigroup under pointwise addition on the intersection of their domains.

LinearPMap.instAddZeroClass instance

: AddZeroClass (E →ₗ.[R] F)

Full source

instance instAddZeroClass : AddZeroClass (E →ₗ.[R] F) :=
  ⟨fun f => by
    ext x y hxy
    · simp [add_domain]
    · simp only [add_apply, hxy, zero_apply, zero_add],
  fun f => by
    ext x y hxy
    · simp [add_domain]
    · simp only [add_apply, hxy, zero_apply, add_zero]⟩

Additive Zero Class Structure on Partially Defined Linear Maps

Informal description

The set of partially defined linear maps $E \toₗ.[R] F$ between modules $E$ and $F$ over a ring $R$ forms an additive zero class. This means it is equipped with a zero map and an addition operation that satisfies the additive identity laws: $0 + f = f$ and $f + 0 = f$ for any partially defined linear map $f$.

LinearPMap.instAddMonoid instance

: AddMonoid (E →ₗ.[R] F)

Full source

instance instAddMonoid : AddMonoid (E →ₗ.[R] F) where
  zero_add f := by
    simp
  add_zero := by
    simp
  nsmul := nsmulRec

Additive Monoid Structure on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$ with additive commutative group structures, the set of partially defined linear maps from $E$ to $F$ forms an additive monoid under pointwise addition on the intersection of their domains. This means it has an associative addition operation with a zero element that acts as an additive identity.

LinearPMap.instAddCommMonoid instance

: AddCommMonoid (E →ₗ.[R] F)

Full source

instance instAddCommMonoid : AddCommMonoid (E →ₗ.[R] F) :=
  ⟨fun f g => by
    ext x y hxy
    · simp only [add_domain, inf_comm]
    · simp only [add_apply, hxy, add_comm]⟩

Additive Commutative Monoid Structure on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$ with additive commutative group structures, the set of partially defined linear maps from $E$ to $F$ forms an additive commutative monoid under pointwise addition on the intersection of their domains. This means the addition operation is commutative and associative with a zero element acting as the additive identity.

LinearPMap.instVAdd instance

: VAdd (E →ₗ[R] F) (E →ₗ.[R] F)

Full source

instance instVAdd : VAdd (E →ₗ[R] F) (E →ₗ.[R] F) :=
  ⟨fun f g =>
    { domain := g.domain
      toFun := f.comp g.domain.subtype + g.toFun }⟩

Vector Addition on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, the space of partially defined linear maps $E \toₗ.[R] F$ has a vector addition structure where any linear map $f : E \toₗ[R] F$ can act on a partially defined linear map $g : E \toₗ.[R] F$ by pointwise addition.

LinearPMap.vadd_domain theorem

(f : E →ₗ[R] F) (g : E →ₗ.[R] F) : (f +ᵥ g).domain = g.domain

Full source

@[simp]
theorem vadd_domain (f : E →ₗ[R] F) (g : E →ₗ.[R] F) : (f +ᵥ g).domain = g.domain :=
  rfl

Domain Preservation under Vector Addition of Linear Maps

Informal description

For any linear map $f \colon E \to F$ and any partially defined linear map $g \colon E \toₗ.[R] F$ over a ring $R$, the domain of the vector addition $f +ᵥ g$ is equal to the domain of $g$.

LinearPMap.vadd_apply theorem

(f : E →ₗ[R] F) (g : E →ₗ.[R] F) (x : (f +ᵥ g).domain) : (f +ᵥ g) x = f x + g x

Full source

theorem vadd_apply (f : E →ₗ[R] F) (g : E →ₗ.[R] F) (x : (f +ᵥ g).domain) :
    (f +ᵥ g) x = f x + g x :=
  rfl

Evaluation of Vector Addition on Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$ with additive commutative group structures. For any linear map $f \colon E \to_{R} F$ and any partially defined linear map $g \colon E \to_{.[R]} F$, the evaluation of the vector addition $f +ᵥ g$ at any point $x$ in its domain is given by $(f +ᵥ g)(x) = f(x) + g(x)$.

LinearPMap.coe_vadd theorem

(f : E →ₗ[R] F) (g : E →ₗ.[R] F) : ⇑(f +ᵥ g) = ⇑(f.comp g.domain.subtype) + ⇑g

Full source

@[simp]
theorem coe_vadd (f : E →ₗ[R] F) (g : E →ₗ.[R] F) : ⇑(f +ᵥ g) = ⇑(f.comp g.domain.subtype) + ⇑g :=
  rfl

Vector Addition Formula for Partially Defined Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any linear map $f \colon E \to_{R} F$ and any partially defined linear map $g \colon E \to_{.[R]} F$, the underlying function of the vector addition $f +ᵥ g$ is equal to the sum of the underlying function of $f$ composed with the inclusion map of the domain of $g$ and the underlying function of $g$. In symbols: \[ (f +ᵥ g)(x) = f(x) + g(x) \quad \text{for all } x \in \text{dom}(g). \]

LinearPMap.instAddAction instance

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

Full source

instance instAddAction : AddAction (E →ₗ[R] F) (E →ₗ.[R] F) where
  vadd := (· +ᵥ ·)
  zero_vadd := fun ⟨_s, _f⟩ => ext' <| zero_add _
  add_vadd := fun _f₁ _f₂ ⟨_s, _g⟩ => ext' <| LinearMap.ext fun _x => add_assoc _ _ _

Additive Action of Linear Maps on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, the space of partially defined linear maps $E \toₗ.[R] F$ has an additive action structure by the space of linear maps $E \toₗ[R] F$. This means that any linear map $f : E \toₗ[R] F$ can act on a partially defined linear map $g : E \toₗ.[R] F$ by pointwise addition, resulting in another partially defined linear map whose domain is the intersection of the domains of $f$ and $g$.

LinearPMap.instSub instance

: Sub (E →ₗ.[R] F)

Full source

instance instSub : Sub (E →ₗ.[R] F) :=
  ⟨fun f g =>
    { domain := f.domain ⊓ g.domain
      toFun := f.toFun.comp (inclusion (inf_le_left : f.domain ⊓ g.domain ≤ _))
        - g.toFun.comp (inclusion (inf_le_right : f.domain ⊓ g.domain ≤ _)) }⟩

Subtraction of Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$, the type of partially defined linear maps $E \toₗ.[R] F$ has a subtraction operation. Specifically, given two such maps $f$ and $g$, their difference $f - g$ is defined on the intersection of their domains and satisfies $(f - g)(x) = f(x) - g(x)$ for all $x$ in this intersection.

LinearPMap.sub_domain theorem

(f g : E →ₗ.[R] F) : (f - g).domain = f.domain ⊓ g.domain

Full source

theorem sub_domain (f g : E →ₗ.[R] F) : (f - g).domain = f.domain ⊓ g.domain := rfl

Domain of Difference of Partial Linear Maps is Intersection of Domains

Informal description

Let $R$ be a ring and let $E$, $F$ be modules over $R$. For any two partially defined linear maps $f, g : E \toₗ.[R] F$, the domain of their difference $f - g$ is equal to the intersection of their domains, i.e., $\text{dom}(f - g) = \text{dom}(f) \cap \text{dom}(g)$.

LinearPMap.sub_apply theorem

 (f g : E →ₗ.[R] F) (x : (f.domain ⊓ g.domain : Submodule R E)) : (f - g) x = f ⟨x, x.prop.1⟩ - g ⟨x, x.prop.2⟩

Full source

theorem sub_apply (f g : E →ₗ.[R] F) (x : (f.domain ⊓ g.domain : Submodule R E)) :
    (f - g) x = f ⟨x, x.prop.1⟩ - g ⟨x, x.prop.2⟩ := rfl

Difference of Partially Defined Linear Maps Evaluates to Difference of Values

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. For any two partially defined linear maps $f, g : E \to_{.[R]} F$ and any element $x$ in the intersection of their domains, the value of the difference map $f - g$ at $x$ is given by $(f - g)(x) = f(x) - g(x)$.

LinearPMap.instSubtractionCommMonoid instance

: SubtractionCommMonoid (E →ₗ.[R] F)

Full source

instance instSubtractionCommMonoid : SubtractionCommMonoid (E →ₗ.[R] F) where
  add_comm := add_comm
  sub_eq_add_neg f g := by
    ext x _ h
    · rfl
    simp [sub_apply, add_apply, neg_apply, ← sub_eq_add_neg, h]
  neg_neg := neg_neg
  neg_add_rev f g := by
    ext x _ h
    · simp [add_domain, sub_domain, neg_domain, And.comm]
    simp [sub_apply, add_apply, neg_apply, ← sub_eq_add_neg, h]
  neg_eq_of_add f g h' := by
    ext x hf hg
    · have : (0 : E →ₗ.[R] F).domain = ⊤ := zero_domain
      simp only [← h', add_domain, inf_eq_top_iff] at this
      rw [neg_domain, this.1, this.2]
    simp only [neg_domain, neg_apply, neg_eq_iff_add_eq_zero]
    rw [ext_iff] at h'
    rcases h' with ⟨hdom, h'⟩
    rw [zero_domain] at hdom
    simp only [hdom, neg_domain, zero_domain, mem_top, zero_apply, forall_true_left] at h'
    apply h'
  zsmul := zsmulRec

Commutative Subtraction Monoid Structure on Partially Defined Linear Maps

Informal description

For any ring $R$ and modules $E$, $F$ over $R$ with additive commutative group structures, the type of partially defined linear maps $E \toₗ.[R] F$ forms a commutative subtraction monoid. This means it has a commutative addition operation with a zero element, and a subtraction operation that satisfies the axioms of a subtraction monoid.

LinearPMap.supSpanSingleton definition

(f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) : E →ₗ.[K] F

Full source

/-- Extend a `LinearPMap` to `f.domain ⊔ K ∙ x`. -/
noncomputable def supSpanSingleton (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) :
    E →ₗ.[K] F :=
  f.sup (mkSpanSingleton x y fun h₀ => hx <| h₀.symm ▸ f.domain.zero_mem) <|
    sup_h_of_disjoint _ _ <| by simpa [disjoint_span_singleton] using fun h ↦ False.elim <| hx h

Extension of a partially defined linear map by a singleton

Informal description

Given a partially defined linear map $ f : E \to_{.[K]} F $ over a division ring $ K $, an element $ x \in E $ not in the domain of $ f $, and an element $ y \in F $, the function `supSpanSingleton` extends $ f $ to the linear span of $ f.domain \cup \{x\} $. The extended map sends $ x $ to $ y $ and agrees with $ f $ on its original domain. More precisely, the extended map is defined on $ f.domain \sqcup K \cdot x $, and for any $ x' \in f.domain $ and $ c \in K $, it maps $ x' + c \cdot x $ to $ f(x') + c \cdot y $.

LinearPMap.domain_supSpanSingleton theorem

(f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) : (f.supSpanSingleton x y hx).domain = f.domain ⊔ K ∙ x

Full source

@[simp]
theorem domain_supSpanSingleton (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) :
    (f.supSpanSingleton x y hx).domain = f.domain ⊔ K ∙ x :=
  rfl

Domain of the Extension of a Partially Defined Linear Map by a Singleton

Informal description

Let $K$ be a division ring, $E$ and $F$ be modules over $K$, and $f : E \to_{.[K]} F$ be a partially defined linear map. For any $x \in E$ not in the domain of $f$ and any $y \in F$, the domain of the extended map $f.\text{supSpanSingleton}\,x\,y\,hx$ is equal to the supremum of the original domain $f.\text{domain}$ and the span of $\{x\}$, i.e., $(f.\text{supSpanSingleton}\,x\,y\,hx).\text{domain} = f.\text{domain} \sqcup K \cdot x$.

LinearPMap.supSpanSingleton_apply_mk theorem

 (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, mem_sup.2 ⟨x', hx', _, mem_span_singleton.2 ⟨c, rfl⟩, rfl⟩⟩ =
    f ⟨x', hx'⟩ + c • y

Full source

@[simp]
theorem supSpanSingleton_apply_mk (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, mem_sup.2 ⟨x', hx', _, mem_span_singleton.2 ⟨c, rfl⟩, rfl⟩⟩ =
      f ⟨x', hx'⟩ + c • y := by
  unfold supSpanSingleton
  rw [sup_apply _ ⟨x', hx'⟩ ⟨c • x, _⟩, mkSpanSingleton'_apply]
  · exact mem_span_singleton.2 ⟨c, rfl⟩
  · rfl

Evaluation of Extended Linear Map on Sum of Domain Element and Scalar Multiple

Informal description

Let $K$ be a division ring, $E$ and $F$ be $K$-modules, and $f : E \to_{.[K]} F$ be a partially defined linear map. For any $x \in E$ not in the domain of $f$, any $y \in F$, any $x' \in E$ in the domain of $f$, and any scalar $c \in K$, the extended map $f.\text{supSpanSingleton}\,x\,y\,hx$ evaluated at $x' + c \cdot x$ equals $f(x') + c \cdot y$.

LinearPMap.sSup definition

(c : Set (E →ₗ.[R] F)) (hc : DirectedOn (· ≤ ·) c) : E →ₗ.[R] F

Full source

protected noncomputable def sSup (c : Set (E →ₗ.[R] F)) (hc : DirectedOn (· ≤ ·) c) : E →ₗ.[R] F :=
  ⟨_, Classical.choose <| sSup_aux c hc⟩

Supremum of a directed set of partially defined linear maps

Informal description

Given a directed set $ c $ of partially defined linear maps from $ E $ to $ F $ over a ring $ R $, the supremum $ \text{sSup} $ is the unique partially defined linear map on the supremum of their domains that extends all maps in $ c $.

LinearPMap.le_sSup theorem

 {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {f : E →ₗ.[R] F} (hf : f ∈ c) : f ≤ LinearPMap.sSup c hc

Full source

protected theorem le_sSup {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {f : E →ₗ.[R] F}
    (hf : f ∈ c) : f ≤ LinearPMap.sSup c hc :=
  Classical.choose_spec (sSup_aux c hc) hf

Partial Order Property: $f \leq \mathrm{sSup}\, c$ for Directed Sets of Partial Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$ with additive commutative group structures. Given a directed set $c$ of partially defined linear maps from $E$ to $F$ (with respect to the partial order $\leq$ on such maps), and a map $f \in c$, then $f$ is less than or equal to the supremum $\mathrm{sSup}\, c$ of the set $c$.

LinearPMap.sSup_le theorem

 {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {g : E →ₗ.[R] F} (hg : ∀ f ∈ c, f ≤ g) : LinearPMap.sSup c hc ≤ g

Full source

protected theorem sSup_le {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {g : E →ₗ.[R] F}
    (hg : ∀ f ∈ c, f ≤ g) : LinearPMap.sSup c hc ≤ g :=
  le_of_eqLocus_ge <|
    sSup_le fun _ ⟨f, hf, Eq⟩ =>
      Eq ▸
        have : f ≤ LinearPMap.sSupLinearPMap.sSup c hc ⊓ g := le_inf (LinearPMap.le_sSup _ hf) (hg f hf)
        this.1

Supremum of Directed Set of Partial Linear Maps is Least Upper Bound

Informal description

Let $R$ be a ring, and let $E$ and $F$ be $R$-modules. Given a directed set $c$ of partially defined linear maps from $E$ to $F$ (with respect to the partial order $\leq$ on such maps) and a partially defined linear map $g : E \to_{.[R]} F$ such that every $f \in c$ satisfies $f \leq g$, then the supremum $\mathrm{sSup}\, c$ of the set $c$ is less than or equal to $g$.

LinearPMap.sSup_apply theorem

 {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {l : E →ₗ.[R] F} (hl : l ∈ c) (x : l.domain) :
  (LinearPMap.sSup c hc) ⟨x, (LinearPMap.le_sSup hc hl).1 x.2⟩ = l x

Full source

protected theorem sSup_apply {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {l : E →ₗ.[R] F}
    (hl : l ∈ c) (x : l.domain) :
    (LinearPMap.sSup c hc) ⟨x, (LinearPMap.le_sSup hc hl).1 x.2⟩ = l x := by
  symm
  apply (Classical.choose_spec (sSup_aux c hc) hl).2
  rfl

Evaluation of the Supremum of a Directed Set of Partial Linear Maps

Informal description

Let $R$ be a ring, and let $E$ and $F$ be $R$-modules. Given a directed set $c$ of partially defined linear maps from $E$ to $F$ (with respect to the partial order $\leq$ on such maps) and a map $l \in c$, for any $x$ in the domain of $l$, the value of the supremum $\mathrm{sSup}\, c$ at $x$ (considered as an element of the domain of $\mathrm{sSup}\, c$) is equal to $l(x)$.

LinearMap.toPMap definition

(f : E →ₗ[R] F) (p : Submodule R E) : E →ₗ.[R] F

Full source

/-- Restrict a linear map to a submodule, reinterpreting the result as a `LinearPMap`. -/
def toPMap (f : E →ₗ[R] F) (p : Submodule R E) : E →ₗ.[R] F :=
  ⟨p, f.comp p.subtype⟩

Restriction of a linear map to a submodule as a partially defined linear map

Informal description

Given a linear map $f \colon E \to F$ over a ring $R$ and a submodule $p$ of $E$, the function `LinearMap.toPMap` restricts $f$ to $p$ and returns it as a partially defined linear map. Specifically, it constructs a `LinearPMap` with domain $p$ and the action given by the composition of $f$ with the inclusion map of $p$ into $E$.

LinearMap.toPMap_apply theorem

(f : E →ₗ[R] F) (p : Submodule R E) (x : p) : f.toPMap p x = f x

Full source

@[simp]
theorem toPMap_apply (f : E →ₗ[R] F) (p : Submodule R E) (x : p) : f.toPMap p x = f x :=
  rfl

Restricted Linear Map Evaluation: $(f \to_{.[R]} F)(x) = f(x)$ for $x \in p$

Informal description

Let $f \colon E \to F$ be a linear map over a ring $R$, and let $p$ be a submodule of $E$. For any $x \in p$, the value of the restricted linear map $f \to_{.[R]} F$ at $x$ is equal to the value of $f$ at $x$, i.e., $(f \to_{.[R]} F)(x) = f(x)$.

LinearMap.toPMap_domain theorem

(f : E →ₗ[R] F) (p : Submodule R E) : (f.toPMap p).domain = p

Full source

@[simp]
theorem toPMap_domain (f : E →ₗ[R] F) (p : Submodule R E) : (f.toPMap p).domain = p :=
  rfl

Domain of Restricted Linear Map Equals Submodule

Informal description

For any linear map $f \colon E \to F$ over a ring $R$ and any submodule $p$ of $E$, the domain of the partially defined linear map obtained by restricting $f$ to $p$ is equal to $p$ itself.

LinearMap.compPMap definition

(g : F →ₗ[R] G) (f : E →ₗ.[R] F) : E →ₗ.[R] G

Full source

/-- Compose a linear map with a `LinearPMap` -/
def compPMap (g : F →ₗ[R] G) (f : E →ₗ.[R] F) : E →ₗ.[R] G where
  domain := f.domain
  toFun := g.comp f.toFun

Composition of a linear map with a partially defined linear map

Informal description

Given a linear map $ g : F \to G $ and a partially defined linear map $ f : E \toₗ.[R] F $, the composition $ g \circ f $ is a partially defined linear map from $ E $ to $ G $ over the ring $ R $. The domain of the composition is the same as the domain of $ f $, and the function is defined by applying $ g $ to the result of $ f $.

LinearMap.compPMap_apply theorem

(g : F →ₗ[R] G) (f : E →ₗ.[R] F) (x) : g.compPMap f x = g (f x)

Full source

@[simp]
theorem compPMap_apply (g : F →ₗ[R] G) (f : E →ₗ.[R] F) (x) : g.compPMap f x = g (f x) :=
  rfl

Composition of Linear Map with Partially Defined Linear Map Preserves Evaluation

Informal description

Let $R$ be a ring, and let $E$, $F$, and $G$ be modules over $R$. Given a linear map $g \colon F \to G$ and a partially defined linear map $f \colon E \to_{.[R]} F$, for any $x$ in the domain of $f$, the composition $g \circ f$ evaluated at $x$ equals $g$ applied to $f(x)$, i.e., $(g \circ f)(x) = g(f(x))$.

LinearPMap.codRestrict definition

(f : E →ₗ.[R] F) (p : Submodule R F) (H : ∀ x, f x ∈ p) : E →ₗ.[R] p

Full source

/-- Restrict codomain of a `LinearPMap` -/
def codRestrict (f : E →ₗ.[R] F) (p : Submodule R F) (H : ∀ x, f x ∈ p) : E →ₗ.[R] p where
  domain := f.domain
  toFun := f.toFun.codRestrict p H

Codomain restriction of a partially defined linear map

Informal description

Given a partially defined linear map $ f : E \to_{.[R]} F $, a submodule $ p $ of $ F $, and a proof $ H $ that for every $ x $ in the domain of $ f $, the image $ f(x) $ lies in $ p $, the function `LinearPMap.codRestrict` restricts the codomain of $ f $ to $ p $. The resulting partially defined linear map has the same domain as $ f $ and maps elements to their images in $ p $.

LinearPMap.comp definition

(g : F →ₗ.[R] G) (f : E →ₗ.[R] F) (H : ∀ x : f.domain, f x ∈ g.domain) : E →ₗ.[R] G

Full source

/-- Compose two `LinearPMap`s -/
def comp (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) (H : ∀ x : f.domain, f x ∈ g.domain) : E →ₗ.[R] G :=
  g.toFun.compPMap <| f.codRestrict _ H

Composition of partially defined linear maps

Informal description

Given two partially defined linear maps $ g : F \to_{.[R]} G $ and $ f : E \to_{.[R]} F $, and a proof $ H $ that for every $ x $ in the domain of $ f $, the image $ f(x) $ lies in the domain of $ g $, the composition $ g \circ f $ is a partially defined linear map from $ E $ to $ G $. The domain of the composition is the same as the domain of $ f $, and the function is defined by applying $ g $ to the result of $ f $.

LinearPMap.coprod definition

(f : E →ₗ.[R] G) (g : F →ₗ.[R] G) : E × F →ₗ.[R] G

Full source

/-- `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`. -/
def coprod (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) : E × FE × F →ₗ.[R] G where
  domain := f.domain.prod g.domain
  toFun :=
    -- Porting note: This is just
    -- `(f.comp (LinearPMap.fst f.domain g.domain) fun x => x.2.1).toFun +`
    -- `  (g.comp (LinearPMap.snd f.domain g.domain) fun x => x.2.2).toFun`,
    HAdd.hAdd
      (α := f.domain.prod g.domain →ₗ[R] G)
      (β := f.domain.prod g.domain →ₗ[R] G)
      (f.comp (LinearPMap.fst f.domain g.domain) fun x => x.2.1).toFun
      (g.comp (LinearPMap.snd f.domain g.domain) fun x => x.2.2).toFun

Coproduct of partially defined linear maps

Informal description

Given two partially defined linear maps $ f : E \to_{.[R]} G $ and $ g : F \to_{.[R]} G $, their coproduct $ f \coprod g $ is the partially defined linear map from $ E \times F $ to $ G $ defined on the product submodule $ \text{domain}(f) \times \text{domain}(g) $. For any $ (x, y) \in \text{domain}(f) \times \text{domain}(g) $, the coproduct is given by $ (f \coprod g)(x, y) = f(x) + g(y) $.

LinearPMap.coprod_apply theorem

 (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) (x) : f.coprod g x = f ⟨(x : E × F).1, x.2.1⟩ + g ⟨(x : E × F).2, x.2.2⟩

Full source

@[simp]
theorem coprod_apply (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) (x) :
    f.coprod g x = f ⟨(x : E × F).1, x.2.1⟩ + g ⟨(x : E × F).2, x.2.2⟩ :=
  rfl

Value of Coproduct of Partially Defined Linear Maps

Informal description

Let $f \colon E \to_{.[R]} G$ and $g \colon F \to_{.[R]} G$ be partially defined linear maps. For any $x$ in the domain of $f \coprod g$, the value of the coproduct map is given by $$(f \coprod g)(x) = f(x_1) + g(x_2),$$ where $x = (x_1, x_2) \in E \times F$ with $x_1 \in \text{domain}(f)$ and $x_2 \in \text{domain}(g)$.

LinearPMap.domRestrict definition

(f : E →ₗ.[R] F) (S : Submodule R E) : E →ₗ.[R] F

Full source

/-- Restrict a partially defined linear map to a submodule of `E` contained in `f.domain`. -/
def domRestrict (f : E →ₗ.[R] F) (S : Submodule R E) : E →ₗ.[R] F :=
  ⟨S ⊓ f.domain, f.toFun.comp (Submodule.inclusion (by simp))⟩

Restriction of a partially defined linear map to a submodule

Informal description

Given a partially defined linear map $ f : E \toₗ.[R] F $ and a submodule $ S $ of $ E $, the restriction of $ f $ to $ S $, denoted $ f.domRestrict \, S $, is the partially defined linear map with domain $ S \cap f.domain $ that agrees with $ f $ on their common domain. More precisely, for any $ x \in S \cap f.domain $, we have $ (f.domRestrict \, S) \, x = f \, x $.

LinearPMap.domRestrict_domain theorem

(f : E →ₗ.[R] F) {S : Submodule R E} : (f.domRestrict S).domain = S ⊓ f.domain

Full source

@[simp]
theorem domRestrict_domain (f : E →ₗ.[R] F) {S : Submodule R E} :
    (f.domRestrict S).domain = S ⊓ f.domain :=
  rfl

Domain of Restricted Partially Defined Linear Map is Intersection with Submodule

Informal description

For any partially defined linear map $f \colon E \toₗ.[R] F$ and any submodule $S$ of $E$, the domain of the restriction $f.domRestrict\, S$ is equal to the intersection $S \cap f.domain$.

LinearPMap.domRestrict_apply theorem

 {f : E →ₗ.[R] F} {S : Submodule R E} ⦃x : ↥(S ⊓ f.domain)⦄ ⦃y : f.domain⦄ (h : (x : E) = y) : f.domRestrict S x = f y

Full source

theorem domRestrict_apply {f : E →ₗ.[R] F} {S : Submodule R E} ⦃x : ↥(S ⊓ f.domain)⦄ ⦃y : f.domain⦄
    (h : (x : E) = y) : f.domRestrict S x = f y := by
  have : Submodule.inclusion (by simp) x = y := by
    ext
    simp [h]
  rw [← this]
  exact LinearPMap.mk_apply _ _ _

Evaluation of Restricted Partially Defined Linear Map on Intersection Domain

Informal description

Let $R$ be a ring, $E$ and $F$ be $R$-modules, and $f \colon E \to_{.[R]} F$ be a partially defined linear map. For any submodule $S$ of $E$ and elements $x \in S \cap \text{domain}(f)$, $y \in \text{domain}(f)$ such that $x = y$ in $E$, the restriction $f|_{S}$ evaluated at $x$ equals $f$ evaluated at $y$, i.e., $f|_{S}(x) = f(y)$.

LinearPMap.domRestrict_le theorem

{f : E →ₗ.[R] F} {S : Submodule R E} : f.domRestrict S ≤ f

Full source

theorem domRestrict_le {f : E →ₗ.[R] F} {S : Submodule R E} : f.domRestrict S ≤ f :=
  ⟨by simp, fun _ _ hxy => domRestrict_apply hxy⟩

Restriction of Partially Defined Linear Map is Below Original Map

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ and any submodule $S$ of $E$, the restriction $f|_{S}$ is less than or equal to $f$ in the partial order of partially defined linear maps. This means that the domain of $f|_{S}$ is contained in the domain of $f$, and $f|_{S}$ agrees with $f$ on their common domain.

LinearPMap.graph definition

(f : E →ₗ.[R] F) : Submodule R (E × F)

Full source

/-- The graph of a `LinearPMap` viewed as a submodule on `E × F`. -/
def graph (f : E →ₗ.[R] F) : Submodule R (E × F) :=
  f.toFun.graph.map (f.domain.subtype.prodMap (LinearMap.id : F →ₗ[R] F))

Graph of a partially defined linear map

Informal description

The graph of a partially defined linear map $ f : E \toₗ.[R] F $ is the submodule of $ E \times F $ consisting of all pairs $ (x, f(x)) $ where $ x $ belongs to the domain of $ f $. More formally, the graph is the set $\{(x, y) \in E \times F \mid \exists (z \in \text{domain of } f), (z, y) = (x, f(z))\}$, which is closed under addition, scalar multiplication, and contains the zero vector.

LinearPMap.mem_graph_iff' theorem

(f : E →ₗ.[R] F) {x : E × F} : x ∈ f.graph ↔ ∃ y : f.domain, (↑y, f y) = x

Full source

theorem mem_graph_iff' (f : E →ₗ.[R] F) {x : E × F} :
    x ∈ f.graphx ∈ f.graph ↔ ∃ y : f.domain, (↑y, f y) = x := by simp [graph]

Characterization of Graph Membership for Partially Defined Linear Maps

Informal description

For a partially defined linear map $f \colon E \to_{.[R]} F$ and any element $x \in E \times F$, we have $x \in \text{graph}(f)$ if and only if there exists an element $y$ in the domain of $f$ such that $(y, f(y)) = x$.

LinearPMap.mem_graph_iff theorem

(f : E →ₗ.[R] F) {x : E × F} : x ∈ f.graph ↔ ∃ y : f.domain, (↑y : E) = x.1 ∧ f y = x.2

Full source

@[simp]
theorem mem_graph_iff (f : E →ₗ.[R] F) {x : E × F} :
    x ∈ f.graphx ∈ f.graph ↔ ∃ y : f.domain, (↑y : E) = x.1 ∧ f y = x.2 := by
  cases x
  simp_rw [mem_graph_iff', Prod.mk_inj]

Characterization of membership in the graph of a partially defined linear map

Informal description

For a partially defined linear map $f \colon E \to_{.[R]} F$ and any pair $x = (x_1, x_2) \in E \times F$, the pair $x$ belongs to the graph of $f$ if and only if there exists an element $y$ in the domain of $f$ such that $y = x_1$ (as elements of $E$) and $f(y) = x_2$.

LinearPMap.mem_graph theorem

(f : E →ₗ.[R] F) (x : domain f) : ((x : E), f x) ∈ f.graph

Full source

/-- The tuple `(x, f x)` is contained in the graph of `f`. -/
theorem mem_graph (f : E →ₗ.[R] F) (x : domain f) : ((x : E), f x)((x : E), f x) ∈ f.graph := by simp

Element and its image belong to the graph of a partially defined linear map

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ and any element $x$ in the domain of $f$, the pair $(x, f(x))$ belongs to the graph of $f$.

LinearPMap.graph_map_fst_eq_domain theorem

(f : E →ₗ.[R] F) : f.graph.map (LinearMap.fst R E F) = f.domain

Full source

theorem graph_map_fst_eq_domain (f : E →ₗ.[R] F) :
    f.graph.map (LinearMap.fst R E F) = f.domain := by
  ext x
  simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
    LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
  constructor <;> intro h
  · rcases h with ⟨x, hx, _⟩
    exact hx
  · use f ⟨x, h⟩
    simp only [h, exists_const]

First Projection of Graph Equals Domain for Partially Defined Linear Maps

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$, the image of its graph under the first projection linear map $\operatorname{fst} \colon E \times F \to E$ is equal to the domain of $f$. In other words, if $G_f = \{(x, f(x)) \mid x \in \operatorname{dom}(f)\}$ is the graph of $f$, then $\operatorname{fst}(G_f) = \operatorname{dom}(f)$.

LinearPMap.graph_map_snd_eq_range theorem

(f : E →ₗ.[R] F) : f.graph.map (LinearMap.snd R E F) = LinearMap.range f.toFun

Full source

theorem graph_map_snd_eq_range (f : E →ₗ.[R] F) :
    f.graph.map (LinearMap.snd R E F) = LinearMap.range f.toFun := by ext; simp

Second Projection of Graph Equals Range of Partially Defined Linear Map

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ over a ring $R$, the image of its graph under the second projection linear map $\operatorname{snd} \colon E \times F \to F$ is equal to the range of $f$, i.e., \[ \operatorname{map}_{\operatorname{snd}}(G(f)) = \operatorname{range}(f), \] where $G(f) = \{(x, f(x)) \mid x \in \operatorname{domain}(f)\}$ is the graph of $f$.

LinearPMap.smul_graph theorem

 (f : E →ₗ.[R] F) (z : M) :
  (z • f).graph = f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (z • (LinearMap.id : F →ₗ[R] F)))

Full source

/-- The graph of `z • f` as a pushforward. -/
theorem smul_graph (f : E →ₗ.[R] F) (z : M) :
    (z • f).graph =
      f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (z • (LinearMap.id : F →ₗ[R] F))) := by
  ext ⟨x_fst, x_snd⟩
  constructor <;> intro h
  · rw [mem_graph_iff] at h
    rcases h with ⟨y, hy, h⟩
    rw [LinearPMap.smul_apply] at h
    rw [Submodule.mem_map]
    simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.smul_apply, Prod.mk_inj, Prod.exists, exists_exists_and_eq_and]
    use x_fst, y, hy
  rw [Submodule.mem_map] at h
  rcases h with ⟨x', hx', h⟩
  cases x'
  simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.smul_apply,
    Prod.mk_inj] at h
  rw [mem_graph_iff] at hx' ⊢
  rcases hx' with ⟨y, hy, hx'⟩
  use y
  rw [← h.1, ← h.2]
  simp [hy, hx']

Graph of Scalar Multiple of a Partially Defined Linear Map

Informal description

For a partially defined linear map $f \colon E \to_{.[R]} F$ and a scalar $z$ in a monoid $M$, the graph of the scalar multiple $z \cdot f$ is equal to the image of the graph of $f$ under the linear map $( \operatorname{id}_E ) \times (z \cdot \operatorname{id}_F )$, where $\operatorname{id}_E$ and $\operatorname{id}_F$ are the identity maps on $E$ and $F$ respectively. In other words, the graph of $z \cdot f$ is obtained by scaling the second component of the graph of $f$ by $z$: \[ G(z \cdot f) = \{(x, z \cdot y) \mid (x, y) \in G(f)\}. \]

LinearPMap.neg_graph theorem

 (f : E →ₗ.[R] F) : (-f).graph = f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (-(LinearMap.id : F →ₗ[R] F)))

Full source

/-- The graph of `-f` as a pushforward. -/
theorem neg_graph (f : E →ₗ.[R] F) :
    (-f).graph =
    f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (-(LinearMap.id : F →ₗ[R] F))) := by
  ext ⟨x_fst, x_snd⟩
  constructor <;> intro h
  · rw [mem_graph_iff] at h
    rcases h with ⟨y, hy, h⟩
    rw [LinearPMap.neg_apply] at h
    rw [Submodule.mem_map]
    simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.neg_apply, Prod.mk_inj, Prod.exists, exists_exists_and_eq_and]
    use x_fst, y, hy
  rw [Submodule.mem_map] at h
  rcases h with ⟨x', hx', h⟩
  cases x'
  simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.neg_apply,
    Prod.mk_inj] at h
  rw [mem_graph_iff] at hx' ⊢
  rcases hx' with ⟨y, hy, hx'⟩
  use y
  rw [← h.1, ← h.2]
  simp [hy, hx']

Graph of the Negative of a Partially Defined Linear Map

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ over a ring $R$, the graph of $-f$ is equal to the image of the graph of $f$ under the linear map $(\operatorname{id}_E, -\operatorname{id}_F) \colon E \times F \to E \times F$. In other words, \[ G(-f) = \{ (x, -y) \mid (x, y) \in G(f) \}, \] where $G(f)$ denotes the graph of $f$.

LinearPMap.mem_graph_snd_inj theorem

 (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'

Full source

theorem mem_graph_snd_inj (f : E →ₗ.[R] F) {x y : E} {x' y' : F} (hx : (x, x')(x, x') ∈ f.graph)
    (hy : (y, y')(y, y') ∈ f.graph) (hxy : x = y) : x' = y' := by
  rw [mem_graph_iff] at hx hy
  rcases hx with ⟨x'', hx1, hx2⟩
  rcases hy with ⟨y'', hy1, hy2⟩
  simp only at hx1 hx2 hy1 hy2
  rw [← hx1, ← hy1, SetLike.coe_eq_coe] at hxy
  rw [← hx2, ← hy2, hxy]

Injectivity of Second Component in Graph of Partially Defined Linear Map

Informal description

Let $f \colon E \to_{.[R]} F$ be a partially defined linear map between modules $E$ and $F$ over a ring $R$. For any elements $x, y \in E$ and $x', y' \in F$ such that $(x, x')$ and $(y, y')$ belong to the graph of $f$, if $x = y$, then $x' = y'$.

LinearPMap.mem_graph_snd_inj' theorem

(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

Full source

theorem mem_graph_snd_inj' (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 := by
  cases x
  cases y
  exact f.mem_graph_snd_inj hx hy hxy

Injectivity of Second Component in Graph of Partially Defined Linear Map (Pair Version)

Informal description

Let $f \colon E \to_{.[R]} F$ be a partially defined linear map between modules $E$ and $F$ over a ring $R$. For any pairs $(x, x')$ and $(y, y')$ in $E \times F$ that belong to the graph of $f$, if the first components are equal ($x = y$), then the second components are also equal ($x' = y'$).

LinearPMap.graph_fst_eq_zero_snd theorem

(f : E →ₗ.[R] F) {x : E} {x' : F} (h : (x, x') ∈ f.graph) (hx : x = 0) : x' = 0

Full source

/-- The property that `f 0 = 0` in terms of the graph. -/
theorem graph_fst_eq_zero_snd (f : E →ₗ.[R] F) {x : E} {x' : F} (h : (x, x')(x, x') ∈ f.graph)
    (hx : x = 0) : x' = 0 :=
  f.mem_graph_snd_inj h f.graph.zero_mem hx

Vanishing of Graph at Zero for Partially Defined Linear Maps

Informal description

Let $f \colon E \to_{.[R]} F$ be a partially defined linear map between modules $E$ and $F$ over a ring $R$. For any $x \in E$ and $x' \in F$ such that $(x, x')$ belongs to the graph of $f$, if $x = 0$, then $x' = 0$.

LinearPMap.mem_domain_iff theorem

{f : E →ₗ.[R] F} {x : E} : x ∈ f.domain ↔ ∃ y : F, (x, y) ∈ f.graph

Full source

theorem mem_domain_iff {f : E →ₗ.[R] F} {x : E} : x ∈ f.domainx ∈ f.domain ↔ ∃ y : F, (x, y) ∈ f.graph := by
  constructor <;> intro h
  · use f ⟨x, h⟩
    exact f.mem_graph ⟨x, h⟩
  obtain ⟨y, h⟩ := h
  rw [mem_graph_iff] at h
  obtain ⟨x', h⟩ := h
  simp only at h
  rw [← h.1]
  simp

Characterization of Domain Membership via Graph of a Partially Defined Linear Map

Informal description

For a partially defined linear map $f \colon E \to_{.[R]} F$ and an element $x \in E$, $x$ belongs to the domain of $f$ if and only if there exists $y \in F$ such that the pair $(x, y)$ is in the graph of $f$.

LinearPMap.mem_domain_of_mem_graph theorem

{f : E →ₗ.[R] F} {x : E} {y : F} (h : (x, y) ∈ f.graph) : x ∈ f.domain

Full source

theorem mem_domain_of_mem_graph {f : E →ₗ.[R] F} {x : E} {y : F} (h : (x, y)(x, y) ∈ f.graph) :
    x ∈ f.domain := by
  rw [mem_domain_iff]
  exact ⟨y, h⟩

Domain membership from graph inclusion for partially defined linear maps

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ and any elements $x \in E$, $y \in F$, if the pair $(x, y)$ belongs to the graph of $f$, then $x$ is in the domain of $f$.

LinearPMap.image_iff theorem

{f : E →ₗ.[R] F} {x : E} {y : F} (hx : x ∈ f.domain) : y = f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph

Full source

theorem image_iff {f : E →ₗ.[R] F} {x : E} {y : F} (hx : x ∈ f.domain) :
    y = f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph := by
  rw [mem_graph_iff]
  constructor <;> intro h
  · use ⟨x, hx⟩
    simp [h]
  rcases h with ⟨⟨x', hx'⟩, ⟨h1, h2⟩⟩
  simp only [Submodule.coe_mk] at h1 h2
  simp only [← h2, h1]

Characterization of the image of a point in the graph of a partially defined linear map

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f \colon E \to_{.[R]} F$ be a partially defined linear map. For any $x \in E$ in the domain of $f$ and any $y \in F$, we have $y = f(x)$ if and only if the pair $(x, y)$ belongs to the graph of $f$.

LinearPMap.mem_range_iff theorem

{f : E →ₗ.[R] F} {y : F} : y ∈ Set.range f ↔ ∃ x : E, (x, y) ∈ f.graph

Full source

theorem mem_range_iff {f : E →ₗ.[R] F} {y : F} : y ∈ Set.range fy ∈ Set.range f ↔ ∃ x : E, (x, y) ∈ f.graph := by
  constructor <;> intro h
  · rw [Set.mem_range] at h
    rcases h with ⟨⟨x, hx⟩, h⟩
    use x
    rw [← h]
    exact f.mem_graph ⟨x, hx⟩
  obtain ⟨x, h⟩ := h
  rw [mem_graph_iff] at h
  obtain ⟨x, h⟩ := h
  rw [Set.mem_range]
  use x
  simp only at h
  rw [h.2]

Characterization of Range Membership via Graph of a Partially Defined Linear Map

Informal description

For a partially defined linear map $f \colon E \to_{.[R]} F$ and any element $y \in F$, $y$ belongs to the range of $f$ if and only if there exists an element $x \in E$ such that the pair $(x, y)$ is in the graph of $f$.

LinearPMap.mem_domain_iff_of_eq_graph theorem

{f g : E →ₗ.[R] F} (h : f.graph = g.graph) {x : E} : x ∈ f.domain ↔ x ∈ g.domain

Full source

theorem mem_domain_iff_of_eq_graph {f g : E →ₗ.[R] F} (h : f.graph = g.graph) {x : E} :
    x ∈ f.domainx ∈ f.domain ↔ x ∈ g.domain := by simp_rw [mem_domain_iff, h]

Equality of domains for partially defined linear maps with identical graphs

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f, g: E \toₗ.[R] F$ be two partially defined linear maps. If $f$ and $g$ have the same graph (i.e., $f.\text{graph} = g.\text{graph}$), then for any $x \in E$, we have $x \in \text{domain}(f)$ if and only if $x \in \text{domain}(g)$.

LinearPMap.le_of_le_graph theorem

{f g : E →ₗ.[R] F} (h : f.graph ≤ g.graph) : f ≤ g

Full source

theorem le_of_le_graph {f g : E →ₗ.[R] F} (h : f.graph ≤ g.graph) : f ≤ g := by
  constructor
  · intro x hx
    rw [mem_domain_iff] at hx ⊢
    obtain ⟨y, hx⟩ := hx
    use y
    exact h hx
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  rw [image_iff]
  refine h ?_
  simp only [Submodule.coe_mk] at hxy
  rw [hxy] at hx
  rw [← image_iff hx]
  simp [hxy]

Partial Order on Linear Maps via Graph Inclusion

Informal description

Let $E$ and $F$ be modules over a ring $R$, and let $f, g \colon E \to_{.[R]} F$ be two partially defined linear maps. If the graph of $f$ is contained in the graph of $g$ (as submodules of $E \times F$), then $f \leq g$ in the partial order of partially defined linear maps.

LinearPMap.le_graph_of_le theorem

{f g : E →ₗ.[R] F} (h : f ≤ g) : f.graph ≤ g.graph

Full source

theorem le_graph_of_le {f g : E →ₗ.[R] F} (h : f ≤ g) : f.graph ≤ g.graph := by
  intro x hx
  rw [mem_graph_iff] at hx ⊢
  obtain ⟨y, hx⟩ := hx
  use ⟨y, h.1 y.2⟩
  simp only [hx, Submodule.coe_mk, eq_self_iff_true, true_and]
  convert hx.2 using 1
  refine (h.2 ?_).symm
  simp only [hx.1, Submodule.coe_mk]

Graph inclusion under partial order of partially defined linear maps

Informal description

For any two partially defined linear maps $f, g \colon E \to_{.[R]} F$ over a ring $R$, if $f \leq g$ in the partial order of partially defined linear maps, then the graph of $f$ is contained in the graph of $g$ as submodules of $E \times F$.

LinearPMap.le_graph_iff theorem

{f g : E →ₗ.[R] F} : f.graph ≤ g.graph ↔ f ≤ g

Full source

theorem le_graph_iff {f g : E →ₗ.[R] F} : f.graph ≤ g.graph ↔ f ≤ g :=
  ⟨le_of_le_graph, le_graph_of_le⟩

Graph Inclusion Criterion for Partial Order of Linear Maps

Informal description

For any two partially defined linear maps $f, g \colon E \to_{.[R]} F$ over a ring $R$, the graph of $f$ is contained in the graph of $g$ (as submodules of $E \times F$) if and only if $f \leq g$ in the partial order of partially defined linear maps.

Submodule.existsUnique_from_graph theorem

 {g : Submodule R (E × F)} (hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E}
  (ha : a ∈ g.map (LinearMap.fst R E F)) : ∃! b : F, (a, b) ∈ g

Full source

theorem existsUnique_from_graph {g : Submodule R (E × F)}
    (hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E}
    (ha : a ∈ g.map (LinearMap.fst R E F)) : ∃! b : F, (a, b) ∈ g := by
  refine existsUnique_of_exists_of_unique ?_ ?_
  · convert ha
    simp
  intro y₁ y₂ hy₁ hy₂
  have hy : ((0 : E), y₁ - y₂)((0 : E), y₁ - y₂) ∈ g := by
    convert g.sub_mem hy₁ hy₂
    exact (sub_self _).symm
  exact sub_eq_zero.mp (hg hy (by simp))

Unique Existence of Second Component in Submodule Graph

Informal description

Let $R$ be a ring, $E$ and $F$ be modules over $R$, and $g$ be a submodule of $E \times F$. Suppose that for any $(x,y) \in g$ with $x = 0$, we have $y = 0$. Then for any $a \in E$ in the image of $g$ under the first projection, there exists a unique $b \in F$ such that $(a,b) \in g$.

Submodule.valFromGraph definition

 {g : Submodule R (E × F)} (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E}
  (ha : a ∈ g.map (LinearMap.fst R E F)) : F

Full source

/-- Auxiliary definition to unfold the existential quantifier. -/
noncomputable def valFromGraph {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E}
    (ha : a ∈ g.map (LinearMap.fst R E F)) : F :=
  (ExistsUnique.exists (existsUnique_from_graph @hg ha)).choose

Value from graph of a submodule

Informal description

Given a submodule $g$ of $E \times F$ over a ring $R$ with the property that for any $(x, y) \in g$, if $x = 0$ then $y = 0$, and given an element $a \in E$ that lies in the image of $g$ under the first projection, the function returns the unique element $b \in F$ such that $(a, b) \in g$.

Submodule.valFromGraph_mem theorem

 {g : Submodule R (E × F)} (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E}
  (ha : a ∈ g.map (LinearMap.fst R E F)) : (a, valFromGraph hg ha) ∈ g

Full source

theorem valFromGraph_mem {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E}
    (ha : a ∈ g.map (LinearMap.fst R E F)) : (a, valFromGraph hg ha)(a, valFromGraph hg ha) ∈ g :=
  (ExistsUnique.exists (existsUnique_from_graph @hg ha)).choose_spec

Membership of Graph Value in Submodule

Informal description

Let $R$ be a ring, $E$ and $F$ be modules over $R$, and $g$ be a submodule of $E \times F$. Suppose that for any $(x, y) \in g$, if $x = 0$ then $y = 0$. Then for any $a \in E$ in the image of $g$ under the first projection, the pair $(a, \text{valFromGraph}(hg)(ha))$ belongs to $g$.

Submodule.toLinearPMapAux definition

 (g : Submodule R (E × F)) (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
  g.map (LinearMap.fst R E F) →ₗ[R] F

Full source

/-- Define a `LinearMap` from its graph.

Helper definition for `LinearPMap`. -/
noncomputable def toLinearPMapAux (g : Submodule R (E × F))
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
    g.map (LinearMap.fst R E F) →ₗ[R] F where
  toFun := fun x => valFromGraph hg x.2
  map_add' := fun v w => by
    have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2
    have hvw := valFromGraph_mem hg hadd
    have hvw' := g.add_mem (valFromGraph_mem hg v.2) (valFromGraph_mem hg w.2)
    rw [Prod.mk_add_mk] at hvw'
    exact (existsUnique_from_graph @hg hadd).unique hvw hvw'
  map_smul' := fun a v => by
    have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
    have hav := valFromGraph_mem hg hsmul
    have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
    rw [Prod.smul_mk] at hav'
    exact (existsUnique_from_graph @hg hsmul).unique hav hav'

Linear map defined by a submodule graph

Informal description

Given a submodule $g$ of $E \times F$ over a ring $R$ with the property that for any $(x, y) \in g$, if $x = 0$ then $y = 0$, the function constructs a linear map from the projection of $g$ onto $E$ (i.e., $\{x \in E \mid \exists y \in F, (x,y) \in g\}$) to $F$. This map sends each $x$ in the domain to the unique $y \in F$ such that $(x,y) \in g$.

Submodule.toLinearPMap definition

(g : Submodule R (E × F)) : E →ₗ.[R] F

Full source

/-- 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. -/
noncomputable def toLinearPMap (g : Submodule R (E × F)) : E →ₗ.[R] F where
  domain := g.map (LinearMap.fst R E F)
  toFun := if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0 then
    g.toLinearPMapAux hg else 0

Partially defined linear map from a submodule graph

Informal description

Given a submodule $g$ of $E \times F$ over a ring $R$, the function constructs a partially defined linear map from $E$ to $F$ whose domain is the projection of $g$ onto $E$ (i.e., $\{x \in E \mid \exists y \in F, (x,y) \in g\}$). The linear map is defined by sending each $x$ in the domain to the unique $y \in F$ such that $(x,y) \in g$, provided that for any $(x, y) \in g$, if $x = 0$ then $y = 0$. If this condition is not satisfied, the resulting map is the zero map.

Submodule.toLinearPMap_domain theorem

(g : Submodule R (E × F)) : g.toLinearPMap.domain = g.map (LinearMap.fst R E F)

Full source

theorem toLinearPMap_domain (g : Submodule R (E × F)) :
    g.toLinearPMap.domain = g.map (LinearMap.fst R E F) := rfl

Domain of Partially Defined Linear Map from Submodule Graph

Informal description

For any submodule $g$ of $E \times F$ over a ring $R$, the domain of the partially defined linear map constructed from $g$ is equal to the projection of $g$ onto $E$, i.e., $\text{domain}(g.\text{toLinearPMap}) = \text{map}(\text{fst}_{R,E,F})(g)$.

Submodule.toLinearPMap_apply_aux theorem

 {g : Submodule R (E × F)} (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
  (x : g.map (LinearMap.fst R E F)) : g.toLinearPMap x = valFromGraph hg x.2

Full source

theorem toLinearPMap_apply_aux {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
    (x : g.map (LinearMap.fst R E F)) :
    g.toLinearPMap x = valFromGraph hg x.2 := by
  classical
  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
  rw [dif_pos]
  · rfl
  · exact hg

Value of Partially Defined Linear Map from Submodule Graph

Informal description

Let $g$ be a submodule of $E \times F$ over a ring $R$ such that for any $(x, y) \in g$, if $x = 0$ then $y = 0$. For any $x$ in the projection of $g$ onto $E$ (i.e., $x \in \text{map} (\text{LinearMap.fst} R E F) g$), the value of the partially defined linear map $g.\text{toLinearPMap}$ at $x$ is equal to $\text{valFromGraph} hg x.2$, where $x.2$ denotes the proof that $x$ is in the projection of $g$ onto $E$.

Submodule.mem_graph_toLinearPMap theorem

 {g : Submodule R (E × F)} (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
  (x : g.map (LinearMap.fst R E F)) : (x.val, g.toLinearPMap x) ∈ g

Full source

theorem mem_graph_toLinearPMap {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
    (x : g.map (LinearMap.fst R E F)) : (x.val, g.toLinearPMap x)(x.val, g.toLinearPMap x) ∈ g := by
  rw [toLinearPMap_apply_aux hg]
  exact valFromGraph_mem hg x.2

Graph Membership of Partially Defined Linear Map from Submodule

Informal description

Let $R$ be a ring, $E$ and $F$ be modules over $R$, and $g$ be a submodule of $E \times F$ such that for any $(x, y) \in g$, if $x = 0$ then $y = 0$. For any $x$ in the projection of $g$ onto $E$ (i.e., $x \in \text{map}(\text{fst}_{R,E,F})(g)$), the pair $(x, g.\text{toLinearPMap}(x))$ belongs to $g$.

Submodule.toLinearPMap_graph_eq theorem

 (g : Submodule R (E × F)) (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) : g.toLinearPMap.graph = g

Full source

@[simp]
theorem toLinearPMap_graph_eq (g : Submodule R (E × F))
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
    g.toLinearPMap.graph = g := by
  ext ⟨x_fst, x_snd⟩
  constructor <;> intro hx
  · rw [LinearPMap.mem_graph_iff] at hx
    rcases hx with ⟨y, hx1, hx2⟩
    convert g.mem_graph_toLinearPMap hg y using 1
    exact Prod.ext hx1.symm hx2.symm
  rw [LinearPMap.mem_graph_iff]
  have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) := by
    simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
    exact ⟨x_snd, hx⟩
  refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩
  rw [toLinearPMap_apply_aux hg]
  exact (existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx

Graph of Partially Defined Linear Map from Submodule Equals Original Submodule

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. Given a submodule $g$ of $E \times F$ such that for any $(x, y) \in g$ with $x = 0$, we have $y = 0$, the graph of the partially defined linear map $g.\text{toLinearPMap}$ is equal to $g$.

Submodule.toLinearPMap_range theorem

 (g : Submodule R (E × F)) (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
  LinearMap.range g.toLinearPMap.toFun = g.map (LinearMap.snd R E F)

Full source

theorem toLinearPMap_range (g : Submodule R (E × F))
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
    LinearMap.range g.toLinearPMap.toFun = g.map (LinearMap.snd R E F) := by
  rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]

Range of Partially Defined Linear Map from Submodule Equals Second Projection of Submodule

Informal description

Let $R$ be a ring, and let $E$ and $F$ be modules over $R$. Given a submodule $g$ of $E \times F$ such that for any $(x, y) \in g$ with $x = 0$, we have $y = 0$, the range of the partially defined linear map $g.\text{toLinearPMap}$ is equal to the image of $g$ under the second projection map $\text{snd} \colon E \times F \to F$. In other words, for such a submodule $g$, we have: \[ \text{range}(g.\text{toLinearPMap}) = \text{snd}(g). \]

LinearPMap.inverse definition

(f : E →ₗ.[R] F) : F →ₗ.[R] E

Full source

/-- The inverse of a `LinearPMap`. -/
noncomputable def inverse (f : E →ₗ.[R] F) : F →ₗ.[R] E :=
  (f.graph.map (LinearEquiv.prodComm R E F)).toLinearPMap

Inverse of a partially defined linear map

Informal description

The inverse of a partially defined linear map $ f : E \toₗ.[R] F $ is a partially defined linear map $ F \toₗ.[R] E $ whose graph is the image of the graph of $ f $ under the linear equivalence that swaps the components of $ E \times F $. More precisely, the domain of the inverse map is the range of $ f $, and for each $ y $ in this domain, the inverse map sends $ y $ to the unique $ x $ in the domain of $ f $ such that $ f(x) = y $.

LinearPMap.inverse_domain theorem

: (inverse f).domain = LinearMap.range f.toFun

Full source

theorem inverse_domain : (inverse f).domain = LinearMap.range f.toFun := by
  rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
  rfl

Domain of Inverse Equals Range of Partially Defined Linear Map

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ over a ring $R$, the domain of its inverse map $f^{-1} \colon F \to_{.[R]} E$ is equal to the range of $f$, i.e., \[ \text{domain}(f^{-1}) = \text{range}(f). \]

LinearPMap.mem_inverse_graph_snd_eq_zero theorem

(x : F × E) (hv : x ∈ (graph f).map (LinearEquiv.prodComm R E F)) (hv' : x.fst = 0) : x.snd = 0

Full source

/-- The graph of the inverse generates a `LinearPMap`. -/
theorem mem_inverse_graph_snd_eq_zero (x : F × E)
    (hv : x ∈ (graph f).map (LinearEquiv.prodComm R E F))
    (hv' : x.fst = 0) : x.snd = 0 := by
  simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
    LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk] at hv
  rcases hv with ⟨a, b, ⟨ha, h1⟩, ⟨h2, h3⟩⟩
  simp only at hv' ⊢
  rw [hv'] at h1
  rw [LinearMap.ker_eq_bot'] at hf
  specialize hf ⟨a, ha⟩ h1
  simp only [Submodule.mk_eq_zero] at hf
  exact hf

Vanishing of Second Component in Inverse Graph When First Component is Zero

Informal description

Let $f : E \to_{.[R]} F$ be a partially defined linear map between $R$-modules $E$ and $F$. For any element $x = (x_1, x_2) \in F \times E$ in the image of the graph of $f$ under the module isomorphism swapping $E$ and $F$ (i.e., $(x_1, x_2) \in \text{graph}(f).\text{map}(\text{prodComm}_{R,E,F})$), if the first component $x_1$ is zero, then the second component $x_2$ must also be zero.

LinearPMap.inverse_graph theorem

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

Full source

theorem inverse_graph : (inverse f).graph = f.graph.map (LinearEquiv.prodComm R E F) := by
  rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]

Graph of Inverse Partially Defined Linear Map via Component Swap

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ over a ring $R$, the graph of its inverse map $f^{-1} \colon F \to_{.[R]} E$ is equal to the image of the graph of $f$ under the linear equivalence that swaps the components of $E \times F$. In other words, \[ \text{graph}(f^{-1}) = \text{graph}(f).\text{map}(\text{prodComm}_{R,E,F}). \]

LinearPMap.inverse_range theorem

: LinearMap.range (inverse f).toFun = f.domain

Full source

theorem inverse_range : LinearMap.range (inverse f).toFun = f.domain := by
  rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
  rfl

Range of Inverse Partially Defined Linear Map Equals Domain

Informal description

For any partially defined linear map $f \colon E \to_{.[R]} F$ over a ring $R$, the range of its inverse map $f^{-1} \colon F \to_{.[R]} E$ is equal to the domain of $f$. In other words, \[ \text{range}(f^{-1}) = \text{dom}(f). \]

LinearPMap.mem_inverse_graph theorem

(x : f.domain) : (f x, (x : E)) ∈ (inverse f).graph

Full source

theorem mem_inverse_graph (x : f.domain) : (f x, (x : E))(f x, (x : E)) ∈ (inverse f).graph := by
  simp only [inverse_graph hf, Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left,
    exists_eq_left, LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
  exact ⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩

Inclusion of $(f(x), x)$ in the Graph of the Inverse Map

Informal description

For any element $x$ in the domain of a partially defined linear map $f \colon E \to_{.[R]} F$, the pair $(f(x), x)$ belongs to the graph of the inverse map $f^{-1} \colon F \to_{.[R]} E$.

LinearPMap.inverse_apply_eq theorem

{y : (inverse f).domain} {x : f.domain} (hxy : f x = y) : (inverse f) y = x

Full source

theorem inverse_apply_eq {y : (inverse f).domain} {x : f.domain} (hxy : f x = y) :
    (inverse f) y = x := by
  have := mem_inverse_graph hf x
  simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left] at this
  rcases this with ⟨hx, h⟩
  rw [← h]
  congr
  simp only [hxy, Subtype.coe_eta]

Inverse of a Partially Defined Linear Map Evaluates to Preimage

Informal description

Let $f \colon E \to_{.[R]} F$ be a partially defined linear map over a ring $R$. For any $y$ in the domain of the inverse map $f^{-1} \colon F \to_{.[R]} E$ and any $x$ in the domain of $f$ such that $f(x) = y$, the inverse map satisfies $f^{-1}(y) = x$.