Mathlib.LinearAlgebra.Prod

LinearMap.fst definition

: M × M₂ →ₗ[R] M

Full source

/-- The first projection of a product is a linear map. -/
def fst : M × M₂M × M₂ →ₗ[R] M where
  toFun := Prod.fst
  map_add' _x _y := rfl
  map_smul' _x _y := rfl

First projection linear map

Informal description

The linear map that projects the first component of a direct product $M \times M_2$ of modules over a ring $R$ onto $M$. Specifically, for any element $(x, y) \in M \times M_2$, the map returns $x$.

LinearMap.snd definition

: M × M₂ →ₗ[R] M₂

Full source

/-- The second projection of a product is a linear map. -/
def snd : M × M₂M × M₂ →ₗ[R] M₂ where
  toFun := Prod.snd
  map_add' _x _y := rfl
  map_smul' _x _y := rfl

Second projection linear map

Informal description

The linear map that projects a pair $(x, y)$ in the product module $M \times M_2$ over a ring $R$ to its second component $y \in M_2$.

LinearMap.fst_apply theorem

(x : M × M₂) : fst R M M₂ x = x.1

Full source

@[simp]
theorem fst_apply (x : M × M₂) : fst R M M₂ x = x.1 :=
  rfl

First Projection Map Evaluation

Informal description

For any element $x = (x_1, x_2)$ in the direct product module $M \times M_2$ over a ring $R$, the first projection linear map satisfies $\text{fst}(x) = x_1$.

LinearMap.snd_apply theorem

(x : M × M₂) : snd R M M₂ x = x.2

Full source

@[simp]
theorem snd_apply (x : M × M₂) : snd R M M₂ x = x.2 :=
  rfl

Evaluation of Second Projection Linear Map

Informal description

For any element $x = (x_1, x_2)$ in the product module $M \times M_2$ over a ring $R$, the second projection linear map satisfies $\operatorname{snd}(x) = x_2$.

LinearMap.coe_fst theorem

: ⇑(fst R M M₂) = Prod.fst

Full source

@[simp, norm_cast] lemma coe_fst : ⇑(fst R M M₂) = Prod.fst := rfl

First Projection Linear Map Equals Standard Projection

Informal description

The underlying function of the first projection linear map $fst_{R,M,M_2} : M \times M_2 \to M$ is equal to the standard first projection function $Prod.fst$ on the product module $M \times M_2$.

LinearMap.coe_snd theorem

: ⇑(snd R M M₂) = Prod.snd

Full source

@[simp, norm_cast] lemma coe_snd : ⇑(snd R M M₂) = Prod.snd := rfl

Coefficient of Second Projection Linear Map Equals Standard Projection

Informal description

The underlying function of the second projection linear map $\operatorname{snd}_{R,M,M_2}$ is equal to the standard second projection function $\operatorname{Prod.snd}$ on the product module $M \times M_2$.

LinearMap.fst_surjective theorem

: Function.Surjective (fst R M M₂)

Full source

theorem fst_surjective : Function.Surjective (fst R M M₂) := fun x => ⟨(x, 0), rfl⟩

Surjectivity of First Projection Linear Map

Informal description

The first projection linear map $\operatorname{fst}_{R,M,M_2} : M \times M_2 \to M$ is surjective.

LinearMap.snd_surjective theorem

: Function.Surjective (snd R M M₂)

Full source

theorem snd_surjective : Function.Surjective (snd R M M₂) := fun x => ⟨(0, x), rfl⟩

Surjectivity of the Second Projection Linear Map

Informal description

The second projection linear map $\operatorname{snd}_{R,M,M_2} : M \times M_2 \to M_2$ is surjective.

LinearMap.prod definition

(f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : M →ₗ[R] M₂ × M₃

Full source

/-- The prod of two linear maps is a linear map. -/
@[simps]
def prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : M →ₗ[R] M₂ × M₃ where
  toFun := Pi.prod f g
  map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add]
  map_smul' c x := by simp only [Pi.prod, Prod.smul_mk, map_smul, RingHom.id_apply]

Product of linear maps

Informal description

Given two linear maps $ f : M \to M_2 $ and $ g : M \to M_3 $ over a ring $ R $, the product linear map $ f \times g : M \to M_2 \times M_3 $ is defined by $ (f \times g)(x) = (f(x), g(x)) $ for all $ x \in M $. This map is linear, preserving addition and scalar multiplication.

LinearMap.coe_prod theorem

