no goals
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Injective ↑f
hg : Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), map f (comap f a) = a ⊓ LinearMap.range f
simp [Submodule.map_comap_eq, inf_comm]
no goals
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Injective ↑f
hg : Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), comap g (map g a) = a ⊔ LinearMap.range f
simp [Submodule.comap_map_eq, h]