Documentation

Mathlib.LinearAlgebra.PerfectPairing

Perfect pairings of modules #

A perfect pairing of two (left) modules may be defined either as:

  1. A bilinear map M × N → R such that the induced maps M → Dual R N and N → Dual R M are both bijective. It follows from this that both M and N are reflexive modules.
  2. A linear equivalence N ≃ Dual R M for which M is reflexive. (It then follows that N is reflexive.)

In this file we provide a PerfectPairing definition corresponding to 1 above, together with logic to connect 1 and 2.

Main definitions #

structure PerfectPairing (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :
Type (max (max u_1 u_2) u_3)

A perfect pairing of two (left) modules over a commutative ring.

Instances For
    def PerfectPairing.mkOfInjective {K : Type u_4} {V : Type u_5} {W : Type u_6} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K V] (B : V →ₗ[K] W →ₗ[K] K) (h : Function.Injective B) (h' : Function.Injective B.flip) :

    If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient to check only injectivity instead of bijectivity of the bilinear form.

    Equations
    Instances For
      def PerfectPairing.mkOfInjective' {K : Type u_4} {V : Type u_5} {W : Type u_6} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] (B : V →ₗ[K] W →ₗ[K] K) (h : Function.Injective B) (h' : Function.Injective B.flip) :

      If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient to check only injectivity instead of bijectivity of the bilinear form.

      Equations
      Instances For
        instance PerfectPairing.instFunLike {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :
        Equations
        • PerfectPairing.instFunLike = { coe := fun (f : PerfectPairing R M N) => f.toLin, coe_injective' := }
        @[simp]
        theorem PerfectPairing.toLin_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) {x : M} :
        p.toLin x = p x
        def PerfectPairing.flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :

        Given a perfect pairing between M and N, we may interchange the roles of M and N.

        Equations
        • p.flip = { toLin := p.toLin.flip, bijectiveLeft := , bijectiveRight := }
        Instances For
          @[simp]
          theorem PerfectPairing.flip_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) {x : M} {y : N} :
          (p.flip y) x = (p x) y
          @[simp]
          theorem PerfectPairing.flip_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :
          p.flip.flip = p
          def PerfectPairing.toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :

          The linear equivalence from M to Dual R N induced by a perfect pairing.

          Equations
          Instances For
            @[simp]
            theorem PerfectPairing.toDualLeft_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (a : M) :
            p.toDualLeft a = p a
            @[simp]
            theorem PerfectPairing.apply_toDualLeft_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (f : Module.Dual R N) (x : N) :
            (p (p.toDualLeft.symm f)) x = f x
            def PerfectPairing.toDualRight {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :

            The linear equivalence from N to Dual R M induced by a perfect pairing.

            Equations
            • p.toDualRight = p.flip.toDualLeft
            Instances For
              @[simp]
              theorem PerfectPairing.toDualRight_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (a : N) :
              p.toDualRight a = p.flip a
              @[simp]
              theorem PerfectPairing.apply_apply_toDualRight_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (x : M) (f : Module.Dual R M) :
              (p x) (p.toDualRight.symm f) = f x
              theorem PerfectPairing.toDualLeft_of_toDualRight_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (x : M) (f : Module.Dual R M) :
              (p.toDualLeft x) (p.toDualRight.symm f) = f x
              theorem PerfectPairing.toDualRight_symm_toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (x : M) :
              p.toDualRight.symm.dualMap (p.toDualLeft x) = (Module.Dual.eval R M) x
              theorem PerfectPairing.toDualRight_symm_comp_toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :
              p.toDualRight.symm.dualMap ∘ₗ p.toDualLeft = Module.Dual.eval R M
              theorem PerfectPairing.bijective_toDualRight_symm_toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :
              Function.Bijective fun (x : M) => p.toDualRight.symm.dualMap (p.toDualLeft x)
              theorem PerfectPairing.reflexive_left {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :
              theorem PerfectPairing.reflexive_right {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :
              instance PerfectPairing.instEquivLikeDual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem PerfectPairing.finrank_eq {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) [Module.Finite R M] [Module.Free R M] :
              def PerfectPairing.restrict {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) {M' : Type u_4} {N' : Type u_5} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] (i : M' →ₗ[R] M) (j : N' →ₗ[R] N) (hM : IsCompl (LinearMap.range i) (Submodule.map p.toDualLeft.symm (LinearMap.range j).dualAnnihilator)) (hN : IsCompl (LinearMap.range j) (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator)) (hi : Function.Injective i) (hj : Function.Injective j) :

              The restriction of a perfect pairing to submodules (expressed as injections to provide definitional control).

              Equations
              • p.restrict i j hM hN hi hj = { toLin := p.toLin.compl₁₂ i j, bijectiveLeft := , bijectiveRight := }
              Instances For
                @[simp]
                theorem PerfectPairing.restrict_toLin {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) {M' : Type u_4} {N' : Type u_5} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] (i : M' →ₗ[R] M) (j : N' →ₗ[R] N) (hM : IsCompl (LinearMap.range i) (Submodule.map p.toDualLeft.symm (LinearMap.range j).dualAnnihilator)) (hN : IsCompl (LinearMap.range j) (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator)) (hi : Function.Injective i) (hj : Function.Injective j) :
                (p.restrict i j hM hN hi hj).toLin = p.toLin.compl₁₂ i j
                theorem PerfectPairing.exists_basis_basis_of_span_eq_top_of_mem_algebraMap {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] (p : PerfectPairing L M N) (M' : Submodule K M) (N' : Submodule K N) (hM : Submodule.span L M' = ) (hN : Submodule.span L N' = ) (hp : xM', yN', (p x) y (algebraMap K L).range) :
                ∃ (n : ) (b : Basis (Fin n) L M) (b' : Basis (Fin n) K M'), ∀ (i : Fin n), b i = (b' i)

                If a perfect pairing over a field L takes values in a subfield K along two K-subspaces whose L span is full, then these subspaces induce a K-structure in the sense of Algebra I, Bourbaki : Chapter II, §8.1 Definition 1.

                def PerfectPairing.restrictScalars {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) {S : Type u_4} [CommRing S] [Algebra S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N] [NoZeroSMulDivisors S R] [Nontrivial R] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [Module S M'] [AddCommGroup N'] [Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (hi : Function.Injective i) (hj : Function.Injective j) (hM : Submodule.span R (LinearMap.range i) = ) (hN : Submodule.span R (LinearMap.range j) = ) (h₁ : ∀ (g : Module.Dual S N'), ∃ (m : M'), S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) (h₂ : ∀ (g : Module.Dual S M'), ∃ (n : N'), S (p.toDualRight (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) (algebraMap S R).range) :

                Restriction of scalars for a perfect pairing taking values in a subring.

                Equations
                Instances For
                  def PerfectPairing.restrictScalarsField {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [AddCommGroup N'] {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N] [Module K M'] [Module K N'] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N) (hi : Function.Injective i) (hj : Function.Injective j) (hM : Submodule.span L (LinearMap.range i) = ) (hN : Submodule.span L (LinearMap.range j) = ) (p : PerfectPairing L M N) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) (algebraMap K L).range) :

                  Restriction of scalars for a perfect pairing taking values in a subfield.

                  Equations
                  Instances For

                    A reflexive module has a perfect pairing with its dual.

                    Equations
                    • IsReflexive.toPerfectPairingDual = { toLin := LinearMap.id, bijectiveLeft := , bijectiveRight := }
                    Instances For
                      @[simp]
                      theorem IsReflexive.toPerfectPairingDual_toLin {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] :
                      IsReflexive.toPerfectPairingDual.toLin = LinearMap.id
                      @[simp]
                      theorem IsReflexive.toPerfectPairingDual_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} {x : M} :
                      (IsReflexive.toPerfectPairingDual f) x = f x
                      def LinearEquiv.flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) :

                      For a reflexive module M, an equivalence N ≃ₗ[R] Dual R M naturally yields an equivalence M ≃ₗ[R] Dual R N. Such equivalences are known as perfect pairings.

                      Equations
                      Instances For
                        @[simp]
                        theorem LinearEquiv.coe_toLinearMap_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) :
                        e.flip = (↑e).flip
                        @[simp]
                        theorem LinearEquiv.flip_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (m : M) (n : N) :
                        (e.flip m) n = (e n) m
                        theorem LinearEquiv.symm_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) :
                        e.flip.symm = e.symm.dualMap ≪≫ₗ (Module.evalEquiv R M).symm
                        theorem LinearEquiv.trans_dualMap_symm_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) :
                        (e ≪≫ₗ e.flip.symm.dualMap) = Module.Dual.eval R N

                        If N is in perfect pairing with M, then it is reflexive.

                        @[simp]
                        theorem LinearEquiv.flip_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (h : Module.IsReflexive R N := ) :
                        e.flip.flip = e
                        def LinearEquiv.toPerfectPairing {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) :

                        If M is reflexive then a linear equivalence N ≃ Dual R M is a perfect pairing.

                        Equations
                        • e.toPerfectPairing = { toLin := e, bijectiveLeft := , bijectiveRight := }
                        Instances For
                          @[simp]
                          theorem LinearEquiv.toPerfectPairing_toLin {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) :
                          e.toPerfectPairing.toLin = e
                          def PerfectPairing.dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) :

                          A perfect pairing induces a perfect pairing between dual spaces.

                          Equations
                          Instances For
                            @[simp]
                            theorem Submodule.dualCoannihilator_map_linearEquiv_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R M) :
                            (Submodule.map e.flip p).dualCoannihilator = Submodule.map e.symm p.dualAnnihilator
                            @[simp]
                            theorem Submodule.map_dualAnnihilator_linearEquiv_flip_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R N) :
                            Submodule.map e.flip.symm p.dualAnnihilator = (Submodule.map e p).dualCoannihilator
                            @[simp]
                            theorem Submodule.map_dualCoannihilator_linearEquiv_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R (Module.Dual R M)) :
                            Submodule.map e.flip p.dualCoannihilator = (Submodule.map e.symm p).dualAnnihilator
                            @[simp]
                            theorem Submodule.dualAnnihilator_map_linearEquiv_flip_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R (Module.Dual R N)) :
                            (Submodule.map e.flip.symm p).dualAnnihilator = Submodule.map e p.dualCoannihilator