Theorems · Theorem · linear algebra

LinearMap.IsPerfPair.restrictScalars_of_field

∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module L M] [inst_6 : Module L N] [inst_7 : Module K M]
  [inst_8 : Module K N] [inst_9 : IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [inst_10 : p.IsPerfPair] {M' : Type u_5}
  {N' : Type u_6} [inst_11 : AddCommGroup M'] [inst_12 : AddCommGroup N'] [inst_13 : Module K M']
  [inst_14 : Module K N'] [inst_15 : IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      p.IsPerfectCompl (Submodule.span L ↑i.range) (Submodule.span L ↑j.range) →
        ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range),
          (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Simultaneously restrict both the domains and scalars of a perfect pairing with coefficients in a field.

Defined in

Mathlib.LinearAlgebra.PerfectPairing.Restrict

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraAddCommGroupAddCommGroupModuleModuleModuleModuleIsScalarTowerLinearMap.IsPerfPairAddCommGroupAddCommGroupModuleModuleIsScalarTower