Documentation

Mathlib.LinearAlgebra.Quotient.Bilinear

Lifting bilinear forms to quotients #

source
def LinearMap.liftQ₂ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [Ring R] [Ring R₂] [Ring S] [Ring S₂] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass R₂ S₂ P] {ρ : R →+* R₂} {σ : S →+* S₂} (M' : Submodule R M) (N' : Submodule S N) (f : M →ₛₗ[ρ] N →ₛₗ[σ] P) (hM' : M' ≤ f.ker) (hN' : N' ≤ f.flip.ker) :
M ⧸ M' →ₛₗ[ρ] N ⧸ N' →ₛₗ[σ] P

Lift a bilinear form from M × N → P to (M ⧸ M') × (N ⧸ N') → P.

Equations
Instances For
    source
    @[simp]
    theorem LinearMap.liftQ₂_mk {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [Ring R] [Ring R₂] [Ring S] [Ring S₂] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass R₂ S₂ P] {ρ : R →+* R₂} {σ : S →+* S₂} {M' : Submodule R M} {N' : Submodule S N} {f : M →ₛₗ[ρ] N →ₛₗ[σ] P} (hM' : M' ≤ f.ker) (hN' : N' ≤ f.flip.ker) (m : M) (n : N) :
    ((liftQ₂ M' N' f hM' hN') (Submodule.Quotient.mk m)) (Submodule.Quotient.mk n) = (f m) n
    source
    @[reducible, inline]
    abbrev LinearMap.IsRefl.liftQ₂ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [AddCommGroup M] [CommRing R] [CommRing S] [Module R M] [AddCommGroup P] [Module S P] {I₁ I₂ : R →+* S} (f : M →ₛₗ[I₁] M →ₛₗ[I₂] P) (N : Submodule R M) (hf : f.IsRefl) (hN : N ≤ f.ker) :
    M ⧸ N →ₛₗ[I₁] M ⧸ N →ₛₗ[I₂] P

    Special case of LinearMap.liftQ₂ with left and right spaces the same. Reducible so that simp lemmas about LinearMap.liftQ₂ apply to it.

    Equations
    Instances For