English
Let p ⊆ M, and let q ⊆ M₂. For a semilinear map f with a lifting hypothesis h, the image of a submodule q of M⧸p under the lifted map equals the image under f of the pulled-back submodule: q.map (p.liftQ f h) = (q.comap p.mkQ).map f.
Русский
Пусть p ⊆ M, q ⊆ M₂. При отображении f с подъёмом h, образ q через поднятое отображение равен образу f от взятого обратного образа: q.map (p.liftQ f h) = (q.comap p.mkQ).map f.
LaTeX
$$$$ q.map (p.liftQ f h) = (q.comap p.mkQ).map f. $$$$
Lean4
theorem map_liftQ [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) (q : Submodule R (M ⧸ p)) :
q.map (p.liftQ f h) = (q.comap p.mkQ).map f :=
le_antisymm (by rintro _ ⟨⟨x⟩, hxq, rfl⟩; exact ⟨x, hxq, rfl⟩)
(by rintro _ ⟨x, hxq, rfl⟩; exact ⟨Quotient.mk x, hxq, rfl⟩)
