English
Let p1 ⊆ M, p2 ⊆ M′ be submodules and q ⊆ M × M′ a submodule. Then q ≤ p1.prod p2 if and only if the images of q under the two projections satisfy q mapped along fst is contained in p1 and q mapped along snd is contained in p2.
Русский
Пусть p1 ⊆ M и p2 ⊆ M′ — подмодули, q ⊆ M × M′ — подмодуль. Тогда q ≤ p1.prod p2 тогда и только тогда, когда образ q по проекции fst лежит в p1, а образ q по проекции snd лежит в p2.
LaTeX
$$$q \le p_1.\mathrm{prod} p_2 \iff \mathrm{map}(\mathrm{LinearMap.fst}\ R M M_2) \, q \le p_1 \;\wedge\; \mathrm{map}(\mathrm{LinearMap.snd}\ R M M_2) \, q \le p_2$$$
Lean4
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⟩⟩
