Documentation

Mathlib.LinearAlgebra.LinearPMap

Partially defined linear maps #

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

Moreover, we define

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

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

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

Instances For

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

    Equations
      Instances For
        def LinearPMap.toFun' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :
        f.domainF
        Equations
          Instances For
            instance LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
            CoeFun (E →ₗ.[R] F) fun (f : E →ₗ.[R] F) => f.domainF
            Equations
              @[simp]
              theorem LinearPMap.toFun_eq_coe {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x : f.domain) :
              f.toFun x = f x
              theorem LinearPMap.ext {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : E⦄ ⦃hf : x f.domain⦄ ⦃hg : x g.domain⦄, f x, hf = g x, hg) :
              f = g
              theorem LinearPMap.dExt {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} (h : f.domain = g.domain) (h' : ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄, x = yf x = g y) :
              f = g

              A dependent version of ext.

              @[simp]
              theorem LinearPMap.map_zero {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :
              f 0 = 0
              theorem LinearPMap.ext_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} :
              f = g f.domain = g.domain ∀ ⦃x : E⦄ ⦃hf : x f.domain⦄ ⦃hg : x g.domain⦄, f x, hf = g x, hg
              theorem LinearPMap.dExt_iff {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} :
              f = g ∃ (_ : f.domain = g.domain), ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄, x = yf x = g y
              theorem LinearPMap.ext' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {s : Submodule R E} {f g : s →ₗ[R] F} (h : f = g) :
              { domain := s, toFun := f } = { domain := s, toFun := g }
              theorem LinearPMap.map_add {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x y : f.domain) :
              f (x + y) = f x + f y
              theorem LinearPMap.map_neg {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x : f.domain) :
              f (-x) = -f x
              theorem LinearPMap.map_sub {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (x y : f.domain) :
              f (x - y) = f x - f y
              theorem LinearPMap.map_smul {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) (c : R) (x : f.domain) :
              f (c x) = c f x
              @[simp]
              theorem LinearPMap.mk_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (f : p →ₗ[R] F) (x : p) :
              { domain := p, toFun := f } x = f x
              noncomputable def LinearPMap.mkSpanSingleton' {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) :

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

              Equations
                Instances For
                  @[simp]
                  theorem LinearPMap.domain_mkSpanSingleton {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) :
                  @[simp]
                  theorem LinearPMap.mkSpanSingleton'_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) (c : R) (h : c x (mkSpanSingleton' x y H).domain) :
                  (mkSpanSingleton' x y H) c x, h = c y
                  @[simp]
                  theorem LinearPMap.mkSpanSingleton'_apply_self {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) (h : x (mkSpanSingleton' x y H).domain) :
                  (mkSpanSingleton' x y H) x, h = y
                  @[reducible, inline]
                  noncomputable abbrev LinearPMap.mkSpanSingleton {K : Type u_5} {E : Type u_6} {F : Type u_7} [DivisionRing K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] (x : E) (y : F) (hx : x 0) :

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

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

                      Projection to the first coordinate as a LinearPMap

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

                          Projection to the second coordinate as a LinearPMap

                          Equations
                            Instances For
                              @[simp]
                              theorem LinearPMap.snd_apply {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R F) (x : (p.prod p')) :
                              (LinearPMap.snd p p') x = (↑x).2
                              instance LinearPMap.le {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
                              LE (E →ₗ.[R] F)
                              Equations
                                theorem LinearPMap.apply_comp_inclusion {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {T S : E →ₗ.[R] F} (h : T S) (x : T.domain) :
                                T x = S ((Submodule.inclusion ) x)
                                theorem LinearPMap.exists_of_le {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {T S : E →ₗ.[R] F} (h : T S) (x : T.domain) :
                                ∃ (y : S.domain), x = y T x = S y
                                theorem LinearPMap.eq_of_le_of_domain_eq {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} (hle : f g) (heq : f.domain = g.domain) :
                                f = g
                                def LinearPMap.eqLocus {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) :

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

                                Equations
                                  Instances For
                                    instance LinearPMap.bot {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
                                    Bot (E →ₗ.[R] F)
                                    Equations
                                      instance LinearPMap.inhabited {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
                                      Equations
                                        instance LinearPMap.semilatticeInf {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
                                        Equations
                                          instance LinearPMap.orderBot {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
                                          Equations
                                            theorem LinearPMap.le_of_eqLocus_ge {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f g : E →ₗ.[R] F} (H : f.domain f.eqLocus g) :
                                            f g
                                            theorem LinearPMap.domain_mono {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] :
                                            noncomputable def LinearPMap.sup {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), x = yf x = g y) :

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

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

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

                                                Algebraic operations #

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

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

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

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

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

                                                                                        Compose a linear map with a LinearPMap

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

                                                                                            Restrict codomain of a LinearPMap

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

                                                                                                Compose two LinearPMaps

                                                                                                Equations
                                                                                                  Instances For
                                                                                                    def LinearPMap.coprod {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {G : Type u_4} [AddCommGroup G] [Module R G] (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) :
                                                                                                    E × F →ₗ.[R] G

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

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

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

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

                                                                                                            Graph #

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

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

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

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

                                                                                                                theorem LinearPMap.graph_map_fst_eq_domain {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) :
                                                                                                                theorem LinearPMap.smul_graph {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] (f : E →ₗ.[R] F) (z : M) :

                                                                                                                The graph of z • f as a pushforward.

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

                                                                                                                The graph of -f as a pushforward.

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

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

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

                                                                                                                Auxiliary definition to unfold the existential quantifier.

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

                                                                                                                    Define a LinearMap from its graph.

                                                                                                                    Helper definition for LinearPMap.

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

                                                                                                                        Define a LinearPMap from its graph.

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

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

                                                                                                                            The inverse of a LinearPMap.

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

                                                                                                                                The graph of the inverse generates a LinearPMap.

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