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
    theorem PerfectPairing.bijectiveLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (self : PerfectPairing R M N) :
    Function.Bijective self.toLin
    theorem PerfectPairing.bijectiveRight {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (self : PerfectPairing R M N) :
    Function.Bijective self.toLin.flip
    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
      noncomputable 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
        noncomputable 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) :
          @[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

          A reflexive module has a perfect pairing with its dual.

          Equations
          • IsReflexive.toPerfectPairingDual = { toLin := LinearMap.id, bijectiveLeft := , bijectiveRight := }
          Instances For
            @[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
            noncomputable 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 : optParam (Module.IsReflexive R N) ) :
              e.flip.flip = e
              @[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
              noncomputable 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 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