English
If P ≤ M and Q ≤ N are submodules and f: M ≃ₗ[R] N is a linear equivalence mapping P to Q, then the induced quotient equivalence (M ⧸ P) ≃ₗ[R] (N ⧸ Q) exists.
Русский
Если P ⊆ M и Q ⊆ N — подмодули и f: M ≃ₗ[R] N линейное взаимно однозначное отображение, переводящее P в Q, то существует эквивалентность фактор‑модулей (M ⧸ P) ≃ₗ[R] (N ⧸ Q).
LaTeX
$$$$ (M ⧸ P) \\simeq (N ⧸ Q) $$$$
Lean4
theorem span_preimage_eq [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty) (h₁ : s ⊆ range f) :
span R (f ⁻¹' s) = (span R₂ s).comap f :=
by
suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this
have hk : ker f ≤ span R (f ⁻¹' s) := by
let y := Classical.choose h₀
have hy : y ∈ s := Classical.choose_spec h₀
rw [ker_le_iff]
use y, h₁ hy
rw [← Set.singleton_subset_iff] at hy
exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
rw [← left_eq_sup] at hk
rw [coe_range f] at h₁
rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]
exact inf_le_right