(f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Pi.prod f g

Full source

theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

Coefficient Equality for Product of Linear Maps

Informal description

For any linear maps $f : M \to M_2$ and $g : M \to M_3$ over a ring $R$, the underlying function of the product linear map $f \times g$ is equal to the product of the functions $f$ and $g$, i.e., $(f \times g)(x) = (f(x), g(x))$ for all $x \in M$.

LinearMap.fst_prod theorem

(f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : (fst R M₂ M₃).comp (prod f g) = f

Full source

@[simp]
theorem fst_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : (fst R M₂ M₃).comp (prod f g) = f := rfl

First projection of product map equals first factor

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be modules over $R$. Given linear maps $f : M \to M_2$ and $g : M \to M_3$, the composition of the first projection map $\mathrm{fst} : M_2 \times M_3 \to M_2$ with the product map $f \times g : M \to M_2 \times M_3$ equals $f$, i.e., $\mathrm{fst} \circ (f \times g) = f$.

LinearMap.snd_prod theorem

(f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : (snd R M₂ M₃).comp (prod f g) = g

Full source

@[simp]
theorem snd_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : (snd R M₂ M₃).comp (prod f g) = g := rfl

Second projection of product map equals second factor

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be modules over $R$. Given linear maps $f : M \to M_2$ and $g : M \to M_3$, the composition of the second projection map $\mathrm{snd} : M_2 \times M_3 \to M_3$ with the product map $f \times g : M \to M_2 \times M_3$ equals $g$, i.e., $\mathrm{snd} \circ (f \times g) = g$.

LinearMap.pair_fst_snd theorem

: prod (fst R M M₂) (snd R M M₂) = LinearMap.id

Full source

@[simp]
theorem pair_fst_snd : prod (fst R M M₂) (snd R M M₂) = LinearMap.id := rfl

Product of Projections is Identity

Informal description

The product of the first projection linear map $\mathrm{fst} : M \times M_2 \to M$ and the second projection linear map $\mathrm{snd} : M \times M_2 \to M_2$ is equal to the identity linear map $\mathrm{id} : M \times M_2 \to M \times M_2$. In other words, $(\mathrm{fst}, \mathrm{snd}) = \mathrm{id}$.

LinearMap.prod_comp theorem

 (f : M₂ →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (h : M →ₗ[R] M₂) : (f.prod g).comp h = (f.comp h).prod (g.comp h)

Full source

theorem prod_comp (f : M₂ →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄)
    (h : M →ₗ[R] M₂) : (f.prod g).comp h = (f.comp h).prod (g.comp h) :=
  rfl

Composition of Product Linear Maps Equals Product of Compositions

Informal description

For any linear maps $ f : M_2 \to M_3 $, $ g : M_2 \to M_4 $, and $ h : M \to M_2 $ over a ring $ R $, the composition of the product map $ f \times g $ with $ h $ is equal to the product of the compositions $ f \circ h $ and $ g \circ h $. In other words, $(f \times g) \circ h = (f \circ h) \times (g \circ h)$.

LinearMap.prodEquiv definition

 [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] :
  ((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] M →ₗ[R] M₂ × M₃

Full source

/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
@[simps]
def prodEquiv [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] :
    ((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] M →ₗ[R] M₂ × M₃ where
  toFun f := f.1.prod f.2
  invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)
  left_inv f := by ext <;> rfl
  right_inv f := by ext <;> rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Equivalence between product of linear maps and linear maps to product

Informal description

Given modules $M$, $M_2$, and $M_3$ over rings $R$ and $S$, with $M_2$ and $M_3$ also being $S$-modules and the scalar multiplications of $R$ and $S$ commuting on $M_2$ and $M_3$, there is a linear equivalence between the product of linear maps $(M \to_{R} M_2) \times (M \to_{R} M_3)$ and the linear maps $M \to_{R} M_2 \times M_3$. This equivalence is constructed by mapping a pair of linear maps $(f, g)$ to their product map $f \times g$, and its inverse takes a linear map $h$ to the pair of compositions $(h \circ \pi_1, h \circ \pi_2)$, where $\pi_1$ and $\pi_2$ are the first and second projection maps from $M_2 \times M_3$ to $M_2$ and $M_3$ respectively.

LinearMap.inl definition

: M →ₗ[R] M × M₂

Full source

/-- The left injection into a product is a linear map. -/
def inl : M →ₗ[R] M × M₂ :=
  prod LinearMap.id 0

Left injection linear map into product

Informal description

The left injection linear map $ \text{inl} : M \to M \times M_2 $ over a ring $ R $ is defined by $ \text{inl}(x) = (x, 0) $ for all $ x \in M $. This map is linear, preserving addition and scalar multiplication.

LinearMap.inr definition

: M₂ →ₗ[R] M × M₂

Full source

/-- The right injection into a product is a linear map. -/
def inr : M₂ →ₗ[R] M × M₂ :=
  prod 0 LinearMap.id

Right injection linear map into product

Informal description

The right injection linear map $ \text{inr} : M_2 \to M \times M_2 $ over a ring $ R $ is defined by $ \text{inr}(x) = (0, x) $ for all $ x \in M_2 $. This map is linear, preserving addition and scalar multiplication.

LinearMap.range_inl theorem

: range (inl R M M₂) = ker (snd R M M₂)

Full source

theorem range_inl : range (inl R M M₂) = ker (snd R M M₂) := by
  ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.fst, Prod.ext rfl h.symm⟩

Range of Left Injection Equals Kernel of Second Projection

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. The range of the left injection linear map $\text{inl} : M \to M \times M_2$ is equal to the kernel of the second projection linear map $\text{snd} : M \times M_2 \to M_2$. In other words, $\text{range}(\text{inl}) = \text{ker}(\text{snd})$, where: - $\text{inl}(x) = (x, 0)$ for all $x \in M$, - $\text{snd}(x, y) = y$ for all $(x, y) \in M \times M_2$.

LinearMap.ker_snd theorem

: ker (snd R M M₂) = range (inl R M M₂)

Full source

theorem ker_snd : ker (snd R M M₂) = range (inl R M M₂) :=
  Eq.symm <| range_inl R M M₂

Kernel of Second Projection Equals Range of Left Injection

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. The kernel of the second projection linear map $\text{snd} : M \times M_2 \to M_2$ is equal to the range of the left injection linear map $\text{inl} : M \to M \times M_2$. In other words, $\text{ker}(\text{snd}) = \text{range}(\text{inl})$, where: - $\text{snd}(x, y) = y$ for all $(x, y) \in M \times M_2$, - $\text{inl}(x) = (x, 0)$ for all $x \in M$.

LinearMap.range_inr theorem

: range (inr R M M₂) = ker (fst R M M₂)

Full source

theorem range_inr : range (inr R M M₂) = ker (fst R M M₂) := by
  ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.snd, Prod.ext h.symm rfl⟩

Range of Right Injection Equals Kernel of First Projection

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. The range of the right injection linear map $\text{inr} : M_2 \to M \times M_2$ is equal to the kernel of the first projection linear map $\text{fst} : M \times M_2 \to M$. In other words, $\text{range}(\text{inr}) = \text{ker}(\text{fst})$, where: - $\text{inr}(x) = (0, x)$ for all $x \in M_2$, - $\text{fst}(x, y) = x$ for all $(x, y) \in M \times M_2$.

LinearMap.ker_fst theorem

: ker (fst R M M₂) = range (inr R M M₂)

Full source

theorem ker_fst : ker (fst R M M₂) = range (inr R M M₂) :=
  Eq.symm <| range_inr R M M₂

Kernel of First Projection Equals Range of Right Injection

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. The kernel of the first projection linear map $\mathrm{fst} : M \times M_2 \to M$ is equal to the range of the right injection linear map $\mathrm{inr} : M_2 \to M \times M_2$. In other words, $\ker(\mathrm{fst}) = \mathrm{range}(\mathrm{inr})$, where: - $\mathrm{fst}(x, y) = x$ for all $(x, y) \in M \times M_2$, - $\mathrm{inr}(x) = (0, x)$ for all $x \in M_2$.

LinearMap.fst_comp_inl theorem

: fst R M M₂ ∘ₗ inl R M M₂ = id

Full source

@[simp] theorem fst_comp_inl : fstfst R M M₂ ∘ₗ inl R M M₂ = id := rfl

First Projection Composed with Left Injection Yields Identity

Informal description

Let $R$ be a ring and let $M$ and $M_2$ be $R$-modules. The composition of the first projection linear map $\text{fst} : M \times M_2 \to M$ with the left injection linear map $\text{inl} : M \to M \times M_2$ equals the identity map on $M$, i.e., $\text{fst} \circ \text{inl} = \text{id}_M$.

LinearMap.snd_comp_inl theorem

: snd R M M₂ ∘ₗ inl R M M₂ = 0

Full source

@[simp] theorem snd_comp_inl : sndsnd R M M₂ ∘ₗ inl R M M₂ = 0 := rfl

Composition of Second Projection with Left Injection Yields Zero Map

Informal description

The composition of the second projection linear map $\text{snd} : M \times M_2 \to M_2$ with the left injection linear map $\text{inl} : M \to M \times M_2$ over a ring $R$ equals the zero map, i.e., $\text{snd} \circ \text{inl} = 0$.

LinearMap.fst_comp_inr theorem

: fst R M M₂ ∘ₗ inr R M M₂ = 0

Full source

@[simp] theorem fst_comp_inr : fstfst R M M₂ ∘ₗ inr R M M₂ = 0 := rfl

Composition of First Projection with Right Injection Yields Zero Map

Informal description

The composition of the first projection linear map $\text{fst} : M \times M_2 \to M$ with the right injection linear map $\text{inr} : M_2 \to M \times M_2$ over a ring $R$ equals the zero map, i.e., $\text{fst} \circ \text{inr} = 0$.

LinearMap.snd_comp_inr theorem

: snd R M M₂ ∘ₗ inr R M M₂ = id

Full source

@[simp] theorem snd_comp_inr : sndsnd R M M₂ ∘ₗ inr R M M₂ = id := rfl

Composition of Second Projection with Right Injection Yields Identity

Informal description

The composition of the second projection linear map $\text{snd} : M \times M_2 \to M_2$ with the right injection linear map $\text{inr} : M_2 \to M \times M_2$ over a ring $R$ equals the identity map on $M_2$, i.e., $\text{snd} \circ \text{inr} = \text{id}_{M_2}$.

LinearMap.coe_inl theorem

: (inl R M M₂ : M → M × M₂) = fun x => (x, 0)

Full source

@[simp]
theorem coe_inl : (inl R M M₂ : M → M × M₂) = fun x => (x, 0) :=
  rfl

Coefficient of Left Injection Linear Map

Informal description

The left injection linear map $\text{inl} : M \to M \times M_2$ over a ring $R$ is given by the function $x \mapsto (x, 0)$.

LinearMap.inl_apply theorem

(x : M) : inl R M M₂ x = (x, 0)

Full source

theorem inl_apply (x : M) : inl R M M₂ x = (x, 0) :=
  rfl

Evaluation of Left Injection Linear Map: $\text{inl}(x) = (x, 0)$

Informal description

For any element $x \in M$, the left injection linear map $\text{inl} : M \to M \times M_2$ over a ring $R$ satisfies $\text{inl}(x) = (x, 0)$.

LinearMap.coe_inr theorem

: (inr R M M₂ : M₂ → M × M₂) = Prod.mk 0

Full source

@[simp]
theorem coe_inr : (inr R M M₂ : M₂ → M × M₂) = Prod.mk 0 :=
  rfl

Coefficient of Right Injection Linear Map

Informal description

The right injection linear map $\text{inr} : M_2 \to M \times M_2$ over a ring $R$ is given by the function $x \mapsto (0, x)$.

LinearMap.inr_apply theorem

(x : M₂) : inr R M M₂ x = (0, x)

Full source

theorem inr_apply (x : M₂) : inr R M M₂ x = (0, x) :=
  rfl

Right Injection Linear Map Evaluation: $\text{inr}(x) = (0, x)$

Informal description

For any element $x \in M_2$, the right injection linear map $\text{inr} : M_2 \to M \times M_2$ over a ring $R$ satisfies $\text{inr}(x) = (0, x)$.

LinearMap.inl_eq_prod theorem

: inl R M M₂ = prod LinearMap.id 0

Full source

theorem inl_eq_prod : inl R M M₂ = prod LinearMap.id 0 :=
  rfl

Left Injection as Product of Identity and Zero Maps

Informal description

The left injection linear map $\text{inl} : M \to M \times M_2$ over a ring $R$ is equal to the product of the identity map $\text{id} : M \to M$ and the zero map $0 : M \to M_2$, i.e., $\text{inl} = (\text{id}, 0)$.

LinearMap.inr_eq_prod theorem

: inr R M M₂ = prod 0 LinearMap.id

Full source

theorem inr_eq_prod : inr R M M₂ = prod 0 LinearMap.id :=
  rfl

Right Injection as Product of Zero and Identity Maps

Informal description

The right injection linear map $\text{inr} : M_2 \to M \times M_2$ over a ring $R$ is equal to the product of the zero map $0 : M \to M_2$ and the identity map $\text{id} : M_2 \to M_2$, i.e., $\text{inr} = (0, \text{id})$.

LinearMap.inl_injective theorem

: Function.Injective (inl R M M₂)

Full source

theorem inl_injective : Function.Injective (inl R M M₂) := fun _ => by simp

Injectivity of Left Injection Linear Map

Informal description

The left injection linear map $\text{inl} \colon M \to M \times M_2$ over a ring $R$ is injective. That is, for any $x, y \in M$, if $\text{inl}(x) = \text{inl}(y)$, then $x = y$.

LinearMap.inr_injective theorem

: Function.Injective (inr R M M₂)

Full source

theorem inr_injective : Function.Injective (inr R M M₂) := fun _ => by simp

Injectivity of the Right Injection Linear Map

Informal description

The right injection linear map $\text{inr} : M_2 \to M \times M_2$ over a ring $R$ is injective. That is, for any $x, y \in M_2$, if $\text{inr}(x) = \text{inr}(y)$, then $x = y$.

LinearMap.coprod definition

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : M × M₂ →ₗ[R] M₃

Full source

/-- The coprod function `x : M × M₂ ↦ f x.1 + g x.2` is a linear map. -/
def coprod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : M × M₂M × M₂ →ₗ[R] M₃ :=
  f.comp (fst _ _ _) + g.comp (snd _ _ _)

Coproduct of linear maps

Informal description

Given two linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$ over a ring $R$, the coproduct linear map $\operatorname{coprod} f g \colon M \times M_2 \to M_3$ is defined by $(x, y) \mapsto f(x) + g(y)$.

LinearMap.coprod_apply theorem

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (x : M × M₂) : coprod f g x = f x.1 + g x.2

Full source

@[simp]
theorem coprod_apply (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (x : M × M₂) :
    coprod f g x = f x.1 + g x.2 :=
  rfl

Evaluation of Coproduct Linear Map: $(f \sqcup g)(x,y) = f(x) + g(y)$

Informal description

For any linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$ over a ring $R$, and any element $x = (x_1, x_2) \in M \times M_2$, the coproduct map satisfies $(f \sqcup g)(x) = f(x_1) + g(x_2)$.

LinearMap.coprod_inl theorem

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inl R M M₂) = f

Full source

@[simp]
theorem coprod_inl (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inl R M M₂) = f := by
  ext; simp only [map_zero, add_zero, coprod_apply, inl_apply, comp_apply]

Composition of Coproduct with Left Injection Equals First Map

Informal description

For any linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$ over a ring $R$, the composition of the coproduct map $f \sqcup g \colon M \times M_2 \to M_3$ with the left injection $\text{inl} \colon M \to M \times M_2$ equals $f$. That is, $(f \sqcup g) \circ \text{inl} = f$.

LinearMap.coprod_inr theorem

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inr R M M₂) = g

Full source

@[simp]
theorem coprod_inr (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inr R M M₂) = g := by
  ext; simp only [map_zero, coprod_apply, inr_apply, zero_add, comp_apply]

Composition of Coproduct with Right Injection Equals Second Map

Informal description

Given two linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$ over a ring $R$, the composition of the coproduct map $f \sqcup g \colon M \times M_2 \to M_3$ with the right injection $\text{inr} \colon M_2 \to M \times M_2$ equals $g$. That is, $(f \sqcup g) \circ \text{inr} = g$.

LinearMap.coprod_inl_inr theorem

: coprod (inl R M M₂) (inr R M M₂) = LinearMap.id

Full source

@[simp]
theorem coprod_inl_inr : coprod (inl R M M₂) (inr R M M₂) = LinearMap.id := by
  ext <;>
    simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

Coproduct of Injections Equals Identity on Product Module

Informal description

For any ring $R$ and $R$-modules $M$ and $M_2$, the coproduct of the left injection $\operatorname{inl} \colon M \to M \times M_2$ and the right injection $\operatorname{inr} \colon M_2 \to M \times M_2$ equals the identity map on $M \times M_2$. That is, $$\operatorname{coprod}(\operatorname{inl}, \operatorname{inr}) = \operatorname{id}.$$

LinearMap.coprod_zero_left theorem

(g : M₂ →ₗ[R] M₃) : (0 : M →ₗ[R] M₃).coprod g = g.comp (snd R M M₂)

Full source

theorem coprod_zero_left (g : M₂ →ₗ[R] M₃) : (0 : M →ₗ[R] M₃).coprod g = g.comp (snd R M M₂) :=
  zero_add _

Coproduct with Zero Left Map Equals Composition with Second Projection

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules. For any linear map $g \colon M_2 \to M_3$, the coproduct of the zero map $0 \colon M \to M_3$ with $g$ is equal to the composition of $g$ with the second projection map $\operatorname{snd} \colon M \times M_2 \to M_2$. In other words, $$ 0 \coprod g = g \circ \operatorname{snd}. $$

LinearMap.coprod_zero_right theorem

(f : M →ₗ[R] M₃) : f.coprod (0 : M₂ →ₗ[R] M₃) = f.comp (fst R M M₂)

Full source

theorem coprod_zero_right (f : M →ₗ[R] M₃) : f.coprod (0 : M₂ →ₗ[R] M₃) = f.comp (fst R M M₂) :=
  add_zero _

Coproduct with Zero Map Equals Composition with First Projection

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules. For any linear map $f \colon M \to M_3$, the coproduct of $f$ with the zero map $0 \colon M_2 \to M_3$ is equal to the composition of $f$ with the first projection map $\operatorname{fst} \colon M \times M_2 \to M$. In other words, $$ f \coprod 0 = f \circ \operatorname{fst}. $$

LinearMap.comp_coprod theorem

 (f : M₃ →ₗ[R] M₄) (g₁ : M →ₗ[R] M₃) (g₂ : M₂ →ₗ[R] M₃) : f.comp (g₁.coprod g₂) = (f.comp g₁).coprod (f.comp g₂)

Full source

theorem comp_coprod (f : M₃ →ₗ[R] M₄) (g₁ : M →ₗ[R] M₃) (g₂ : M₂ →ₗ[R] M₃) :
    f.comp (g₁.coprod g₂) = (f.comp g₁).coprod (f.comp g₂) :=
  ext fun x => f.map_add (g₁ x.1) (g₂ x.2)

Composition Distributes Over Coproduct of Linear Maps

Informal description

Let $R$ be a ring, and let $M$, $M_2$, $M_3$, and $M_4$ be $R$-modules. For any linear maps $f \colon M_3 \to M_4$, $g_1 \colon M \to M_3$, and $g_2 \colon M_2 \to M_3$, the composition of $f$ with the coproduct of $g_1$ and $g_2$ is equal to the coproduct of the compositions $f \circ g_1$ and $f \circ g_2$. In other words, $$ f \circ (g_1 \coprod g_2) = (f \circ g_1) \coprod (f \circ g_2). $$

LinearMap.fst_eq_coprod theorem

: fst R M M₂ = coprod LinearMap.id 0

Full source

theorem fst_eq_coprod : fst R M M₂ = coprod LinearMap.id 0 := by ext; simp

First Projection as Coproduct of Identity and Zero Maps

Informal description

The first projection linear map $\operatorname{fst} \colon M \times M_2 \to M$ over a ring $R$ is equal to the coproduct of the identity map $\operatorname{id} \colon M \to M$ and the zero map $0 \colon M_2 \to M$. In other words, for any $(x, y) \in M \times M_2$, we have $\operatorname{fst}(x, y) = \operatorname{id}(x) + 0(y) = x$.

LinearMap.snd_eq_coprod theorem

: snd R M M₂ = coprod 0 LinearMap.id

Full source

theorem snd_eq_coprod : snd R M M₂ = coprod 0 LinearMap.id := by ext; simp

Second Projection as Coproduct of Zero and Identity Maps

Informal description

The second projection linear map $\operatorname{snd} \colon M \times M_2 \to M_2$ over a ring $R$ is equal to the coproduct of the zero map $0 \colon M \to M_2$ and the identity map $\operatorname{id} \colon M_2 \to M_2$. In other words, for any $(x, y) \in M \times M_2$, we have $\operatorname{snd}(x, y) = 0(x) + \operatorname{id}(y) = y$.

LinearMap.coprod_comp_prod theorem

 (f : M₂ →ₗ[R] M₄) (g : M₃ →ₗ[R] M₄) (f' : M →ₗ[R] M₂) (g' : M →ₗ[R] M₃) :
  (f.coprod g).comp (f'.prod g') = f.comp f' + g.comp g'

Full source

@[simp]
theorem coprod_comp_prod (f : M₂ →ₗ[R] M₄) (g : M₃ →ₗ[R] M₄) (f' : M →ₗ[R] M₂) (g' : M →ₗ[R] M₃) :
    (f.coprod g).comp (f'.prod g') = f.comp f' + g.comp g' :=
  rfl

Composition of Coproduct and Product of Linear Maps Equals Sum of Compositions

Informal description

Let $R$ be a ring, and let $M$, $M_2$, $M_3$, and $M_4$ be $R$-modules. Given linear maps $f \colon M_2 \to M_4$, $g \colon M_3 \to M_4$, $f' \colon M \to M_2$, and $g' \colon M \to M_3$, the composition of the coproduct map $(f \operatorname{coprod} g) \colon M_2 \times M_3 \to M_4$ with the product map $(f' \operatorname{prod} g') \colon M \to M_2 \times M_3$ is equal to the sum of the compositions $f \circ f'$ and $g \circ g'$. That is, $$(f \operatorname{coprod} g) \circ (f' \operatorname{prod} g') = f \circ f' + g \circ g'.$$

LinearMap.coprod_map_prod theorem

 (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M) (S' : Submodule R M₂) :
  (Submodule.prod S S').map (LinearMap.coprod f g) = S.map f ⊔ S'.map g

Full source

@[simp]
theorem coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M)
    (S' : Submodule R M₂) : (Submodule.prod S S').map (LinearMap.coprod f g) = S.map f ⊔ S'.map g :=
  SetLike.coe_injective <| by
    simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]
    rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]
    exact Set.image_prod fun m m₂ => f m + g m₂

Image of Product Submodule under Coproduct Map Equals Supremum of Images

Informal description

Let $R$ be a ring, $M$, $M_2$, and $M_3$ be $R$-modules, and $f \colon M \to M_3$ and $g \colon M_2 \to M_3$ be linear maps. For any submodules $S \subseteq M$ and $S' \subseteq M_2$, the image of the product submodule $S \times S'$ under the coproduct map $f \operatorname{coprod} g$ is equal to the supremum of the images of $S$ under $f$ and $S'$ under $g$. That is, $$(S \times S').\text{map}(f \operatorname{coprod} g) = S.\text{map}(f) \sqcup S'.\text{map}(g).$$

LinearMap.coprodEquiv definition

 [Module S M₃] [SMulCommClass R S M₃] : ((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] M × M₂ →ₗ[R] M₃

Full source

/-- Taking the product of two maps with the same codomain is equivalent to taking the product of
their domains.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
@[simps]
def coprodEquiv [Module S M₃] [SMulCommClass R S M₃] :
    ((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] M × M₂ →ₗ[R] M₃ where
  toFun f := f.1.coprod f.2
  invFun f := (f.comp (inl _ _ _), f.comp (inr _ _ _))
  left_inv f := by simp only [coprod_inl, coprod_inr]
  right_inv f := by simp only [← comp_coprod, comp_id, coprod_inl_inr]
  map_add' a b := by
    ext
    simp only [Prod.snd_add, add_apply, coprod_apply, Prod.fst_add, add_add_add_comm]
  map_smul' r a := by
    dsimp
    ext
    simp only [smul_add, smul_apply, Prod.smul_snd, Prod.smul_fst, coprod_apply]

Linear equivalence between product of linear maps and coproduct linear map

Informal description

Given modules $M$, $M_2$, and $M_3$ over a ring $R$, and a module $M_3$ over a ring $S$ with compatible scalar multiplication (i.e., $R$ and $S$ actions commute on $M_3$), the equivalence $\text{coprodEquiv}$ establishes a linear isomorphism between the product of linear maps $(M \to_{R} M_3) \times (M_2 \to_{R} M_3)$ and the linear maps from the product module $M \times M_2$ to $M_3$ over $R$. Explicitly, the equivalence maps a pair of linear maps $(f, g)$ to their coproduct $\operatorname{coprod} f g \colon M \times M_2 \to M_3$, defined by $(x, y) \mapsto f(x) + g(y)$. The inverse operation decomposes a linear map $h \colon M \times M_2 \to M_3$ into its components $h \circ \text{inl}$ and $h \circ \text{inr}$, where $\text{inl} \colon M \to M \times M_2$ and $\text{inr} \colon M_2 \to M \times M_2$ are the canonical inclusion maps.

LinearMap.prod_ext_iff theorem

 {f g : M × M₂ →ₗ[R] M₃} : f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _)

Full source

theorem prod_ext_iff {f g : M × M₂M × M₂ →ₗ[R] M₃} :
    f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _) :=
  (coprodEquiv ℕ).symm.injective.eq_iff.symm.trans Prod.ext_iff

Equality of Linear Maps on Product Module via Components

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules. For any two linear maps $f, g \colon M \times M_2 \to M_3$, the following are equivalent: 1. $f = g$ as linear maps. 2. Both $f \circ \text{inl} = g \circ \text{inl}$ and $f \circ \text{inr} = g \circ \text{inr}$, where $\text{inl} \colon M \to M \times M_2$ and $\text{inr} \colon M_2 \to M \times M_2$ are the canonical inclusion maps.

LinearMap.prod_ext theorem

 {f g : M × M₂ →ₗ[R] M₃} (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _)) (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) :
  f = g

Full source

/--
Split equality of linear maps from a product into linear maps over each component, to allow `ext`
to apply lemmas specific to `M →ₗ M₃` and `M₂ →ₗ M₃`.

See note [partially-applied ext lemmas]. -/
@[ext 1100]
theorem prod_ext {f g : M × M₂M × M₂ →ₗ[R] M₃} (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
    (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) : f = g :=
  prod_ext_iff.2 ⟨hl, hr⟩

Equality of Linear Maps on Product via Componentwise Equality

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules. For any two linear maps $f, g \colon M \times M_2 \to M_3$, if the compositions $f \circ \text{inl} = g \circ \text{inl}$ and $f \circ \text{inr} = g \circ \text{inr}$ hold, where $\text{inl} \colon M \to M \times M_2$ and $\text{inr} \colon M_2 \to M \times M_2$ are the canonical inclusion maps, then $f = g$.

LinearMap.prodMap definition

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : M × M₂ →ₗ[R] M₃ × M₄

Full source

/-- `Prod.map` of two linear maps. -/
def prodMap (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : M × M₂M × M₂ →ₗ[R] M₃ × M₄ :=
  (f.comp (fst R M M₂)).prod (g.comp (snd R M M₂))

Product of linear maps on product modules

Informal description

Given two linear maps $ f : M \to M_3 $ and $ g : M_2 \to M_4 $ over a ring $ R $, the product map $ f \times g : M \times M_2 \to M_3 \times M_4 $ is defined by $(f \times g)(x, y) = (f(x), g(y))$ for all $(x, y) \in M \times M_2$. This map is constructed by composing $f$ with the first projection and $g$ with the second projection, then taking their product.

LinearMap.coe_prodMap theorem

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : ⇑(f.prodMap g) = Prod.map f g

Full source

theorem coe_prodMap (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : ⇑(f.prodMap g) = Prod.map f g :=
  rfl

Coefficient of Product Map Equals Product of Coefficients

Informal description

For any linear maps $ f : M \to M_3 $ and $ g : M_2 \to M_4 $ over a ring $ R $, the underlying function of the product map $ f \times g $ is equal to the product of the functions $ f $ and $ g $, i.e., $ (f \times g)(x, y) = (f(x), g(y)) $ for all $ (x, y) \in M \times M_2 $.

LinearMap.prodMap_apply theorem

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x) : f.prodMap g x = (f x.1, g x.2)

Full source

@[simp]
theorem prodMap_apply (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x) : f.prodMap g x = (f x.1, g x.2) :=
  rfl

Evaluation of Product Map on Product Module Elements

Informal description

Given two linear maps $ f : M \to M_3 $ and $ g : M_2 \to M_4 $ over a ring $ R $, and an element $ x = (x_1, x_2) \in M \times M_2 $, the product map $ f \times g $ satisfies $(f \times g)(x) = (f(x_1), g(x_2))$.

LinearMap.prodMap_comap_prod theorem

 (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (S : Submodule R M₂) (S' : Submodule R M₄) :
  (Submodule.prod S S').comap (LinearMap.prodMap f g) = (S.comap f).prod (S'.comap g)

Full source

theorem prodMap_comap_prod (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (S : Submodule R M₂)
    (S' : Submodule R M₄) :
    (Submodule.prod S S').comap (LinearMap.prodMap f g) = (S.comap f).prod (S'.comap g) :=
  SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

Preimage of Product Submodule under Product Map

Informal description

Let $R$ be a ring, $f : M \to M_2$ and $g : M_3 \to M_4$ be linear maps over $R$, and $S \subseteq M_2$, $S' \subseteq M_4$ be submodules. Then the preimage of the product submodule $S \times S'$ under the product map $f \times g$ is equal to the product of the preimages, i.e., $$(f \times g)^{-1}(S \times S') = f^{-1}(S) \times g^{-1}(S').$$

LinearMap.ker_prodMap theorem

(f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) : ker (LinearMap.prodMap f g) = Submodule.prod (ker f) (ker g)

Full source

theorem ker_prodMap (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) :
    ker (LinearMap.prodMap f g) = Submodule.prod (ker f) (ker g) := by
  dsimp only [ker]
  rw [← prodMap_comap_prod, Submodule.prod_bot]

Kernel of Product Map Equals Product of Kernels

Informal description

Let $R$ be a ring, and let $f : M \to M_2$ and $g : M_3 \to M_4$ be linear maps over $R$. The kernel of the product map $f \times g : M \times M_3 \to M_2 \times M_4$ is equal to the product of the kernels of $f$ and $g$, i.e., $$\ker(f \times g) = \ker f \times \ker g.$$

LinearMap.prodMap_id theorem

: (id : M →ₗ[R] M).prodMap (id : M₂ →ₗ[R] M₂) = id

Full source

@[simp]
theorem prodMap_id : (id : M →ₗ[R] M).prodMap (id : M₂ →ₗ[R] M₂) = id :=
  rfl

Identity Product Map Equals Identity on Product Module

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. The product of the identity linear maps $\text{id}_M : M \to M$ and $\text{id}_{M_2} : M_2 \to M_2$ is equal to the identity linear map on the product module $M \times M_2$, i.e., $$\text{id}_M \times \text{id}_{M_2} = \text{id}_{M \times M_2}.$$

LinearMap.prodMap_one theorem

: (1 : M →ₗ[R] M).prodMap (1 : M₂ →ₗ[R] M₂) = 1

Full source

@[simp]
theorem prodMap_one : (1 : M →ₗ[R] M).prodMap (1 : M₂ →ₗ[R] M₂) = 1 :=
  rfl

Product of Identity Maps is Identity on Product Module

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. The product of the identity linear maps $\text{id}_M : M \to M$ and $\text{id}_{M_2} : M_2 \to M_2$ is equal to the identity linear map on the product module $M \times M_2$, i.e., $$\text{id}_M \times \text{id}_{M_2} = \text{id}_{M \times M_2}.$$

LinearMap.prodMap_comp theorem

 (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆) :
  f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂)

Full source

theorem prodMap_comp (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅)
    (g₂₃ : M₅ →ₗ[R] M₆) :
    f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂) :=
  rfl

Composition of Product Linear Maps Equals Product of Compositions

Informal description

Let $R$ be a ring, and let $M$, $M_2$, $M_3$, $M_4$, $M_5$, $M_6$ be $R$-modules. Given linear maps $f_{12} : M \to M_2$, $f_{23} : M_2 \to M_3$, $g_{12} : M_4 \to M_5$, and $g_{23} : M_5 \to M_6$, the composition of the product maps $f_{23} \times g_{23}$ and $f_{12} \times g_{12}$ equals the product map of the compositions $(f_{23} \circ f_{12}) \times (g_{23} \circ g_{12})$. In other words, $$(f_{23} \times g_{23}) \circ (f_{12} \times g_{12}) = (f_{23} \circ f_{12}) \times (g_{23} \circ g_{12}).$$

LinearMap.prodMap_mul theorem

 (f₁₂ : M →ₗ[R] M) (f₂₃ : M →ₗ[R] M) (g₁₂ : M₂ →ₗ[R] M₂) (g₂₃ : M₂ →ₗ[R] M₂) :
  f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (g₂₃ * g₁₂)

Full source

theorem prodMap_mul (f₁₂ : M →ₗ[R] M) (f₂₃ : M →ₗ[R] M) (g₁₂ : M₂ →ₗ[R] M₂) (g₂₃ : M₂ →ₗ[R] M₂) :
    f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (g₂₃ * g₁₂) :=
  rfl

Composition of Product Linear Maps Equals Product of Compositions

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be $R$-modules. Given linear endomorphisms $f_{12}, f_{23} : M \to M$ and $g_{12}, g_{23} : M_2 \to M_2$, the composition of the product maps $f_{23} \times g_{23}$ and $f_{12} \times g_{12}$ equals the product map of the compositions $(f_{23} \circ f_{12}) \times (g_{23} \circ g_{12})$. In other words, $$(f_{23} \times g_{23}) \circ (f_{12} \times g_{12}) = (f_{23} \circ f_{12}) \times (g_{23} \circ g_{12}).$$

LinearMap.prodMap_add theorem

 (f₁ : M →ₗ[R] M₃) (f₂ : M →ₗ[R] M₃) (g₁ : M₂ →ₗ[R] M₄) (g₂ : M₂ →ₗ[R] M₄) :
  (f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂

Full source

theorem prodMap_add (f₁ : M →ₗ[R] M₃) (f₂ : M →ₗ[R] M₃) (g₁ : M₂ →ₗ[R] M₄) (g₂ : M₂ →ₗ[R] M₄) :
    (f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂ :=
  rfl

Additivity of Product of Linear Maps

Informal description

Let $R$ be a ring, and let $M$, $M_2$, $M_3$, $M_4$ be $R$-modules. Given linear maps $f_1, f_2 : M \to M_3$ and $g_1, g_2 : M_2 \to M_4$, the product map of the sums $(f_1 + f_2) \times (g_1 + g_2)$ is equal to the sum of the product maps $f_1 \times g_1 + f_2 \times g_2$. In other words, $$(f_1 + f_2) \times (g_1 + g_2) = (f_1 \times g_1) + (f_2 \times g_2).$$

LinearMap.prodMap_zero theorem

: (0 : M →ₗ[R] M₂).prodMap (0 : M₃ →ₗ[R] M₄) = 0

Full source

@[simp]
theorem prodMap_zero : (0 : M →ₗ[R] M₂).prodMap (0 : M₃ →ₗ[R] M₄) = 0 :=
  rfl

Product of Zero Maps is Zero

Informal description

The product map of the zero linear maps from $M$ to $M_2$ and from $M_3$ to $M_4$ is equal to the zero linear map from $M \times M_3$ to $M_2 \times M_4$.

LinearMap.prodMap_smul theorem

 [DistribMulAction S M₃] [DistribMulAction S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] (s : S) (f : M →ₗ[R] M₃)
  (g : M₂ →ₗ[R] M₄) : prodMap (s • f) (s • g) = s • prodMap f g

Full source

@[simp]
theorem prodMap_smul [DistribMulAction S M₃] [DistribMulAction S M₄] [SMulCommClass R S M₃]
    [SMulCommClass R S M₄] (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
    prodMap (s • f) (s • g) = s • prodMap f g :=
  rfl

Scalar Multiplication Commutes with Product of Linear Maps

Informal description

Let $R$ and $S$ be rings, and let $M$, $M_2$, $M_3$, $M_4$ be $R$-modules such that $M_3$ and $M_4$ are also $S$-modules with compatible scalar actions. For any scalar $s \in S$ and linear maps $f : M \to M_3$ and $g : M_2 \to M_4$ over $R$, the product map of the scaled maps $s \cdot f$ and $s \cdot g$ is equal to the scaling of the product map by $s$, i.e., $$(s \cdot f) \times (s \cdot g) = s \cdot (f \times g).$$

LinearMap.prodMapLinear definition

 [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] :
  (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄

Full source

/-- `LinearMap.prodMap` as a `LinearMap` -/
@[simps]
def prodMapLinear [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] :
    (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄)(M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄ where
  toFun f := prodMap f.1 f.2
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Linear map of product maps

Informal description

Given modules $ M, M_2, M_3, M_4 $ over a ring $ R $, and a ring $ S $ such that $ M_3 $ and $ M_4 $ are also $ S $-modules with compatible scalar actions, the function `LinearMap.prodMapLinear` maps a pair of linear maps $ (f : M \to M_3, g : M_2 \to M_4) $ to the linear map $ f \times g : M \times M_2 \to M_3 \times M_4 $ defined by $ (f \times g)(x, y) = (f(x), g(y)) $. This construction is itself an $ S $-linear map.

LinearMap.prodMapRingHom definition

: (M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂

Full source

/-- `LinearMap.prodMap` as a `RingHom` -/
@[simps]
def prodMapRingHom : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)(M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂ where
  toFun f := prodMap f.1 f.2
  map_one' := prodMap_one
  map_zero' := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl

Ring homomorphism of product maps of linear endomorphisms

Informal description

The function `LinearMap.prodMapRingHom` constructs a ring homomorphism from the product of two endomorphism rings of $R$-modules $M$ and $M_2$ to the endomorphism ring of their product module $M \times M_2$. Specifically, it maps a pair of linear endomorphisms $(f : M \to M, g : M_2 \to M_2)$ to the product map $f \times g : M \times M_2 \to M \times M_2$ defined by $(f \times g)(x, y) = (f(x), g(y))$. This construction preserves the ring structure, including addition, multiplication, and multiplicative identity.

LinearMap.inl_map_mul theorem

(a₁ a₂ : A) : LinearMap.inl R A B (a₁ * a₂) = LinearMap.inl R A B a₁ * LinearMap.inl R A B a₂

Full source

theorem inl_map_mul (a₁ a₂ : A) :
    LinearMap.inl R A B (a₁ * a₂) = LinearMap.inl R A B a₁ * LinearMap.inl R A B a₂ :=
  Prod.ext rfl (by simp)

Multiplicativity of the Left Injection Linear Map

Informal description

For any elements $a_1, a_2$ in an $R$-algebra $A$, the left injection linear map $\text{inl} \colon A \to A \times B$ satisfies the multiplicative property: \[ \text{inl}(a_1 \cdot a_2) = \text{inl}(a_1) \cdot \text{inl}(a_2). \]

LinearMap.inr_map_mul theorem

(b₁ b₂ : B) : LinearMap.inr R A B (b₁ * b₂) = LinearMap.inr R A B b₁ * LinearMap.inr R A B b₂

Full source

theorem inr_map_mul (b₁ b₂ : B) :
    LinearMap.inr R A B (b₁ * b₂) = LinearMap.inr R A B b₁ * LinearMap.inr R A B b₂ :=
  Prod.ext (by simp) rfl

Multiplicativity of the Right Injection Linear Map

Informal description

For any elements $b_1, b_2$ in an $R$-algebra $B$, the right injection linear map $\text{inr} \colon B \to A \times B$ satisfies the multiplicative property: \[ \text{inr}(b_1 \cdot b_2) = \text{inr}(b_1) \cdot \text{inr}(b_2). \]

LinearMap.prodMapAlgHom definition

: Module.End R M × Module.End R M₂ →ₐ[R] Module.End R (M × M₂)

Full source

/-- `LinearMap.prodMap` as an `AlgHom` -/
@[simps!]
def prodMapAlgHom : Module.EndModule.End R M × Module.End R M₂Module.End R M × Module.End R M₂ →ₐ[R] Module.End R (M × M₂) :=
  { prodMapRingHom R M M₂ with commutes' := fun _ => rfl }

Algebra homomorphism of product maps of linear endomorphisms

Informal description

The algebra homomorphism version of the product map of linear endomorphisms, which maps a pair of endomorphisms $(f, g)$ of $R$-modules $M$ and $M_2$ to the product endomorphism $f \times g$ of $M \times M_2$. This homomorphism preserves the algebra structure, including scalar multiplication by elements of $R$.

LinearMap.range_coprod theorem

(f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : range (f.coprod g) = range f ⊔ range g

Full source

theorem range_coprod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : range (f.coprod g) = rangerange f ⊔ range g :=
  Submodule.ext fun x => by simp [mem_sup]

Range of Coproduct of Linear Maps is Supremum of Ranges

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules. Given linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$, the range of the coproduct map $\operatorname{coprod} f g \colon M \times M_2 \to M_3$ is equal to the supremum of the ranges of $f$ and $g$. That is, \[ \operatorname{range}(f \sqcup g) = \operatorname{range}(f) \sqcup \operatorname{range}(g). \]

LinearMap.isCompl_range_inl_inr theorem

: IsCompl (range <| inl R M M₂) (range <| inr R M M₂)

Full source

theorem isCompl_range_inl_inr : IsCompl (range <| inl R M M₂) (range <| inr R M M₂) := by
  constructor
  · rw [disjoint_def]
    rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩
    simp only [Prod.ext_iff, inl_apply, inr_apply, mem_bot] at hx hy ⊢
    exact ⟨hy.1.symm, hx.2.symm⟩
  · rw [codisjoint_iff_le_sup]
    rintro ⟨x, y⟩ -
    simp only [mem_sup, mem_range, exists_prop]
    refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩
    simp

Complementarity of Injection Ranges in Product Module

Informal description

Let $R$ be a ring and $M$, $M_2$ be $R$-modules. The ranges of the left injection linear map $\text{inl} \colon M \to M \times M_2$ and the right injection linear map $\text{inr} \colon M_2 \to M \times M_2$ are complementary submodules of $M \times M_2$, meaning their sum is the entire module and their intersection is trivial.

LinearMap.sup_range_inl_inr theorem

: (range <| inl R M M₂) ⊔ (range <| inr R M M₂) = ⊤

Full source

theorem sup_range_inl_inr : (range <| inl R M M₂) ⊔ (range <| inr R M M₂) = ⊤ :=
  IsCompl.sup_eq_top isCompl_range_inl_inr

Supremum of Injection Ranges Covers Product Module

Informal description

Let $R$ be a ring and $M$, $M_2$ be $R$-modules. The supremum of the ranges of the left injection linear map $\text{inl} \colon M \to M \times M_2$ and the right injection linear map $\text{inr} \colon M_2 \to M \times M_2$ is equal to the top submodule of $M \times M_2$. In other words, the sum of their ranges spans the entire product module: \[ \text{range}(\text{inl}) \sqcup \text{range}(\text{inr}) = \top. \]

LinearMap.disjoint_inl_inr theorem

: Disjoint (range <| inl R M M₂) (range <| inr R M M₂)

Full source

theorem disjoint_inl_inr : Disjoint (range <| inl R M M₂) (range <| inr R M M₂) := by
  simp +contextual [disjoint_def, @eq_comm M 0, @eq_comm M₂ 0]

Disjointness of Left and Right Injection Ranges in Product Module

Informal description

The ranges of the left injection linear map $\text{inl} \colon M \to M \times M_2$ and the right injection linear map $\text{inr} \colon M_2 \to M \times M_2$ are disjoint submodules of $M \times M_2$ over a ring $R$.

LinearMap.map_coprod_prod theorem

 (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M) (q : Submodule R M₂) :
  map (coprod f g) (p.prod q) = map f p ⊔ map g q

Full source

theorem map_coprod_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M)
    (q : Submodule R M₂) : map (coprod f g) (p.prod q) = mapmap f p ⊔ map g q := by
  refine le_antisymm ?_ (sup_le (map_le_iff_le_comap.2 ?_) (map_le_iff_le_comap.2 ?_))
  · rw [SetLike.le_def]
    rintro _ ⟨x, ⟨h₁, h₂⟩, rfl⟩
    exact mem_sup.2 ⟨_, ⟨_, h₁, rfl⟩, _, ⟨_, h₂, rfl⟩, rfl⟩
  · exact fun x hx => ⟨(x, 0), by simp [hx]⟩
  · exact fun x hx => ⟨(0, x), by simp [hx]⟩

Image of Product Submodule under Coproduct Map Equals Supremum of Images

Informal description

For any linear maps $f \colon M \to M₃$ and $g \colon M₂ \to M₃$ over a ring $R$, and any submodules $p \subseteq M$ and $q \subseteq M₂$, the image of the product submodule $p \times q$ under the coproduct map $\operatorname{coprod} f g$ is equal to the supremum of the images of $p$ under $f$ and $q$ under $g$. That is, $$ (\operatorname{coprod} f g)(p \times q) = f(p) \sqcup g(q). $$

LinearMap.comap_prod_prod theorem

 (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : Submodule R M₂) (q : Submodule R M₃) :
  comap (prod f g) (p.prod q) = comap f p ⊓ comap g q

Full source

theorem comap_prod_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : Submodule R M₂)
    (q : Submodule R M₃) : comap (prod f g) (p.prod q) = comapcomap f p ⊓ comap g q :=
  Submodule.ext fun _x => Iff.rfl

Preimage of Product Submodule under Product Map Equals Intersection of Preimages

Informal description

For linear maps $ f : M \to M_2 $ and $ g : M \to M_3 $ over a ring $ R $, and submodules $ p \subseteq M_2 $ and $ q \subseteq M_3 $, the preimage of the product submodule $ p \times q $ under the product map $ f \times g $ is equal to the intersection of the preimages of $ p $ under $ f $ and $ q $ under $ g $. That is, \[ (f \times g)^{-1}(p \times q) = f^{-1}(p) \cap g^{-1}(q). \]

LinearMap.prod_eq_inf_comap theorem

 (p : Submodule R M) (q : Submodule R M₂) : p.prod q = p.comap (LinearMap.fst R M M₂) ⊓ q.comap (LinearMap.snd R M M₂)

Full source

theorem prod_eq_inf_comap (p : Submodule R M) (q : Submodule R M₂) :
    p.prod q = p.comap (LinearMap.fst R M M₂) ⊓ q.comap (LinearMap.snd R M M₂) :=
  Submodule.ext fun _x => Iff.rfl

Product Submodule as Intersection of Projection Preimages

Informal description

For any submodules $p$ of $M$ and $q$ of $M_2$ over a ring $R$, the product submodule $p \times q$ is equal to the intersection of the preimages of $p$ under the first projection map and $q$ under the second projection map. That is, $$ p \times q = fst^{-1}(p) \cap snd^{-1}(q) $$ where $fst: M \times M_2 \to M$ and $snd: M \times M_2 \to M_2$ are the canonical projection linear maps.

LinearMap.prod_eq_sup_map theorem

 (p : Submodule R M) (q : Submodule R M₂) : p.prod q = p.map (LinearMap.inl R M M₂) ⊔ q.map (LinearMap.inr R M M₂)

Full source

theorem prod_eq_sup_map (p : Submodule R M) (q : Submodule R M₂) :
    p.prod q = p.map (LinearMap.inl R M M₂) ⊔ q.map (LinearMap.inr R M M₂) := by
  rw [← map_coprod_prod, coprod_inl_inr, map_id]

Product Submodule as Supremum of Injection Images

Informal description

For any submodules $p$ of $M$ and $q$ of $M_2$ over a ring $R$, the product submodule $p \times q$ is equal to the supremum of the images of $p$ under the left injection map $\operatorname{inl} \colon M \to M \times M_2$ and $q$ under the right injection map $\operatorname{inr} \colon M_2 \to M \times M_2$. That is, $$ p \times q = \operatorname{inl}(p) \sqcup \operatorname{inr}(q). $$

LinearMap.span_inl_union_inr theorem

{s : Set M} {t : Set M₂} : span R (inl R M M₂ '' s ∪ inr R M M₂ '' t) = (span R s).prod (span R t)

Full source

theorem span_inl_union_inr {s : Set M} {t : Set M₂} :
    span R (inlinl R M M₂ '' sinl R M M₂ '' s ∪ inr R M M₂ '' t) = (span R s).prod (span R t) := by
  rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]

Span of Union of Injection Images Equals Product of Spans

Informal description

For any subsets $s$ of $M$ and $t$ of $M_2$ over a ring $R$, the linear span of the union of the images of $s$ under the left injection map $\operatorname{inl} \colon M \to M \times M_2$ and $t$ under the right injection map $\operatorname{inr} \colon M_2 \to M \times M_2$ is equal to the product of the linear spans of $s$ and $t$. That is, \[ \operatorname{span}_R (\operatorname{inl}(s) \cup \operatorname{inr}(t)) = (\operatorname{span}_R s) \times (\operatorname{span}_R t). \]

LinearMap.ker_prod theorem

(f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ker (prod f g) = ker f ⊓ ker g

Full source

@[simp]
theorem ker_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ker (prod f g) = kerker f ⊓ ker g := by
  rw [ker, ← prod_bot, comap_prod_prod]; rfl

Kernel of Product Map Equals Intersection of Kernels

Informal description

For linear maps $ f : M \to M_2 $ and $ g : M \to M_3 $ over a ring $ R $, the kernel of the product map $ f \times g $ is equal to the intersection of the kernels of $ f $ and $ g $. That is, \[ \ker(f \times g) = \ker f \cap \ker g. \]

LinearMap.range_prod_le theorem

(f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : range (prod f g) ≤ (range f).prod (range g)

Full source

theorem range_prod_le (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
    range (prod f g) ≤ (range f).prod (range g) := by
  simp only [SetLike.le_def, prod_apply, mem_range, SetLike.mem_coe, mem_prod, exists_imp]
  rintro _ x rfl
  exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩

Range of Product Map is Contained in Product of Ranges

Informal description

For any linear maps $ f : M \to M_2 $ and $ g : M \to M_3 $ over a ring $ R $, the range of the product map $ f \times g : M \to M_2 \times M_3 $ is contained in the product of their ranges, i.e., \[ \operatorname{range}(f \times g) \subseteq (\operatorname{range} f) \times (\operatorname{range} g). \]

LinearMap.ker_prod_ker_le_ker_coprod theorem

 {M₂ : Type*} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type*} [AddCommMonoid M₃] [Module R M₃] (f : M →ₗ[R] M₃)
  (g : M₂ →ₗ[R] M₃) : (ker f).prod (ker g) ≤ ker (f.coprod g)

Full source

theorem ker_prod_ker_le_ker_coprod {M₂ : Type*} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type*}
    [AddCommMonoid M₃] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
    (ker f).prod (ker g) ≤ ker (f.coprod g) := by
  rintro ⟨y, z⟩
  simp +contextual

Inclusion of Product of Kernels in Kernel of Coproduct

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules with $M_2$ and $M_3$ being additive commutative monoids. For any linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$, the product of their kernels is contained in the kernel of their coproduct, i.e., $(\ker f) \times (\ker g) \subseteq \ker (f \operatorname{coprod} g)$.

LinearMap.ker_coprod_of_disjoint_range theorem

 {M₂ : Type*} [AddCommGroup M₂] [Module R M₂] {M₃ : Type*} [AddCommGroup M₃] [Module R M₃] (f : M →ₗ[R] M₃)
  (g : M₂ →ₗ[R] M₃) (hd : Disjoint (range f) (range g)) : ker (f.coprod g) = (ker f).prod (ker g)

Full source

theorem ker_coprod_of_disjoint_range {M₂ : Type*} [AddCommGroup M₂] [Module R M₂] {M₃ : Type*}
    [AddCommGroup M₃] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃)
    (hd : Disjoint (range f) (range g)) : ker (f.coprod g) = (ker f).prod (ker g) := by
  apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g)
  rintro ⟨y, z⟩ h
  simp only [mem_ker, mem_prod, coprod_apply] at h ⊢
  have : f y ∈ (range f) ⊓ (range g) := by
    simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]
    use -z
    rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
  rw [hd.eq_bot, mem_bot] at this
  rw [this] at h
  simpa [this] using h

Kernel of Coproduct Map for Linear Maps with Disjoint Ranges

Informal description

Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be $R$-modules with $M_2$ and $M_3$ being additive commutative groups. For any linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$ with disjoint ranges (i.e., $\operatorname{range} f \cap \operatorname{range} g = \{0\}$), the kernel of their coproduct map $f \operatorname{coprod} g$ is equal to the product of their kernels, i.e., \[ \ker(f \operatorname{coprod} g) = (\ker f) \times (\ker g). \]

Submodule.sup_eq_range theorem

(p q : Submodule R M) : p ⊔ q = range (p.subtype.coprod q.subtype)

Full source

theorem sup_eq_range (p q : Submodule R M) : p ⊔ q = range (p.subtype.coprod q.subtype) :=
  Submodule.ext fun x => by simp [Submodule.mem_sup, SetLike.exists]

Supremum of Submodules as Range of Coproduct Inclusion Maps

Informal description

Let $R$ be a ring and $M$ an $R$-module. For any two submodules $p$ and $q$ of $M$, their supremum $p \sqcup q$ is equal to the range of the coproduct of their inclusion maps, i.e., \[ p \sqcup q = \operatorname{range} (p.\text{subtype} \operatorname{coprod} q.\text{subtype}). \]

Submodule.map_inl theorem

: p.map (inl R M M₂) = prod p ⊥

Full source

@[simp]
theorem map_inl : p.map (inl R M M₂) = prod p ⊥ := by
  ext ⟨x, y⟩
  simp only [and_left_comm, eq_comm, mem_map, Prod.mk_inj, inl_apply, mem_bot, exists_eq_left',
    mem_prod]

Image of Submodule under Left Injection Equals Product with Zero Submodule

Informal description

For any submodule $p$ of an $R$-module $M$, the image of $p$ under the left injection linear map $\text{inl} : M \to M \times M_2$ is equal to the direct product $p \times \{0\}$ (where $\{0\}$ denotes the zero submodule of $M_2$).

Submodule.map_inr theorem

: q.map (inr R M M₂) = prod ⊥ q

Full source

@[simp]
theorem map_inr : q.map (inr R M M₂) = prod ⊥ q := by
  ext ⟨x, y⟩; simp [and_left_comm, eq_comm, and_comm]

Image of Submodule under Right Injection Equals Product with Zero Submodule

Informal description

For any submodule $q$ of an $R$-module $M_2$, the image of $q$ under the right injection linear map $\text{inr} : M_2 \to M \times M_2$ is equal to the direct product $\{0\} \times q$ (where $\{0\}$ denotes the zero submodule of $M$).

Submodule.comap_fst theorem

: p.comap (fst R M M₂) = prod p ⊤

Full source

@[simp]
theorem comap_fst : p.comap (fst R M M₂) = prod p ⊤ := by ext ⟨x, y⟩; simp

Preimage of Submodule under First Projection Equals Product with Full Module

Informal description

For any submodule $p$ of $M$, the preimage of $p$ under the first projection linear map $\operatorname{fst} : M \times M_2 \to M$ is equal to the direct product $p \times M_2$.

Submodule.comap_snd theorem

: q.comap (snd R M M₂) = prod ⊤ q

Full source

@[simp]
theorem comap_snd : q.comap (snd R M M₂) = prod ⊤ q := by ext ⟨x, y⟩; simp

Preimage of Submodule under Second Projection Equals Product with Full Module

Informal description

For any submodule $q$ of $M_2$, the preimage of $q$ under the second projection linear map $\operatorname{snd} : M \times M_2 \to M_2$ is equal to the direct product $M \times q$.

Submodule.prod_comap_inl theorem

: (prod p q).comap (inl R M M₂) = p

Full source

@[simp]
theorem prod_comap_inl : (prod p q).comap (inl R M M₂) = p := by ext; simp

Preimage of Product Submodule under Left Injection Equals First Factor

Informal description

For any submodules $p$ of $M$ and $q$ of $M₂$ over a ring $R$, the preimage of the product submodule $p \times q$ under the left injection linear map $\operatorname{inl} : M \to M \times M₂$ is equal to $p$.

Submodule.prod_comap_inr theorem

: (prod p q).comap (inr R M M₂) = q

Full source

@[simp]
theorem prod_comap_inr : (prod p q).comap (inr R M M₂) = q := by ext; simp

Preimage of Product Submodule under Right Injection Equals Second Factor

Informal description

For any submodules $p$ of $M$ and $q$ of $M_2$ over a ring $R$, the preimage of the product submodule $p \times q$ under the right injection linear map $\operatorname{inr} : M_2 \to M \times M_2$ is equal to $q$.

Submodule.prod_map_fst theorem

: (prod p q).map (fst R M M₂) = p

Full source

@[simp]
theorem prod_map_fst : (prod p q).map (fst R M M₂) = p := by
  ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ q)]

First Projection of Product Submodule Equals First Factor

Informal description

For any submodules $p$ of $M$ and $q$ of $M_2$ over a ring $R$, the image of the product submodule $p \times q$ under the first projection linear map $\operatorname{fst} : M \times M_2 \to M$ is equal to $p$.

Submodule.prod_map_snd theorem

: (prod p q).map (snd R M M₂) = q

Full source

@[simp]
theorem prod_map_snd : (prod p q).map (snd R M M₂) = q := by
  ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ p)]

Second Projection of Product Submodule Equals Second Factor

Informal description

For any submodules $p$ of $M$ and $q$ of $M_2$ over a ring $R$, the image of the product submodule $p \times q$ under the second projection linear map $\operatorname{snd} : M \times M_2 \to M_2$ is equal to $q$.

Submodule.ker_inl theorem

: ker (inl R M M₂) = ⊥

Full source

@[simp]
theorem ker_inl : ker (inl R M M₂) = ⊥ := by rw [ker, ← prod_bot, prod_comap_inl]

Kernel of Left Injection is Trivial

Informal description

The kernel of the left injection linear map $\operatorname{inl} : M \to M \times M_2$ over a ring $R$ is the trivial submodule $\{0\}$.

Submodule.ker_inr theorem

: ker (inr R M M₂) = ⊥

Full source

@[simp]
theorem ker_inr : ker (inr R M M₂) = ⊥ := by rw [ker, ← prod_bot, prod_comap_inr]

Kernel of Right Injection Linear Map is Trivial

Informal description

The kernel of the right injection linear map $\operatorname{inr} : M_2 \to M \times M_2$ is the trivial submodule $\{0\}$.

Submodule.range_fst theorem

: range (fst R M M₂) = ⊤

Full source

@[simp]
theorem range_fst : range (fst R M M₂) = ⊤ := by rw [range_eq_map, ← prod_top, prod_map_fst]

First Projection Linear Map is Surjective

Informal description

The range of the first projection linear map $\operatorname{fst} : M \times M_2 \to M$ is equal to the entire module $M$.

Submodule.range_snd theorem

: range (snd R M M₂) = ⊤

Full source

@[simp]
theorem range_snd : range (snd R M M₂) = ⊤ := by rw [range_eq_map, ← prod_top, prod_map_snd]

Second Projection Linear Map is Surjective

Informal description

The range of the second projection linear map $\operatorname{snd} : M \times M_2 \to M_2$ is equal to the entire module $M_2$.

Submodule.fst definition

: Submodule R (M × M₂)

Full source

/-- `M` as a submodule of `M × N`. -/
def fst : Submodule R (M × M₂) :=
  (⊥ : Submodule R M₂).comap (LinearMap.snd R M M₂)

First component submodule of $M \times M_2$

Informal description

The submodule of the product module $M \times M_2$ over a ring $R$ consisting of all pairs $(x, 0)$ where $x \in M$ and $0$ is the zero element of $M_2$. This is equivalent to $M$ embedded as the first component in the product.

Submodule.fstEquiv definition

: Submodule.fst R M M₂ ≃ₗ[R] M

Full source

/-- `M` as a submodule of `M × N` is isomorphic to `M`. -/
@[simps]
def fstEquiv : Submodule.fstSubmodule.fst R M M₂ ≃ₗ[R] M where
  -- Porting note: proofs were `tidy` or `simp`
  toFun x := x.1.1
  invFun m := ⟨⟨m, 0⟩, by simp [fst]⟩
  map_add' := by simp
  map_smul' := by simp
  left_inv := by
    rintro ⟨⟨x, y⟩, hy⟩
    simp only [fst, comap_bot, mem_ker, snd_apply] at hy
    simpa only [Subtype.mk.injEq, Prod.mk.injEq, true_and] using hy.symm
  right_inv := by rintro x; rfl

Linear equivalence between first component submodule and $M$

Informal description

The first component submodule $\mathrm{fst}\, R\, M\, M_2$ of the product module $M \times M_2$ over a ring $R$ is linearly equivalent to $M$. The equivalence maps each element $(x, 0)$ in the submodule to $x \in M$, and its inverse maps each $x \in M$ to $(x, 0)$ in the submodule.

Submodule.fst_map_fst theorem

: (Submodule.fst R M M₂).map (LinearMap.fst R M M₂) = ⊤

Full source

theorem fst_map_fst : (Submodule.fst R M M₂).map (LinearMap.fst R M M₂) = ⊤ := by
  aesop

First projection maps first component submodule to entire module

Informal description

For any ring $R$ and modules $M$ and $M_2$ over $R$, the image of the first component submodule $\{(x, 0) \mid x \in M\}$ under the first projection linear map $(x, y) \mapsto x$ is the entire module $M$ (denoted by $\top$).

Submodule.fst_map_snd theorem

: (Submodule.fst R M M₂).map (LinearMap.snd R M M₂) = ⊥

Full source

theorem fst_map_snd : (Submodule.fst R M M₂).map (LinearMap.snd R M M₂) = ⊥ := by
  aesop (add simp fst)

Second projection annihilates first component submodule

Informal description

The image of the first component submodule $M \times \{0\}$ under the second projection linear map $\mathrm{snd} : M \times M_2 \to M_2$ is the trivial submodule $\{0\}$ of $M_2$.

Submodule.snd definition

: Submodule R (M × M₂)

Full source

/-- `N` as a submodule of `M × N`. -/
def snd : Submodule R (M × M₂) :=
  (⊥ : Submodule R M).comap (LinearMap.fst R M M₂)

Second component submodule of $M \times M_2$

Informal description

The submodule of the direct product $M \times M_2$ consisting of elements of the form $(0, y)$, where $y \in M_2$. This is equivalent to $M_2$ embedded as the second component of the product.

Submodule.sndEquiv definition

: Submodule.snd R M M₂ ≃ₗ[R] M₂

Full source

/-- `N` as a submodule of `M × N` is isomorphic to `N`. -/
@[simps]
def sndEquiv : Submodule.sndSubmodule.snd R M M₂ ≃ₗ[R] M₂ where
  -- Porting note: proofs were `tidy` or `simp`
  toFun x := x.1.2
  invFun n := ⟨⟨0, n⟩, by simp [snd]⟩
  map_add' := by simp
  map_smul' := by simp
  left_inv := by
    rintro ⟨⟨x, y⟩, hx⟩
    simp only [snd, comap_bot, mem_ker, fst_apply] at hx
    simpa only [Subtype.mk.injEq, Prod.mk.injEq, and_true] using hx.symm
  right_inv := by rintro x; rfl

Linear equivalence between second component submodule and $M_2$

Informal description

The submodule of the direct product $M \times M_2$ consisting of elements of the form $(0, y)$, where $y \in M_2$, is linearly equivalent to $M_2$ itself. The equivalence is given by the projection map $(0, y) \mapsto y$ and the embedding map $y \mapsto (0, y)$.

Submodule.snd_map_fst theorem

: (Submodule.snd R M M₂).map (LinearMap.fst R M M₂) = ⊥

Full source

theorem snd_map_fst : (Submodule.snd R M M₂).map (LinearMap.fst R M M₂) = ⊥ := by
  aesop (add simp snd)

First Projection Maps Second Component to Zero Submodule

Informal description

The image of the second component submodule $S = \{(0, y) \mid y \in M_2\}$ under the first projection linear map $f : M \times M_2 \to M$ is the trivial submodule $\{0\}$ of $M$, i.e., $f(S) = \bot$.

Submodule.snd_map_snd theorem

: (Submodule.snd R M M₂).map (LinearMap.snd R M M₂) = ⊤

Full source

theorem snd_map_snd : (Submodule.snd R M M₂).map (LinearMap.snd R M M₂) = ⊤ := by
  aesop

Second Projection Maps Second Component Submodule Surjectively to $M_2$

Informal description

The image of the second component submodule $\{(0, y) \mid y \in M_2\}$ under the second projection linear map $(x, y) \mapsto y$ is the entire module $M_2$, i.e., $\text{map}(\text{snd})(\text{snd}(R, M, M_2)) = M_2$.

Submodule.fst_sup_snd theorem

: Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂ = ⊤

Full source

theorem fst_sup_snd : Submodule.fstSubmodule.fst R M M₂ ⊔ Submodule.snd R M M₂ = ⊤ := by
  rw [eq_top_iff]
  rintro ⟨m, n⟩ -
  rw [show (m, n) = (m, 0) + (0, n) by simp]
  apply Submodule.add_mem (Submodule.fstSubmodule.fst R M M₂ ⊔ Submodule.snd R M M₂)
  · exact Submodule.mem_sup_left (Submodule.mem_comap.mpr (by simp))
  · exact Submodule.mem_sup_right (Submodule.mem_comap.mpr (by simp))

First and Second Component Submodules Span the Product Module

Informal description

For any ring $R$ and $R$-modules $M$ and $M_2$, the supremum of the first component submodule $\{(x, 0) \mid x \in M\}$ and the second component submodule $\{(0, y) \mid y \in M_2\}$ in the product module $M \times M_2$ is equal to the entire module, i.e., $\text{fst}(R, M, M_2) \vee \text{snd}(R, M, M_2) = M \times M_2$.

Submodule.fst_inf_snd theorem

: Submodule.fst R M M₂ ⊓ Submodule.snd R M M₂ = ⊥

Full source

theorem fst_inf_snd : Submodule.fstSubmodule.fst R M M₂ ⊓ Submodule.snd R M M₂ = ⊥ := by
  aesop

Trivial Intersection of First and Second Component Submodules in Product Module

Informal description

The intersection of the first component submodule and the second component submodule of the product module $M \times M_2$ over a ring $R$ is the trivial submodule, i.e., $\text{fst}(R, M, M_2) \cap \text{snd}(R, M, M_2) = \{0\}$.

Submodule.le_prod_iff theorem

 {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
  q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Full source

theorem le_prod_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
    q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ := by
  constructor
  · intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Submodule Containment in Product Module via Projections

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $p_1$, $p_2$ be submodules of $M$ and $M_2$ respectively. For any submodule $q$ of the product module $M \times M_2$, the following are equivalent: 1. $q$ is contained in the product submodule $p_1 \times p_2$. 2. The image of $q$ under the first projection map is contained in $p_1$, and the image of $q$ under the second projection map is contained in $p_2$. In other words, $q \leq p_1 \times p_2$ if and only if $\text{fst}(q) \leq p_1$ and $\text{snd}(q) \leq p_2$.

Submodule.prod_le_iff theorem

 {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
  p₁.prod p₂ ≤ q ↔ map (LinearMap.inl R M M₂) p₁ ≤ q ∧ map (LinearMap.inr R M M₂) p₂ ≤ q

Full source

theorem prod_le_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
    p₁.prod p₂ ≤ q ↔ map (LinearMap.inl R M M₂) p₁ ≤ q ∧ map (LinearMap.inr R M M₂) p₂ ≤ q := by
  constructor
  · intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, zero_mem p₂⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨zero_mem p₁, hx⟩
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1
    have h2' : (LinearMap.inr R _ _) x2 ∈ q := by
      apply hK
      simpa using h2
    simpa using add_mem h1' h2'

Product Submodule Containment via Injection Maps

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $p_1$, $p_2$ be submodules of $M$ and $M_2$ respectively. For any submodule $q$ of the product module $M \times M_2$, the following are equivalent: 1. The product submodule $p_1 \times p_2$ is contained in $q$. 2. The image of $p_1$ under the left injection map $\text{inl} : M \to M \times M_2$ is contained in $q$, and the image of $p_2$ under the right injection map $\text{inr} : M_2 \to M \times M_2$ is contained in $q$. In other words, $p_1 \times p_2 \leq q$ if and only if $\text{inl}(p_1) \leq q$ and $\text{inr}(p_2) \leq q$.

Submodule.prod_eq_bot_iff theorem

{p₁ : Submodule R M} {p₂ : Submodule R M₂} : p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥

Full source

theorem prod_eq_bot_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
    p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥ := by
  simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot, ker_inl, ker_inr]

Product Submodule is Trivial if and only if Components are Trivial

Informal description

For submodules $p_1$ of $M$ and $p_2$ of $M_2$ over a ring $R$, the product submodule $p_1 \times p_2$ is trivial if and only if both $p_1$ and $p_2$ are trivial.

Submodule.prod_eq_top_iff theorem

{p₁ : Submodule R M} {p₂ : Submodule R M₂} : p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤

Full source

theorem prod_eq_top_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
    p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤ := by
  simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, map_top, range_fst, range_snd]

Product Submodule is Top if and only if Components are Top

Informal description

For any submodules $p_1$ of $M$ and $p_2$ of $M_2$ over a ring $R$, the product submodule $p_1 \times p_2$ is equal to the top submodule of $M \times M_2$ if and only if both $p_1$ is the top submodule of $M$ and $p_2$ is the top submodule of $M_2$.

LinearEquiv.prodComm definition

(R M N : Type*) [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : (M × N) ≃ₗ[R] N × M

Full source

/-- Product of modules is commutative up to linear isomorphism. -/
@[simps apply]
def prodComm (R M N : Type*) [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M]
    [Module R N] : (M × N) ≃ₗ[R] N × M :=
  { AddEquiv.prodComm with
    toFun := Prod.swap
    map_smul' := fun _r ⟨_m, _n⟩ => rfl }

Commutativity of module product via linear isomorphism

Informal description

The linear equivalence that swaps the components of the product module $M \times N$ to give $N \times M$, preserving the module structure. Specifically, for any semiring $R$ and $R$-modules $M$ and $N$, there exists a linear isomorphism between $M \times N$ and $N \times M$ that maps $(m, n)$ to $(n, m)$ and commutes with scalar multiplication.

LinearEquiv.fst_comp_prodComm theorem

: (LinearMap.fst R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.snd R M M₂)

Full source

theorem fst_comp_prodComm :
    (LinearMap.fst R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.snd R M M₂) := by
  ext <;> simp

Composition of First Projection with Product Commutator Equals Second Projection

Informal description

For any semiring $R$ and $R$-modules $M$ and $M₂$, the composition of the first projection linear map $\text{fst} \colon M₂ \times M \to M₂$ with the linear isomorphism $\text{prodComm} \colon M \times M₂ \to M₂ \times M$ equals the second projection linear map $\text{snd} \colon M \times M₂ \to M₂$.

LinearEquiv.snd_comp_prodComm theorem

: (LinearMap.snd R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.fst R M M₂)

Full source

theorem snd_comp_prodComm :
    (LinearMap.snd R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.fst R M M₂) := by
  ext <;> simp

Composition of Second Projection with Product Commutator Equals First Projection

Informal description

For any semiring $R$ and $R$-modules $M$ and $M₂$, the composition of the second projection linear map $\text{snd} \colon M₂ \times M \to M$ with the linear isomorphism $\text{prodComm} \colon M \times M₂ \to M₂ \times M$ equals the first projection linear map $\text{fst} \colon M \times M₂ \to M$.

LinearEquiv.prodAssoc definition

 (R M₁ M₂ M₃ : Type*) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂]
  [Module R M₃] : ((M₁ × M₂) × M₃) ≃ₗ[R] (M₁ × (M₂ × M₃))

Full source

/-- Product of modules is associative up to linear isomorphism. -/
@[simps apply]
def prodAssoc (R M₁ M₂ M₃ : Type*) [Semiring R]
    [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]
    [Module R M₁] [Module R M₂] [Module R M₃] : ((M₁ × M₂) × M₃) ≃ₗ[R] (M₁ × (M₂ × M₃)) :=
  { AddEquiv.prodAssoc with
    map_smul' := fun _r ⟨_m, _n⟩ => rfl }

Associativity of module products under linear equivalence

Informal description

Given a semiring $R$ and $R$-modules $M_1$, $M_2$, $M_3$, there exists a linear equivalence between the $R$-modules $(M_1 \times M_2) \times M_3$ and $M_1 \times (M_2 \times M_3)$. This equivalence preserves both the additive and multiplicative structures, showing that the product of modules is associative up to linear isomorphism.

LinearEquiv.fst_comp_prodAssoc theorem

 :
  (LinearMap.fst R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
    (LinearMap.fst R M₁ M₂).comp (LinearMap.fst R (M₁ × M₂) M₃)

Full source

theorem fst_comp_prodAssoc :
    (LinearMap.fst R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
    (LinearMap.fst R M₁ M₂).comp (LinearMap.fst R (M₁ × M₂) M₃) := by
  ext <;> simp

First Projection Commutes with Associativity Equivalence

Informal description

Let $R$ be a semiring, and let $M_1$, $M_2$, $M_3$ be $R$-modules. The composition of the first projection linear map $\text{fst} \colon M_1 \times (M_2 \times M_3) \to M_1$ with the linear equivalence $\text{prodAssoc} \colon (M_1 \times M_2) \times M_3 \to M_1 \times (M_2 \times M_3)$ is equal to the composition of the first projection $\text{fst} \colon M_1 \times M_2 \to M_1$ with the first projection $\text{fst} \colon (M_1 \times M_2) \times M_3 \to M_1 \times M_2$.

LinearEquiv.snd_comp_prodAssoc theorem

 :
  (LinearMap.snd R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
    (LinearMap.snd R M₁ M₂).prodMap (LinearMap.id : M₃ →ₗ[R] M₃)

Full source

theorem snd_comp_prodAssoc :
    (LinearMap.snd R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
    (LinearMap.snd R M₁ M₂).prodMap (LinearMap.id : M₃ →ₗ[R] M₃):= by
  ext <;> simp

Compatibility of Second Projection with Associativity Linear Equivalence

Informal description

Let $R$ be a semiring, and let $M_1$, $M_2$, $M_3$ be $R$-modules. The composition of the second projection map $\text{snd} \colon M_1 \times (M_2 \times M_3) \to M_2 \times M_3$ with the linear equivalence $\text{prodAssoc} \colon (M_1 \times M_2) \times M_3 \to M_1 \times (M_2 \times M_3)$ is equal to the product map of the second projection $\text{snd} \colon M_1 \times M_2 \to M_2$ and the identity map $\text{id} \colon M_3 \to M_3$. In other words, the following diagram commutes: \[ \text{snd} \circ \text{prodAssoc} = \text{snd} \times \text{id} \]

LinearEquiv.prodProdProdComm definition

: ((M × M₂) × M₃ × M₄) ≃ₗ[R] (M × M₃) × M₂ × M₄

Full source

/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
@[simps apply]
def prodProdProdComm : ((M × M₂) × M₃ × M₄) ≃ₗ[R] (M × M₃) × M₂ × M₄ :=
  { AddEquiv.prodProdProdComm M M₂ M₃ M₄ with
    toFun := fun mnmn => ((mnmn.1.1, mnmn.2.1), (mnmn.1.2, mnmn.2.2))
    invFun := fun mmnn => ((mmnn.1.1, mmnn.2.1), (mmnn.1.2, mmnn.2.2))
    map_smul' := fun _c _mnmn => rfl }

Commutativity of quadruple product linear equivalence

Informal description

The linear equivalence `prodProdProdComm` rearranges the components of a quadruple product `((M × M₂) × M₃ × M₄)` to `((M × M₃) × M₂ × M₄)`, preserving both the additive and scalar multiplicative structures. Explicitly, it maps `((x, y), (z, w))` to `((x, z), (y, w))` and its inverse maps `((x, y), (z, w))` back to `((x, z), (y, w))`.

LinearEquiv.prodProdProdComm_symm theorem

: (prodProdProdComm R M M₂ M₃ M₄).symm = prodProdProdComm R M M₃ M₂ M₄

Full source

@[simp]
theorem prodProdProdComm_symm :
    (prodProdProdComm R M M₂ M₃ M₄).symm = prodProdProdComm R M M₃ M₂ M₄ :=
  rfl

Inverse of quadruple product linear equivalence equals its reverse form

Informal description

The inverse of the linear equivalence `prodProdProdComm` that rearranges components from `((M × M₂) × M₃ × M₄)` to `((M × M₃) × M₂ × M₄)` is equal to the linear equivalence `prodProdProdComm` that rearranges components from `((M × M₃) × M₂ × M₄)` to `((M × M₂) × M₃ × M₄)`.

LinearEquiv.prodProdProdComm_toAddEquiv theorem

: (prodProdProdComm R M M₂ M₃ M₄ : _ ≃+ _) = AddEquiv.prodProdProdComm M M₂ M₃ M₄

Full source

@[simp]
theorem prodProdProdComm_toAddEquiv :
    (prodProdProdComm R M M₂ M₃ M₄ : _ ≃+ _) = AddEquiv.prodProdProdComm M M₂ M₃ M₄ :=
  rfl

Additive Equivalence of Quadruple Product Rearrangement

Informal description

The underlying additive equivalence of the linear equivalence `prodProdProdComm` is equal to the additive equivalence `prodProdProdComm` that rearranges the components of the quadruple product $((M \times M₂) \times M₃ \times M₄)$ to $((M \times M₃) \times M₂ \times M₄)$.

LinearEquiv.prodCongr definition

: (M × M₃) ≃ₗ[R] M₂ × M₄

Full source

/-- Product of linear equivalences; the maps come from `Equiv.prodCongr`. -/
protected def prodCongr : (M × M₃) ≃ₗ[R] M₂ × M₄ :=
  { e₁.toAddEquiv.prodCongr e₂.toAddEquiv with
    map_smul' := fun c _x => Prod.ext (e₁.map_smulₛₗ c _) (e₂.map_smulₛₗ c _) }

Product of linear equivalences

Informal description

Given linear equivalences $e_1 : M \simeq M_2$ and $e_2 : M_3 \simeq M_4$ over a ring $R$, the product linear equivalence $e_1 \times e_2$ maps $(x, y) \in M \times M_3$ to $(e_1(x), e_2(y)) \in M_2 \times M_4$.

LinearEquiv.prodCongr_symm theorem

: (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

Full source

theorem prodCongr_symm : (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm :=
  rfl

Inverse of Product of Linear Equivalences Equals Product of Inverses

Informal description

Given linear equivalences $e_1 : M \simeq M_2$ and $e_2 : M_3 \simeq M_4$ over a ring $R$, the inverse of the product linear equivalence $e_1 \times e_2$ is equal to the product of the inverses $e_1^{-1} \times e_2^{-1}$.

LinearEquiv.prodCongr_apply theorem

(p) : e₁.prodCongr e₂ p = (e₁ p.1, e₂ p.2)

Full source

@[simp]
theorem prodCongr_apply (p) : e₁.prodCongr e₂ p = (e₁ p.1, e₂ p.2) :=
  rfl

Action of Product Linear Equivalence on Pairs

Informal description

Given linear equivalences $e_1 : M \simeq M_2$ and $e_2 : M_3 \simeq M_4$ over a ring $R$, and any pair $p = (x,y) \in M \times M_3$, the product linear equivalence $e_1 \times e_2$ maps $p$ to $(e_1(x), e_2(y)) \in M_2 \times M_4$.

LinearEquiv.coe_prodCongr theorem

 : (e₁.prodCongr e₂ : M × M₃ →ₗ[R] M₂ × M₄) = (e₁ : M →ₗ[R] M₂).prodMap (e₂ : M₃ →ₗ[R] M₄)

Full source

@[simp, norm_cast]
theorem coe_prodCongr :
    (e₁.prodCongr e₂ : M × M₃M × M₃ →ₗ[R] M₂ × M₄) = (e₁ : M →ₗ[R] M₂).prodMap (e₂ : M₃ →ₗ[R] M₄) :=
  rfl

Product Linear Equivalence as Product Map

Informal description

Given linear equivalences $e_1 : M \simeq M_2$ and $e_2 : M_3 \simeq M_4$ over a ring $R$, the underlying linear map of the product linear equivalence $e_1 \times e_2$ is equal to the product map $(e_1 : M \to M_2) \times (e_2 : M_3 \to M_4)$.

LinearEquiv.skewProd definition

(f : M →ₗ[R] M₄) : (M × M₃) ≃ₗ[R] M₂ × M₄

Full source

/-- Equivalence given by a block lower diagonal matrix. `e₁` and `e₂` are diagonal square blocks,
  and `f` is a rectangular block below the diagonal. -/
protected def skewProd (f : M →ₗ[R] M₄) : (M × M₃) ≃ₗ[R] M₂ × M₄ :=
  { ((e₁ : M →ₗ[R] M₂).comp (LinearMap.fst R M M₃)).prod
      ((e₂ : M₃ →ₗ[R] M₄).comp (LinearMap.snd R M M₃) +
        f.comp (LinearMap.fst R M M₃)) with
    invFun := fun p : M₂ × M₄ => (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1)))
    left_inv := fun p => by simp
    right_inv := fun p => by simp }

Skew product linear equivalence

Informal description

Given linear equivalences $e_1 : M \simeq M_2$ and $e_2 : M_3 \simeq M_4$ over a ring $R$, and a linear map $f : M \to M_4$, the skew product linear equivalence $e_1.skewProd\ e_2\ f : M \times M_3 \simeq M_2 \times M_4$ is defined by: \[ (x, y) \mapsto (e_1(x), e_2(y) + f(x)) \] with inverse: \[ (a, b) \mapsto (e_1^{-1}(a), e_2^{-1}(b - f(e_1^{-1}(a)))) \] This equivalence can be viewed as a block lower triangular matrix where $e_1$ and $e_2$ form the diagonal blocks and $f$ contributes to the off-diagonal block.

LinearEquiv.skewProd_apply theorem

(f : M →ₗ[R] M₄) (x) : e₁.skewProd e₂ f x = (e₁ x.1, e₂ x.2 + f x.1)

Full source

@[simp]
theorem skewProd_apply (f : M →ₗ[R] M₄) (x) : e₁.skewProd e₂ f x = (e₁ x.1, e₂ x.2 + f x.1) :=
  rfl

Application Formula for Skew Product Linear Equivalence

Informal description

Given linear equivalences $e_1 \colon M \simeq M_2$ and $e_2 \colon M_3 \simeq M_4$ over a ring $R$, and a linear map $f \colon M \to M_4$, the skew product linear equivalence $e_1.\text{skewProd}\ e_2\ f$ applied to an element $x = (x_1, x_2) \in M \times M_3$ is given by: \[ e_1.\text{skewProd}\ e_2\ f\ (x_1, x_2) = (e_1(x_1), e_2(x_2) + f(x_1)). \]

LinearEquiv.skewProd_symm_apply theorem

(f : M →ₗ[R] M₄) (x) : (e₁.skewProd e₂ f).symm x = (e₁.symm x.1, e₂.symm (x.2 - f (e₁.symm x.1)))

Full source

@[simp]
theorem skewProd_symm_apply (f : M →ₗ[R] M₄) (x) :
    (e₁.skewProd e₂ f).symm x = (e₁.symm x.1, e₂.symm (x.2 - f (e₁.symm x.1))) :=
  rfl

Inverse Formula for Skew Product Linear Equivalence

Informal description

Let $R$ be a ring, and let $e_1 \colon M \simeq M_2$ and $e_2 \colon M_3 \simeq M_4$ be linear equivalences over $R$. Given a linear map $f \colon M \to M_4$, the inverse of the skew product linear equivalence $e_1.\text{skewProd}\ e_2\ f$ applied to an element $x = (x_1, x_2) \in M_2 \times M_4$ is given by: \[ (e_1.\text{skewProd}\ e_2\ f)^{-1}(x_1, x_2) = \big(e_1^{-1}(x_1), e_2^{-1}(x_2 - f(e_1^{-1}(x_1)))\big). \]

LinearMap.range_prod_eq theorem

{f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f ⊔ ker g = ⊤) : range (prod f g) = (range f).prod (range g)

Full source

/-- If the union of the kernels `ker f` and `ker g` spans the domain, then the range of
`Prod f g` is equal to the product of `range f` and `range g`. -/
theorem range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : kerker f ⊔ ker g = ⊤) :
    range (prod f g) = (range f).prod (range g) := by
  refine le_antisymm (f.range_prod_le g) ?_
  simp only [SetLike.le_def, prod_apply, mem_range, SetLike.mem_coe, mem_prod, exists_imp, and_imp,
    Prod.forall, Pi.prod]
  rintro _ _ x rfl y rfl
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(f := f)`
  simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]
  have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
  rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩
  refine ⟨x' + x, ?_, ?_⟩
  · rwa [add_sub_cancel_right]
  · simp [← eq_sub_iff_add_eq.1 H, map_add, add_left_inj, left_eq_add, mem_ker.mp hy']

Range of Product Map Equals Product of Ranges When Kernels Span Domain

Informal description

Let $f \colon M \to M_2$ and $g \colon M \to M_3$ be linear maps over a ring $R$. If the join of their kernels spans the entire domain (i.e., $\ker f \sqcup \ker g = \top$), then the range of the product map $f \times g \colon M \to M_2 \times M_3$ is equal to the product of their ranges: \[ \operatorname{range}(f \times g) = (\operatorname{range} f) \times (\operatorname{range} g). \]

LinearMap.graph definition

: Submodule R (M × M₂)

Full source

/-- Graph of a linear map. -/
def graph : Submodule R (M × M₂) where
  carrier := { p | p.2 = f p.1 }
  add_mem' (ha : _ = _) (hb : _ = _) := by
    change _ + _ = f (_ + _)
    rw [map_add, ha, hb]
  zero_mem' := Eq.symm (map_zero f)
  smul_mem' c x (hx : _ = _) := by
    change _ • _ = f (_ • _)
    rw [map_smul, hx]

Graph of a linear map

Informal description

The graph of a linear map $f : M \to M₂$ is the submodule of $M \times M₂$ consisting of all pairs $(x, f(x))$ where $x \in M$. More formally, the graph is defined as the set $\{(x, y) \in M \times M₂ \mid y = f(x)\}$, which is closed under addition, scalar multiplication, and contains the zero vector.

LinearMap.mem_graph_iff theorem

(x : M × M₂) : x ∈ f.graph ↔ x.2 = f x.1

Full source

@[simp]
theorem mem_graph_iff (x : M × M₂) : x ∈ f.graphx ∈ f.graph ↔ x.2 = f x.1 :=
  Iff.rfl

Characterization of Graph Membership for Linear Maps

Informal description

For any element $x = (x_1, x_2) \in M \times M_2$, $x$ belongs to the graph of the linear map $f \colon M \to M_2$ if and only if $x_2 = f(x_1)$.

LinearMap.graph_eq_ker_coprod theorem

: g.graph = ker ((-g).coprod LinearMap.id)

Full source

theorem graph_eq_ker_coprod : g.graph = ker ((-g).coprod LinearMap.id) := by
  ext x
  change _ = _ ↔ -g x.1 + x.2 = _
  rw [add_comm, add_neg_eq_zero]

Graph-Kernel Equality for Linear Maps via Coproduct

Informal description

The graph of a linear map $g \colon M \to M_2$ is equal to the kernel of the coproduct linear map $(-g) \coprod \text{id} \colon M \times M_2 \to M_2$, where $\text{id}$ is the identity map on $M_2$.

LinearMap.graph_eq_range_prod theorem

: f.graph = range (LinearMap.id.prod f)

Full source

theorem graph_eq_range_prod : f.graph = range (LinearMap.id.prod f) := by
  ext x
  exact ⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩

Graph of Linear Map as Range of Product Map

Informal description

The graph of a linear map $f : M \to M_2$ is equal to the range of the product linear map $\text{id} \times f : M \to M \times M_2$, where $\text{id}$ is the identity map on $M$. In other words, the submodule $\{(x, f(x)) \mid x \in M\}$ is precisely the image of the map $x \mapsto (x, f(x))$.

LinearMap.exists_range_eq_graph theorem

 {f : G →ₛₗ[σ] H × I} (hf₁ : Surjective (Prod.fst ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
  ∃ f' : H →ₗ[S] I, LinearMap.range f = LinearMap.graph f'

Full source

/-- **Vertical line test** for linear maps.

Let `f : G → H × I` be a linear (or semilinear) map to a product. Assume that `f` is surjective on
the first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at
most once. Then the image of `f` is the graph of some linear map `f' : H → I`. -/
lemma LinearMap.exists_range_eq_graph {f : G →ₛₗ[σ] H × I} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : H →ₗ[S] I, LinearMap.range f = LinearMap.graph f' := by
  obtain ⟨f', hf'⟩ :=
    AddMonoidHom.exists_mrange_eq_mgraph (G := G) (H := H) (I := I) (f := f) hf₁ hf
  simp only [SetLike.ext_iff, AddMonoidHom.mem_mrange, AddMonoidHom.coe_coe,
    AddMonoidHom.mem_mgraph] at hf'
  use
  { toFun := f'.toFun
    map_add' := f'.map_add'
    map_smul' := by
      intro s h
      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]
      refine (hf' (s • h, _)).mp ?_
      rw [← Prod.smul_mk, ← LinearMap.mem_range]
      apply Submodule.smul_mem
      rw [LinearMap.mem_range, hf'] }
  ext x
  simpa only [mem_range, Eq.comm, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_graph_iff,
    coe_mk, AddHom.coe_mk, AddMonoidHom.coe_coe, Set.mem_range] using hf' x

Graph Representation Theorem for Surjective Semilinear Maps with Vertical Line Test

Informal description

Let $f \colon G \to H \times I$ be a semilinear map between modules over semirings with a ring homomorphism $\sigma \colon R \to S$. Suppose that: 1. The composition $\pi_1 \circ f \colon G \to H$ (where $\pi_1$ is the first projection) is surjective. 2. For any $g_1, g_2 \in G$, if $f(g_1)_1 = f(g_2)_1$ (i.e., their first components are equal), then $f(g_1)_2 = f(g_2)_2$ (their second components must also be equal). Then there exists a linear map $f' \colon H \to I$ such that the range of $f$ equals the graph of $f'$, i.e., $\text{range}(f) = \{(h, f'(h)) \mid h \in H\}$.

Submodule.exists_eq_graph theorem

{G : Submodule S (H × I)} (hf₁ : Bijective (Prod.fst ∘ G.subtype)) : ∃ f : H →ₗ[S] I, G = LinearMap.graph f

Full source

/-- **Vertical line test** for linear maps.

Let `G ≤ H × I` be a submodule of a product of modules. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some linear map `f : H →ₗ[R] I`. -/
lemma Submodule.exists_eq_graph {G : Submodule S (H × I)} (hf₁ : Bijective (Prod.fstProd.fst ∘ G.subtype)) :
    ∃ f : H →ₗ[S] I, G = LinearMap.graph f := by
  simpa only [range_subtype] using LinearMap.exists_range_eq_graph hf₁.surjective
      (fun a b h ↦ congr_arg (Prod.sndProd.snd ∘ G.subtype) (hf₁.injective h))

Graph Representation Theorem for Submodules with Bijective First Projection

Informal description

Let $G$ be a submodule of the direct product $H \times I$ of modules over a semiring $S$. If the composition of the first projection $\pi_1 \colon H \times I \to H$ with the inclusion map $G \hookrightarrow H \times I$ is bijective, then there exists a linear map $f \colon H \to I$ such that $G$ is equal to the graph of $f$, i.e., $G = \{(h, f(h)) \mid h \in H\}$.

LinearMap.exists_linearEquiv_eq_graph theorem

 {f : G →ₛₗ[σ] H × I} (hf₁ : Surjective (Prod.fst ∘ f)) (hf₂ : Surjective (Prod.snd ∘ f))
  (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ e : H ≃ₗ[S] I, range f = e.toLinearMap.graph

Full source

/-- **Line test** for module isomorphisms.

Let `f : G → H × I` be a linear (or semilinear) map to a product of modules. Assume that `f` is
surjective onto both factors and that the image of `f` intersects every "vertical line"
`{(h, i) | i : I}` and every "horizontal line" `{(h, i) | h : H}` at most once. Then the image of
`f` is the graph of some module isomorphism `f' : H ≃ I`. -/
lemma LinearMap.exists_linearEquiv_eq_graph {f : G →ₛₗ[σ] H × I} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf₂ : Surjective (Prod.sndProd.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
    ∃ e : H ≃ₗ[S] I, range f = e.toLinearMap.graph := by
  obtain ⟨e₁, he₁⟩ := f.exists_range_eq_graph hf₁ fun _ _ ↦ (hf _ _).1
  obtain ⟨e₂, he₂⟩ := ((LinearEquiv.prodComm _ _ _).toLinearMap.comp f).exists_range_eq_graph
    (by simpa) <| by simp [hf]
  have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂
    rw [Eq.comm, ← he₁ (h, i), Eq.comm, ← he₂ (i, h)]
    simp only [mem_range, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.prodComm_apply, Prod.swap_eq_iff_eq_swap, Prod.swap_prod_mk]
  exact ⟨
  { toFun := e₁
    map_smul' := e₁.map_smul'
    map_add' := e₁.map_add'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

Graph Representation Theorem for Bijective Semilinear Maps with Line Test

Informal description

Let $f \colon G \to H \times I$ be a semilinear map between modules over semirings with a ring homomorphism $\sigma \colon R \to S$. Suppose that: 1. The composition $\pi_1 \circ f \colon G \to H$ (where $\pi_1$ is the first projection) is surjective. 2. The composition $\pi_2 \circ f \colon G \to I$ (where $\pi_2$ is the second projection) is surjective. 3. For any $g_1, g_2 \in G$, the first components of $f(g_1)$ and $f(g_2)$ are equal if and only if their second components are equal. Then there exists a linear isomorphism $e \colon H \simeq I$ such that the range of $f$ equals the graph of $e$, i.e., $\text{range}(f) = \{(h, e(h)) \mid h \in H\}$.

Submodule.exists_equiv_eq_graph theorem

 {G : Submodule S (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.snd ∘ G.subtype)) :
  ∃ e : H ≃ₗ[S] I, G = e.toLinearMap.graph

Full source

/-- **Goursat's lemma** for module isomorphisms.

Let `G ≤ H × I` be a submodule of a product of modules. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some module isomorphism `f : H ≃ I`. -/
lemma Submodule.exists_equiv_eq_graph {G : Submodule S (H × I)}
    (hG₁ : Bijective (Prod.fstProd.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.sndProd.snd ∘ G.subtype)) :
    ∃ e : H ≃ₗ[S] I, G = e.toLinearMap.graph := by
  simpa only [range_subtype] using LinearMap.exists_linearEquiv_eq_graph
    hG₁.surjective hG₂.surjective fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Goursat's Lemma for Module Isomorphisms via Graph Representation

Informal description

Let $G$ be a submodule of the direct product $H \times I$ of modules over a semiring $S$. If both the composition of the first projection $\pi_1 \colon H \times I \to H$ with the inclusion map $G \hookrightarrow H \times I$ and the composition of the second projection $\pi_2 \colon H \times I \to I$ with the inclusion map are bijective, then there exists a linear isomorphism $e \colon H \simeq I$ such that $G$ is equal to the graph of $e$, i.e., $G = \{(h, e(h)) \mid h \in H\}$.

Main definitions