English
A linear equivalence between M and N that takes P to Q induces a linear equivalence between M/ P and N/ Q; the construction is functorial in composition.
Русский
Линейное эквивалентное отображение между M и N, отправляющее P в Q, индуцирует линейное эквивалентное отображение между M/ P и N/ Q; конструкция совместима с композициями.
LaTeX
$$$$ \\text{equiv} : (M/ P) \\simeq (N/ Q) $$$$
Lean4
/-- If `P` is a submodule of `M` and `Q` a submodule of `N`,
and `f : M ≃ₗ N` maps `P` to `Q`, then `M ⧸ P` is equivalent to `N ⧸ Q`. -/
@[simps]
def equiv {N : Type*} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N)
(hf : P.map f = Q) : (M ⧸ P) ≃ₗ[R] N ⧸ Q :=
{
P.mapQ Q (f : M →ₗ[R] N) fun _ hx =>
hf ▸
Submodule.mem_map_of_mem
hx with
toFun := P.mapQ Q (f : M →ₗ[R] N) fun _ hx => hf ▸ Submodule.mem_map_of_mem hx
invFun :=
Q.mapQ P (f.symm : N →ₗ[R] M) fun x hx =>
by
rw [← hf, Submodule.mem_map] at hx
obtain ⟨y, hy, rfl⟩ := hx
simpa
left_inv := fun x => Submodule.Quotient.induction_on _ x (by simp)
right_inv := fun x => Submodule.Quotient.induction_on _ x (by simp) }
