Documentation

Mathlib.LinearAlgebra.Dual

Dual vector spaces #

The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to R$.

Main definitions #

Main results #

@[reducible, inline]
abbrev Module.Dual (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] :
Type (max uM uR)

The dual space of an R-module M is the R-module of linear maps M → R.

Equations
Instances For
    def Module.dualPairing (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :

    The canonical pairing of a vector space and its algebraic dual.

    Equations
    Instances For
      @[simp]
      theorem Module.dualPairing_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (v : Module.Dual R M) (x : M) :
      ((Module.dualPairing R M) v) x = v x
      Equations

      Maps a module M to the dual of the dual of M. See Module.erange_coe and Module.evalEquiv.

      Equations
      Instances For
        @[simp]
        theorem Module.Dual.eval_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (v : M) (a : Module.Dual R M) :
        ((Module.Dual.eval R M) v) a = a v
        def Module.Dual.transpose {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type uM'} [AddCommMonoid M'] [Module R M'] :

        The transposition of linear maps, as a linear map from M →ₗ[R] M' to Dual R M' →ₗ[R] Dual R M.

        Equations
        Instances For
          theorem Module.Dual.transpose_apply {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type uM'} [AddCommMonoid M'] [Module R M'] (u : M →ₗ[R] M') (l : Module.Dual R M') :
          (Module.Dual.transpose u) l = l ∘ₗ u
          theorem Module.Dual.transpose_comp {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type uM'} [AddCommMonoid M'] [Module R M'] {M'' : Type uM''} [AddCommMonoid M''] [Module R M''] (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') :
          Module.Dual.transpose (u ∘ₗ v) = Module.Dual.transpose v ∘ₗ Module.Dual.transpose u
          @[simp]
          theorem Module.dualProdDualEquivDual_apply_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type uM') [AddCommMonoid M'] [Module R M'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (a : M × M') :
          ((Module.dualProdDualEquivDual R M M') f) a = f.1 a.1 + f.2 a.2
          @[simp]
          theorem Module.dualProdDualEquivDual_symm_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type uM') [AddCommMonoid M'] [Module R M'] (f : M × M' →ₗ[R] R) :
          (Module.dualProdDualEquivDual R M M').symm f = (f ∘ₗ LinearMap.inl R M M', f ∘ₗ LinearMap.inr R M M')
          def Module.dualProdDualEquivDual (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type uM') [AddCommMonoid M'] [Module R M'] :

          Taking duals distributes over products.

          Equations
          Instances For
            @[simp]
            theorem Module.dualProdDualEquivDual_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type uM') [AddCommMonoid M'] [Module R M'] (φ : Module.Dual R M) (ψ : Module.Dual R M') :
            def LinearMap.dualMap {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) :

            Given a linear map f : M₁ →ₗ[R] M₂, f.dualMap is the linear map between the dual of M₂ and M₁ such that it maps the functional φ to φ ∘ f.

            Equations
            • f.dualMap = Module.Dual.transpose f
            Instances For
              theorem LinearMap.dualMap_eq_lcomp {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
              f.dualMap = LinearMap.lcomp R R f
              theorem LinearMap.dualMap_def {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
              f.dualMap = Module.Dual.transpose f
              theorem LinearMap.dualMap_apply' {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂) :
              f.dualMap g = g ∘ₗ f
              @[simp]
              theorem LinearMap.dualMap_apply {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂) (x : M₁) :
              (f.dualMap g) x = g (f x)
              @[simp]
              theorem LinearMap.dualMap_id {R : Type u} [CommSemiring R] {M₁ : Type v} [AddCommMonoid M₁] [Module R M₁] :
              LinearMap.id.dualMap = LinearMap.id
              theorem LinearMap.dualMap_comp_dualMap {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_1} [AddCommGroup M₃] [Module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
              f.dualMap ∘ₗ g.dualMap = (g ∘ₗ f).dualMap
              theorem LinearMap.dualMap_injective_of_surjective {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {f : M₁ →ₗ[R] M₂} (hf : Function.Surjective f) :
              Function.Injective f.dualMap

              If a linear map is surjective, then its dual is injective.

              def LinearEquiv.dualMap {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ ≃ₗ[R] M₂) :

              The Linear_equiv version of LinearMap.dualMap.

              Equations
              • f.dualMap = { toLinearMap := (↑f).dualMap, invFun := (↑f.symm).dualMap, left_inv := , right_inv := }
              Instances For
                @[simp]
                theorem LinearEquiv.dualMap_apply {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ ≃ₗ[R] M₂) (g : Module.Dual R M₂) (x : M₁) :
                (f.dualMap g) x = g (f x)
                @[simp]
                theorem LinearEquiv.dualMap_refl {R : Type u} [CommSemiring R] {M₁ : Type v} [AddCommMonoid M₁] [Module R M₁] :
                (LinearEquiv.refl R M₁).dualMap = LinearEquiv.refl R (Module.Dual R M₁)
                @[simp]
                theorem LinearEquiv.dualMap_symm {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {f : M₁ ≃ₗ[R] M₂} :
                f.dualMap.symm = f.symm.dualMap
                theorem LinearEquiv.dualMap_trans {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_1} [AddCommGroup M₃] [Module R M₃] (f : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₃) :
                g.dualMap ≪≫ₗ f.dualMap = (f ≪≫ₗ g).dualMap
                @[simp]
                theorem Dual.apply_one_mul_eq {R : Type u} [CommSemiring R] (f : Module.Dual R R) (r : R) :
                f 1 * r = f r
                def Basis.toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) :

                The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.

                Equations
                • b.toDual = (b.constr ) fun (v : ι) => (b.constr ) fun (w : ι) => if w = v then 1 else 0
                Instances For
                  theorem Basis.toDual_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) (j : ι) :
                  (b.toDual (b i)) (b j) = if i = j then 1 else 0
                  @[simp]
                  theorem Basis.toDual_linearCombination_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
                  (b.toDual ((Finsupp.linearCombination R b) f)) (b i) = f i
                  @[deprecated Basis.toDual_linearCombination_left]
                  theorem Basis.toDual_total_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
                  (b.toDual ((Finsupp.linearCombination R b) f)) (b i) = f i

                  Alias of Basis.toDual_linearCombination_left.

                  @[simp]
                  theorem Basis.toDual_linearCombination_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
                  (b.toDual (b i)) ((Finsupp.linearCombination R b) f) = f i
                  @[deprecated Basis.toDual_linearCombination_right]
                  theorem Basis.toDual_total_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
                  (b.toDual (b i)) ((Finsupp.linearCombination R b) f) = f i

                  Alias of Basis.toDual_linearCombination_right.

                  theorem Basis.toDual_apply_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) :
                  (b.toDual m) (b i) = (b.repr m) i
                  theorem Basis.toDual_apply_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) (m : M) :
                  (b.toDual (b i)) m = (b.repr m) i
                  theorem Basis.coe_toDual_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) :
                  b.toDual (b i) = b.coord i
                  def Basis.toDualFlip {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) :

                  h.toDual_flip v is the linear map sending w to h.toDual w v.

                  Equations
                  • b.toDualFlip m = b.toDual.flip m
                  Instances For
                    theorem Basis.toDualFlip_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m₁ : M) (m₂ : M) :
                    (b.toDualFlip m₁) m₂ = (b.toDual m₂) m₁
                    theorem Basis.toDual_eq_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) :
                    (b.toDual m) (b i) = (b.repr m) i
                    theorem Basis.toDual_eq_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) (i : ι) :
                    (b.toDual m) (b i) = b.equivFun m i
                    theorem Basis.toDual_injective {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) :
                    Function.Injective b.toDual
                    theorem Basis.toDual_inj {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (a : b.toDual m = 0) :
                    m = 0
                    theorem Basis.toDual_ker {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) :
                    theorem Basis.toDual_range {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
                    @[simp]
                    theorem Basis.sum_dual_apply_smul_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (f : Module.Dual R M) :
                    x : ι, f (b x) b.coord x = f
                    def Basis.toDualEquiv {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :

                    A vector space is linearly equivalent to its dual space.

                    Equations
                    Instances For
                      @[simp]
                      theorem Basis.toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) :
                      b.toDualEquiv m = b.toDual m

                      A vector space over a field is isomorphic to its dual if and only if it is finite-dimensional: a consequence of the Erdős-Kaplansky theorem.

                      def Basis.dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
                      Basis ι R (Module.Dual R M)

                      Maps a basis for V to a basis for the dual space.

                      Equations
                      • b.dualBasis = b.map b.toDualEquiv
                      Instances For
                        theorem Basis.dualBasis_apply_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (j : ι) :
                        (b.dualBasis i) (b j) = if j = i then 1 else 0
                        theorem Basis.linearCombination_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (f : ι →₀ R) (i : ι) :
                        ((Finsupp.linearCombination R b.dualBasis) f) (b i) = f i
                        @[deprecated Basis.linearCombination_dualBasis]
                        theorem Basis.total_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (f : ι →₀ R) (i : ι) :
                        ((Finsupp.linearCombination R b.dualBasis) f) (b i) = f i

                        Alias of Basis.linearCombination_dualBasis.

                        theorem Basis.dualBasis_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) :
                        (b.dualBasis.repr l) i = l (b i)
                        theorem Basis.dualBasis_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (m : M) :
                        (b.dualBasis i) m = (b.repr m) i
                        @[simp]
                        theorem Basis.coe_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
                        b.dualBasis = b.coord
                        @[simp]
                        theorem Basis.toDual_toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
                        b.dualBasis.toDual ∘ₗ b.toDual = Module.Dual.eval R M
                        theorem Basis.dualBasis_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) :
                        b.dualBasis.equivFun l i = l (b i)
                        theorem Basis.eval_ker {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Basis ι R M) :
                        theorem Basis.eval_range {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} [Finite ι] (b : Basis ι R M) :
                        instance Basis.dual_free {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] :
                        Equations
                        • =
                        instance Basis.dual_finite {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] :
                        Equations
                        • =
                        @[simp]
                        theorem Basis.linearCombination_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
                        ((Finsupp.linearCombination R b.coord) f) (b i) = f i

                        simp normal form version of linearCombination_dualBasis

                        @[deprecated Basis.linearCombination_coord]
                        theorem Basis.total_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
                        ((Finsupp.linearCombination R b.coord) f) (b i) = f i

                        Alias of Basis.linearCombination_coord.


                        simp normal form version of linearCombination_dualBasis

                        theorem Basis.dual_rank_eq {K : Type uK} {V : Type uV} {ι : Type uι} [CommRing K] [AddCommGroup V] [Module K V] [Finite ι] (b : Basis ι K V) :
                        theorem Module.eval_apply_eq_zero_iff (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] (v : V) :
                        (Module.Dual.eval K V) v = 0 v = 0
                        theorem Module.forall_dual_apply_eq_zero_iff (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] (v : V) :
                        (∀ (φ : Module.Dual K V), φ v = 0) v = 0
                        Equations
                        • =
                        Equations
                        • =
                        class Module.IsReflexive (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :

                        A reflexive module is one for which the natural map to its double dual is a bijection.

                        Any finitely-generated free module (and thus any finite-dimensional vector space) is reflexive. See Module.IsReflexive.of_finite_of_free.

                        Instances
                          theorem Module.IsReflexive.bijective_dual_eval' {R : Type u_1} {M : Type u_2} :
                          ∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} [self : Module.IsReflexive R M], Function.Bijective (Module.Dual.eval R M)

                          A reflexive module is one for which the natural map to its double dual is a bijection.

                          See also Module.instFiniteDimensionalOfIsReflexive for the converse over a field.

                          Equations
                          • =

                          The bijection between a reflexive module and its double dual, bundled as a LinearEquiv.

                          Equations
                          Instances For
                            @[simp]
                            theorem Module.evalEquiv_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (m : M) :
                            @[simp]
                            theorem Module.apply_evalEquiv_symm_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (f : Module.Dual R M) (g : Module.Dual R (Module.Dual R M)) :
                            f ((Module.evalEquiv R M).symm g) = g f
                            @[simp]
                            theorem Module.symm_dualMap_evalEquiv (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] :
                            (Module.evalEquiv R M).symm.dualMap = Module.Dual.eval R (Module.Dual R M)

                            The dual of a reflexive module is reflexive.

                            Equations
                            • =

                            The isomorphism Module.evalEquiv induces an order isomorphism on subspaces.

                            Equations
                            Instances For
                              @[simp]
                              @[simp]
                              instance Prod.instModuleIsReflexive (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.IsReflexive R M] [Module.IsReflexive R N] :
                              Equations
                              • =
                              theorem Module.equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.IsReflexive R M] (e : M ≃ₗ[R] N) :
                              Equations
                              • =
                              Equations
                              • =
                              theorem Submodule.exists_dual_map_eq_bot_of_nmem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} {x : M} (hx : xp) (hp' : Module.Free R (M p)) :
                              ∃ (f : Module.Dual R M), f x 0 Submodule.map f p =
                              theorem Submodule.exists_dual_map_eq_bot_of_lt_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} (hp : p < ) (hp' : Module.Free R (M p)) :
                              ∃ (f : Module.Dual R M), f 0 Submodule.map f p =
                              theorem Submodule.span_eq_top_of_ne_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] {s : Set (M →ₗ[R] R)} [Module.Free R ((M →ₗ[R] R) Submodule.span R s)] (h : ∀ (z : M), z 0fs, f z 0) :

                              Consider a reflexive module and a set s of linear forms. If for any z ≠ 0 there exists f ∈ s such that f z ≠ 0, then s spans the whole dual space.

                              theorem FiniteDimensional.mem_span_of_iInf_ker_le_ker {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {L : ιE →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜} (h : ⨅ (i : ι), LinearMap.ker (L i) LinearMap.ker K) :
                              theorem mem_span_of_iInf_ker_le_ker {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [Finite ι] {L : ιE →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜} (h : ⨅ (i : ι), LinearMap.ker (L i) LinearMap.ker K) :

                              Given some linear forms $L_1, ..., L_n, K$ over a vector space $E$, if $\bigcap_{i=1}^n \mathrm{ker}(L_i) \subseteq \mathrm{ker}(K)$, then $K$ is in the space generated by $L_1, ..., L_n$.

                              Try using Set.toFinite to dispatch a Set.Finite goal.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                structure Module.DualBases {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : ιM) (ε : ιModule.Dual R M) :

                                e and ε have characteristic properties of a basis and its dual

                                • eval_same : ∀ (i : ι), (ε i) (e i) = 1
                                • eval_of_ne : Pairwise fun (i j : ι) => (ε i) (e j) = 0
                                • total : ∀ {m : M}, (∀ (i : ι), (ε i) m = 0)m = 0
                                • finite : ∀ (m : M), {i : ι | (ε i) m 0}.Finite
                                Instances For
                                  theorem Module.DualBases.eval_same {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (self : Module.DualBases e ε) (i : ι) :
                                  (ε i) (e i) = 1
                                  theorem Module.DualBases.eval_of_ne {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (self : Module.DualBases e ε) :
                                  Pairwise fun (i j : ι) => (ε i) (e j) = 0
                                  theorem Module.DualBases.total {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (self : Module.DualBases e ε) {m : M} :
                                  (∀ (i : ι), (ε i) m = 0)m = 0
                                  theorem Module.DualBases.finite {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (self : Module.DualBases e ε) (m : M) :
                                  {i : ι | (ε i) m 0}.Finite
                                  def Module.DualBases.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (m : M) :
                                  ι →₀ R

                                  The coefficients of v on the basis e

                                  Equations
                                  • h.coeffs m = { support := .toFinset, toFun := fun (i : ι) => (ε i) m, mem_support_toFun := }
                                  Instances For
                                    @[simp]
                                    theorem Module.DualBases.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (m : M) (i : ι) :
                                    (h.coeffs m) i = (ε i) m
                                    def Module.DualBases.lc {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_4} (e : ιM) (l : ι →₀ R) :
                                    M

                                    linear combinations of elements of e. This is a convenient abbreviation for Finsupp.linearCombination R e l

                                    Equations
                                    Instances For
                                      theorem Module.DualBases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (e : ιM) (l : ι →₀ R) :
                                      theorem Module.DualBases.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (l : ι →₀ R) (i : ι) :
                                      (ε i) (Module.DualBases.lc e l) = l i
                                      @[simp]
                                      theorem Module.DualBases.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (l : ι →₀ R) :
                                      h.coeffs (Module.DualBases.lc e l) = l
                                      @[simp]
                                      theorem Module.DualBases.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (m : M) :
                                      Module.DualBases.lc e (h.coeffs m) = m

                                      For any m : M n, \sum_{p ∈ Q n} (ε p m) • e p = m

                                      @[simp]
                                      theorem Module.DualBases.basis_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (m : M) :
                                      h.basis.repr m = h.coeffs m
                                      theorem Module.DualBases.basis_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) (l : ι →₀ R) :
                                      h.basis.repr.symm l = Module.DualBases.lc e l
                                      def Module.DualBases.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) :
                                      Basis ι R M

                                      (h : DualBases e ε).basis shows the family of vectors e forms a basis.

                                      Equations
                                      • h.basis = { repr := { toFun := h.coeffs, map_add' := , map_smul' := , invFun := Module.DualBases.lc e, left_inv := , right_inv := } }
                                      Instances For
                                        @[simp]
                                        theorem Module.DualBases.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) :
                                        h.basis = e
                                        theorem Module.DualBases.mem_of_mem_span {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) {H : Set ι} {x : M} (hmem : x Submodule.span R (e '' H)) (i : ι) :
                                        (ε i) x 0i H
                                        theorem Module.DualBases.coe_dualBasis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιModule.Dual R M} (h : Module.DualBases e ε) [DecidableEq ι] [Finite ι] :
                                        h.basis.dualBasis = ε

                                        The dualRestrict of a submodule W of M is the linear map from the dual of M to the dual of W such that the domain of each linear map is restricted to W.

                                        Equations
                                        Instances For
                                          theorem Submodule.dualRestrict_def {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) :
                                          W.dualRestrict = W.subtype.dualMap
                                          @[simp]
                                          theorem Submodule.dualRestrict_apply {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) (φ : Module.Dual R M) (x : W) :
                                          (W.dualRestrict φ) x = φ x

                                          The dualAnnihilator of a submodule W is the set of linear maps φ such that φ w = 0 for all w ∈ W.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Submodule.mem_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {W : Submodule R M} (φ : Module.Dual R M) :
                                            φ W.dualAnnihilator wW, φ w = 0
                                            theorem Submodule.dualRestrict_ker_eq_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) :
                                            LinearMap.ker W.dualRestrict = W.dualAnnihilator

                                            That $\operatorname{ker}(\iota^* : V^* \to W^*) = \operatorname{ann}(W)$. This is the definition of the dual annihilator of the submodule $W$.

                                            The dualAnnihilator of a submodule of the dual space pulled back along the evaluation map Module.Dual.eval.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Submodule.mem_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {Φ : Submodule R (Module.Dual R M)} (x : M) :
                                              x Φ.dualCoannihilator φΦ, φ x = 0
                                              theorem Submodule.comap_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (Φ : Submodule R (Module.Dual R M)) :
                                              Submodule.comap (Module.Dual.eval R M) Φ.dualAnnihilator = Φ.dualCoannihilator
                                              theorem Submodule.map_dualCoannihilator_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (Φ : Submodule R (Module.Dual R M)) :
                                              Submodule.map (Module.Dual.eval R M) Φ.dualCoannihilator Φ.dualAnnihilator
                                              theorem Submodule.dualAnnihilator_gc (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :
                                              GaloisConnection (OrderDual.toDual Submodule.dualAnnihilator) (Submodule.dualCoannihilator OrderDual.ofDual)
                                              theorem Submodule.le_dualAnnihilator_iff_le_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R (Module.Dual R M)} {V : Submodule R M} :
                                              U V.dualAnnihilator V U.dualCoannihilator
                                              @[simp]
                                              theorem Submodule.dualAnnihilator_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                                              .dualAnnihilator =
                                              @[simp]
                                              theorem Submodule.dualAnnihilator_top {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                                              .dualAnnihilator =
                                              @[simp]
                                              theorem Submodule.dualCoannihilator_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                                              .dualCoannihilator =
                                              theorem Submodule.dualAnnihilator_anti {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R M} {V : Submodule R M} (hUV : U V) :
                                              V.dualAnnihilator U.dualAnnihilator
                                              theorem Submodule.dualCoannihilator_anti {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R (Module.Dual R M)} {V : Submodule R (Module.Dual R M)} (hUV : U V) :
                                              V.dualCoannihilator U.dualCoannihilator
                                              theorem Submodule.le_dualAnnihilator_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) :
                                              U U.dualAnnihilator.dualCoannihilator
                                              theorem Submodule.le_dualCoannihilator_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R (Module.Dual R M)) :
                                              U U.dualCoannihilator.dualAnnihilator
                                              theorem Submodule.dualAnnihilator_dualCoannihilator_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) :
                                              U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator
                                              theorem Submodule.dualCoannihilator_dualAnnihilator_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R (Module.Dual R M)) :
                                              U.dualCoannihilator.dualAnnihilator.dualCoannihilator = U.dualCoannihilator
                                              theorem Submodule.dualAnnihilator_sup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) (V : Submodule R M) :
                                              (U V).dualAnnihilator = U.dualAnnihilator V.dualAnnihilator
                                              theorem Submodule.dualCoannihilator_sup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R (Module.Dual R M)) (V : Submodule R (Module.Dual R M)) :
                                              (U V).dualCoannihilator = U.dualCoannihilator V.dualCoannihilator
                                              theorem Submodule.dualAnnihilator_iSup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_1} (U : ιSubmodule R M) :
                                              (⨆ (i : ι), U i).dualAnnihilator = ⨅ (i : ι), (U i).dualAnnihilator
                                              theorem Submodule.dualCoannihilator_iSup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_1} (U : ιSubmodule R (Module.Dual R M)) :
                                              (⨆ (i : ι), U i).dualCoannihilator = ⨅ (i : ι), (U i).dualCoannihilator
                                              theorem Submodule.sup_dualAnnihilator_le_inf {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) (V : Submodule R M) :
                                              U.dualAnnihilator V.dualAnnihilator (U V).dualAnnihilator

                                              See also Subspace.dualAnnihilator_inf_eq for vector subspaces.

                                              theorem Submodule.iSup_dualAnnihilator_le_iInf {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_1} (U : ιSubmodule R M) :
                                              ⨆ (i : ι), (U i).dualAnnihilator (⨅ (i : ι), U i).dualAnnihilator

                                              See also Subspace.dualAnnihilator_iInf_eq for vector subspaces when ι is finite.

                                              @[simp]
                                              theorem Subspace.dualAnnihilator_dualCoannihilator_eq {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} :
                                              (Submodule.dualAnnihilator W).dualCoannihilator = W
                                              theorem Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) (v : V) :
                                              (∀ φSubmodule.dualAnnihilator W, φ v = 0) v W
                                              def Subspace.dualAnnihilatorGci (K : Type u_1) (V : Type u_2) [Field K] [AddCommGroup V] [Module K V] :
                                              GaloisCoinsertion (OrderDual.toDual Submodule.dualAnnihilator) (Submodule.dualCoannihilator OrderDual.ofDual)

                                              Submodule.dualAnnihilator and Submodule.dualCoannihilator form a Galois coinsertion.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                noncomputable def Subspace.dualLift {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

                                                Given a subspace W of V and an element of its dual φ, dualLift W φ is an arbitrary extension of φ to an element of the dual of V. That is, dualLift W φ sends w ∈ W to φ x and x in a chosen complement of W to 0.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Subspace.dualLift_of_subtype {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} {φ : Module.Dual K W} (w : W) :
                                                  (W.dualLift φ) w = φ w
                                                  theorem Subspace.dualLift_of_mem {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} {φ : Module.Dual K W} {w : V} (hw : w W) :
                                                  (W.dualLift φ) w = φ w, hw
                                                  @[simp]
                                                  theorem Subspace.dualRestrict_comp_dualLift {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :
                                                  Submodule.dualRestrict W ∘ₗ W.dualLift = 1
                                                  theorem Subspace.dualLift_injective {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} :
                                                  Function.Injective W.dualLift
                                                  noncomputable def Subspace.quotAnnihilatorEquiv {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

                                                  The quotient by the dualAnnihilator of a subspace is isomorphic to the dual of that subspace.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem Subspace.quotAnnihilatorEquiv_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) (φ : Module.Dual K V) :
                                                    W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (Submodule.dualRestrict W) φ
                                                    noncomputable def Subspace.dualEquivDual {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :
                                                    Module.Dual K W ≃ₗ[K] (LinearMap.range W.dualLift)

                                                    The natural isomorphism from the dual of a subspace W to W.dualLift.range.

                                                    Equations
                                                    Instances For
                                                      theorem Subspace.dualEquivDual_def {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :
                                                      W.dualEquivDual = W.dualLift.rangeRestrict
                                                      @[simp]
                                                      theorem Subspace.dualEquivDual_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} (φ : Module.Dual K W) :
                                                      W.dualEquivDual φ = W.dualLift φ,
                                                      @[simp]
                                                      noncomputable def Subspace.quotDualEquivAnnihilator {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) :

                                                      The quotient by the dual is isomorphic to its dual annihilator.

                                                      Equations
                                                      Instances For
                                                        noncomputable def Subspace.quotEquivAnnihilator {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) :

                                                        The quotient by a subspace is isomorphic to its dual annihilator.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem LinearMap.ker_dualMap_eq_dualAnnihilator_range {R : Type uR} [CommSemiring R] {M₁ : Type uM₁} {M₂ : Type uM₂} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
                                                          LinearMap.ker f.dualMap = (LinearMap.range f).dualAnnihilator
                                                          theorem LinearMap.range_dualMap_le_dualAnnihilator_ker {R : Type uR} [CommSemiring R] {M₁ : Type uM₁} {M₂ : Type uM₂} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
                                                          LinearMap.range f.dualMap (LinearMap.ker f).dualAnnihilator
                                                          def Submodule.dualCopairing {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) :
                                                          W.dualAnnihilator →ₗ[R] M W →ₗ[R] R

                                                          Given a submodule, corestrict to the pairing on M ⧸ W by simultaneously restricting to W.dualAnnihilator.

                                                          See Subspace.dualCopairing_nondegenerate.

                                                          Equations
                                                          • W.dualCopairing = (W.liftQ ((Module.dualPairing R M).domRestrict W.dualAnnihilator).flip ).flip
                                                          Instances For
                                                            instance Submodule.instFunLikeSubtypeDualMemDualAnnihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) :
                                                            FunLike (↥W.dualAnnihilator) M R
                                                            Equations
                                                            • W.instFunLikeSubtypeDualMemDualAnnihilator = { coe := fun (φ : W.dualAnnihilator) => φ, coe_injective' := }
                                                            @[simp]
                                                            theorem Submodule.dualCopairing_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} (φ : W.dualAnnihilator) (x : M) :
                                                            (W.dualCopairing φ) (Submodule.Quotient.mk x) = φ x
                                                            def Submodule.dualPairing {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) :
                                                            Module.Dual R M W.dualAnnihilator →ₗ[R] W →ₗ[R] R

                                                            Given a submodule, restrict to the pairing on W by simultaneously corestricting to Module.Dual R M ⧸ W.dualAnnihilator. This is Submodule.dualRestrict factored through the quotient by its kernel (which is W.dualAnnihilator by definition).

                                                            See Subspace.dualPairing_nondegenerate.

                                                            Equations
                                                            • W.dualPairing = W.dualAnnihilator.liftQ W.dualRestrict
                                                            Instances For
                                                              @[simp]
                                                              theorem Submodule.dualPairing_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} (φ : Module.Dual R M) (x : W) :
                                                              (W.dualPairing (Submodule.Quotient.mk φ)) x = φ x
                                                              theorem Submodule.range_dualMap_mkQ_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) :
                                                              LinearMap.range W.mkQ.dualMap = W.dualAnnihilator

                                                              That $\operatorname{im}(q^* : (V/W)^* \to V^*) = \operatorname{ann}(W)$.

                                                              def Submodule.dualQuotEquivDualAnnihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) :
                                                              Module.Dual R (M W) ≃ₗ[R] W.dualAnnihilator

                                                              Equivalence $(M/W)^* \cong \operatorname{ann}(W)$. That is, there is a one-to-one correspondence between the dual of M ⧸ W and those elements of the dual of M that vanish on W.

                                                              The inverse of this is Submodule.dualCopairing.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem Submodule.dualQuotEquivDualAnnihilator_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) (φ : Module.Dual R (M W)) (x : M) :
                                                                (W.dualQuotEquivDualAnnihilator φ) x = φ (Submodule.Quotient.mk x)
                                                                theorem Submodule.dualCopairing_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) :
                                                                W.dualCopairing = W.dualQuotEquivDualAnnihilator.symm
                                                                @[simp]
                                                                theorem Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) (φ : W.dualAnnihilator) (x : M) :
                                                                (W.dualQuotEquivDualAnnihilator.symm φ) (Submodule.Quotient.mk x) = φ x
                                                                theorem Submodule.finite_dualAnnihilator_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} [Module.Free R (M W)] :
                                                                Module.Finite R W.dualAnnihilator Module.Finite R (M W)
                                                                def Submodule.quotDualCoannihilatorToDual {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) :
                                                                M W.dualCoannihilator →ₗ[R] Module.Dual R W

                                                                The pairing between a submodule W of a dual module Dual R M and the quotient of M by the coannihilator of W, which is always nondegenerate.

                                                                Equations
                                                                • W.quotDualCoannihilatorToDual = W.dualCoannihilator.liftQ W.subtype.flip
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Submodule.quotDualCoannihilatorToDual_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) (m : M) (w : W) :
                                                                  (W.quotDualCoannihilatorToDual (Submodule.Quotient.mk m)) w = w m
                                                                  theorem Submodule.quotDualCoannihilatorToDual_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) :
                                                                  Function.Injective W.quotDualCoannihilatorToDual
                                                                  theorem Submodule.flip_quotDualCoannihilatorToDual_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) :
                                                                  Function.Injective W.quotDualCoannihilatorToDual.flip
                                                                  theorem Submodule.quotDualCoannihilatorToDual_nondegenerate {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) :
                                                                  W.quotDualCoannihilatorToDual.Nondegenerate
                                                                  theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Surjective f) :
                                                                  LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator
                                                                  theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Surjective (LinearMap.range f).subtype.dualMap) :
                                                                  LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator
                                                                  theorem LinearMap.ker_dualMap_eq_dualCoannihilator_range {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') :
                                                                  LinearMap.ker f.dualMap = (LinearMap.range (Module.Dual.eval R M' ∘ₗ f)).dualCoannihilator
                                                                  @[simp]
                                                                  theorem LinearMap.dualCoannihilator_range_eq_ker_flip {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (B : M →ₗ[R] M' →ₗ[R] R) :
                                                                  (LinearMap.range B).dualCoannihilator = LinearMap.ker B.flip
                                                                  theorem Module.Dual.range_eq_top_of_ne_zero {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] {f : Module.Dual K V₁} (hf : f 0) :
                                                                  theorem Module.Dual.finrank_ker_add_one_of_ne_zero {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] {f : Module.Dual K V₁} (hf : f 0) [FiniteDimensional K V₁] :
                                                                  theorem Module.Dual.isCompl_ker_of_disjoint_of_ne_bot {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] {f : Module.Dual K V₁} (hf : f 0) [FiniteDimensional K V₁] {p : Submodule K V₁} (hpf : Disjoint (LinearMap.ker f) p) (hp : p ) :
                                                                  theorem Module.Dual.eq_of_ker_eq_of_apply_eq {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] {f : Module.Dual K V₁} {g : Module.Dual K V₁} (x : V₁) (h : LinearMap.ker f = LinearMap.ker g) (h' : f x = g x) (hx : f x 0) :
                                                                  f = g
                                                                  theorem LinearMap.dualPairing_nondegenerate {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] :
                                                                  (Module.dualPairing K V₁).Nondegenerate
                                                                  theorem LinearMap.dualMap_surjective_of_injective {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} (hf : Function.Injective f) :
                                                                  Function.Surjective f.dualMap
                                                                  theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] (f : V₁ →ₗ[K] V₂) :
                                                                  LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator
                                                                  @[simp]
                                                                  theorem LinearMap.dualMap_surjective_iff {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} :

                                                                  For vector spaces, f.dualMap is surjective if and only if f is injective

                                                                  theorem Subspace.dualPairing_eq {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] (W : Subspace K V₁) :
                                                                  Submodule.dualPairing W = W.quotAnnihilatorEquiv
                                                                  theorem Subspace.dualPairing_nondegenerate {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] (W : Subspace K V₁) :
                                                                  (Submodule.dualPairing W).Nondegenerate
                                                                  theorem Subspace.dualCopairing_nondegenerate {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] (W : Subspace K V₁) :
                                                                  (Submodule.dualCopairing W).Nondegenerate
                                                                  theorem Subspace.dualAnnihilator_iInf_eq {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] {ι : Type u_1} [Finite ι] (W : ιSubspace K V₁) :
                                                                  Submodule.dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), Submodule.dualAnnihilator (W i)
                                                                  theorem Subspace.isCompl_dualAnnihilator {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] {W : Subspace K V₁} {W' : Subspace K V₁} (h : IsCompl W W') :

                                                                  For vector spaces, dual annihilators carry direct sum decompositions to direct sum decompositions.

                                                                  def Subspace.dualQuotDistrib {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] (W : Subspace K V₁) :
                                                                  Module.Dual K (V₁ W) ≃ₗ[K] Module.Dual K V₁ LinearMap.range W.dualLift

                                                                  For finite-dimensional vector spaces, one can distribute duals over quotients by identifying W.dualLift.range with W. Note that this depends on a choice of splitting of V₁.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem LinearMap.finrank_range_dualMap_eq_finrank_range {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] (f : V₁ →ₗ[K] V₂) :
                                                                    @[simp]
                                                                    theorem LinearMap.dualMap_injective_iff {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} :

                                                                    f.dualMap is injective if and only if f is surjective

                                                                    @[simp]
                                                                    theorem LinearMap.dualMap_bijective_iff {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} :

                                                                    f.dualMap is bijective if and only if f is

                                                                    @[simp]
                                                                    theorem LinearMap.dualAnnihilator_ker_eq_range_flip {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [Module.IsReflexive K V₂] :
                                                                    (LinearMap.ker B).dualAnnihilator = LinearMap.range B.flip
                                                                    theorem LinearMap.flip_injective_iff₁ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] :
                                                                    theorem LinearMap.flip_injective_iff₂ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] :
                                                                    theorem LinearMap.flip_surjective_iff₁ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] :
                                                                    theorem LinearMap.flip_surjective_iff₂ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] :
                                                                    theorem LinearMap.flip_bijective_iff₁ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] :
                                                                    theorem LinearMap.flip_bijective_iff₂ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] :
                                                                    theorem Subspace.dualCoannihilator_dualAnnihilator_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K (Module.Dual K V)} [FiniteDimensional K W] :
                                                                    (Submodule.dualCoannihilator W).dualAnnihilator = W
                                                                    theorem Subspace.finiteDimensional_quot_dualCoannihilator_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K (Module.Dual K V)} :
                                                                    FiniteDimensional K (V W.dualCoannihilator) FiniteDimensional K W
                                                                    def Subspace.orderIsoFiniteCodimDim {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] :
                                                                    { W : Subspace K V // FiniteDimensional K (V W) } ≃o { W : Subspace K (Module.Dual K V) // FiniteDimensional K W }ᵒᵈ

                                                                    For any vector space, dualAnnihilator and dualCoannihilator gives an antitone order isomorphism between the finite-codimensional subspaces in the vector space and the finite-dimensional subspaces in its dual.

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

                                                                      For any finite-dimensional vector space, dualAnnihilator and dualCoannihilator give an antitone order isomorphism between the subspaces in the vector space and the subspaces in its dual.

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

                                                                        The canonical linear map from Dual M ⊗ Dual N to Dual (M ⊗ N), sending f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem TensorProduct.dualDistrib_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (g : Module.Dual R N) (m : M) (n : N) :
                                                                          ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = f m * g n
                                                                          @[simp]
                                                                          theorem TensorProduct.AlgebraTensorModule.dualDistrib_apply {R : Type u_1} (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] (f : Module.Dual A M) (g : Module.Dual R N) (m : M) (n : N) :
                                                                          noncomputable def TensorProduct.dualDistribInvOfBasis {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :

                                                                          An inverse to TensorProduct.dualDistrib given bases.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem TensorProduct.dualDistribInvOfBasis_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (f : Module.Dual R (TensorProduct R M N)) :
                                                                            (TensorProduct.dualDistribInvOfBasis b c) f = i : ι, j : κ, f (b i ⊗ₜ[R] c j) b.dualBasis i ⊗ₜ[R] c.dualBasis j
                                                                            theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
                                                                            theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
                                                                            @[simp]
                                                                            theorem TensorProduct.dualDistribEquivOfBasis_apply_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
                                                                            ∀ (a : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (a_1 : TensorProduct R M N), ((TensorProduct.dualDistribEquivOfBasis b c) a) a_1 = (TensorProduct.lid R R) (((TensorProduct.homTensorHomMap R M N R R) a) a_1)
                                                                            @[simp]
                                                                            theorem TensorProduct.dualDistribEquivOfBasis_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (a : Module.Dual R (TensorProduct R M N)) :
                                                                            (TensorProduct.dualDistribEquivOfBasis b c).symm a = x : ι, x_1 : κ, a (b x ⊗ₜ[R] c x_1) b.coord x ⊗ₜ[R] c.coord x_1
                                                                            noncomputable def TensorProduct.dualDistribEquivOfBasis {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :

                                                                            A linear equivalence between Dual M ⊗ Dual N and Dual (M ⊗ N) given bases for M and N. It sends f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

                                                                            Equations
                                                                            Instances For
                                                                              noncomputable def TensorProduct.dualDistribEquiv (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Free R M] [Module.Free R N] :

                                                                              A linear equivalence between Dual M ⊗ Dual N and Dual (M ⊗ N) when M and N are finite free modules. It sends f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

                                                                              Equations
                                                                              Instances For