English
Let p1 ⊆ M, p2 ⊆ M′, q ⊆ M × M′ be submodules. Then p1.prod p2 ≤ q if and only if the images under the inl and inr maps are contained in q.
Русский
Пусть p1 ⊆ M, p2 ⊆ M′, q ⊆ M × M′ — подмодули. Тогда p1.prod p2 ≤ q тогда и только тогда, когда образ подмодуля p1 по инл и образ p2 по инр лежат внутри q.
LaTeX
$$$p_1.\mathrm{prod} p_2 \le q \iff \mathrm{map}(\mathrm{LinearMap.inl}\ R M M_2)\, p_1 \le q \land \mathrm{map}(\mathrm{LinearMap.inr}\ R M M_2)\, p_2 \le q$$$
Lean4
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'
