Images of pairs of submodules under bilinear maps #
This file provides Submodule.map₂
, which is later used to implement Submodule.mul
.
Main results #
Submodule.map₂_eq_span_image2
: the image of two submodules under a bilinear map is the span of theirSet.image2
.
Notes #
This file is quite similar to the n-ary section of Data.Set.Basic
and to Order.Filter.NAry
.
Please keep them in sync.
TODO #
Generalize this file to semilinear maps.
def
Submodule.map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q : Submodule R N)
:
Submodule R P
Map a pair of submodules under a bilinear map.
This is the submodule version of Set.image2
.
Equations
- Submodule.map₂ f p q = ⨆ (s : ↥p), Submodule.map (f ↑s) q
Instances For
theorem
Submodule.apply_mem_map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
{m : M}
{n : N}
{p : Submodule R M}
{q : Submodule R N}
(hm : m ∈ p)
(hn : n ∈ q)
:
theorem
Submodule.map₂_le
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p : Submodule R M}
{q : Submodule R N}
{r : Submodule R P}
:
theorem
Submodule.map₂_span_span
(R : Type u_1)
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(s : Set M)
(t : Set N)
:
@[simp]
theorem
Submodule.map₂_bot_right
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
:
@[simp]
theorem
Submodule.map₂_bot_left
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(q : Submodule R N)
:
theorem
Submodule.map₂_le_map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p₁ p₂ : Submodule R M}
{q₁ q₂ : Submodule R N}
(hp : p₁ ≤ p₂)
(hq : q₁ ≤ q₂)
:
theorem
Submodule.map₂_le_map₂_left
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p₁ p₂ : Submodule R M}
{q : Submodule R N}
(h : p₁ ≤ p₂)
:
theorem
Submodule.map₂_le_map₂_right
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p : Submodule R M}
{q₁ q₂ : Submodule R N}
(h : q₁ ≤ q₂)
:
theorem
Submodule.map₂_sup_right
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q₁ q₂ : Submodule R N)
:
theorem
Submodule.map₂_sup_left
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p₁ p₂ : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.image2_subset_map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.map₂_eq_span_image2
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.map₂_flip
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.map₂_iSup_left
{ι : Sort uι}
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(s : ι → Submodule R M)
(t : Submodule R N)
:
theorem
Submodule.map₂_iSup_right
{ι : Sort uι}
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(s : Submodule R M)
(t : ι → Submodule R N)
:
theorem
Submodule.map₂_span_singleton_eq_map
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(m : M)
:
theorem
Submodule.map₂_span_singleton_eq_map_flip
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(s : Submodule R M)
(n : N)
:
theorem
Submodule.map_map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{P₂ : Type u_7}
[AddCommMonoid P₂]
[Module R P₂]
(f : P →ₗ[R] P₂)
(g : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.map₂_map_right
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{N₂ : Type u_6}
[AddCommMonoid N₂]
[Module R N₂]
(f : M →ₗ[R] N₂ →ₗ[R] P)
(g : N →ₗ[R] N₂)
(p : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.map₂_map_left
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{M₂ : Type u_5}
[AddCommMonoid M₂]
[Module R M₂]
(f : M₂ →ₗ[R] N →ₗ[R] P)
(g : M →ₗ[R] M₂)
(p : Submodule R M)
(q : Submodule R N)
:
theorem
Submodule.map₂_map_map
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{M₂ : Type u_5}
{N₂ : Type u_6}
[AddCommMonoid M₂]
[AddCommMonoid N₂]
[Module R M₂]
[Module R N₂]
(f : M₂ →ₗ[R] N₂ →ₗ[R] P)
(g : M →ₗ[R] M₂)
(h : N →ₗ[R] N₂)
(p : Submodule R M)
(q : Submodule R N)
: