Theorems · Theorem · linear algebra

LinearMap.IsPerfPair.restrictScalars

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] {S : Type u_4}
  {M' : Type u_5} {N' : Type u_6} [inst_6 : CommRing S] [inst_7 : IsDomain S] [inst_8 : Algebra S R]
  [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : IsScalarTower S R M] [inst_12 : IsScalarTower S R N]
  [inst_13 : Module.IsTorsionFree S R] [inst_14 : Nontrivial R] [inst_15 : AddCommGroup M'] [inst_16 : Module S M']
  [inst_17 : AddCommGroup N'] [inst_18 : Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      Submodule.span R ↑i.range = ⊤ →
        Submodule.span R ↑j.range = ⊤ →
          (∀ (g : Module.Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) →
            (∀ (g : Module.Dual S M'), ∃ n, ↑S (p.flip.toPerfPair (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) →
              ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range),
                (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).IsPerfPair

Restricting a perfect pairing to a subring of the scalars results in a perfect pairing.

Defined in

Mathlib.LinearAlgebra.PerfectPairing.Restrict

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleLinearMap.IsPerfPairCommRingIsDomainAlgebraModuleModuleIsScalarTowerIsScalarTowerModule.IsTorsionFreeNontrivialAddCommGroupModuleAddCommGroupModule