Lifting bilinear forms to quotients #
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)
:
Lift a bilinear form from M × N → P to (M ⧸ M') × (N ⧸ N') → P.
Instances For
@[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)
:
@[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)
:
Special case of LinearMap.liftQ₂ with left and right spaces the same. Reducible so
that simp lemmas about LinearMap.liftQ₂ apply to it.
Equations
- LinearMap.IsRefl.liftQ₂ f N hf hN = LinearMap.liftQ₂ N N f hN ⋯