no goals
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
inst✝¹ : IsArtinian R M
inst✝ : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ↑f
hg : Function.Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), Submodule.map f (Submodule.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 u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
inst✝¹ : IsArtinian R M
inst✝ : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ↑f
hg : Function.Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), Submodule.comap g (Submodule.map g a) = a ⊔ LinearMap.range f
simp [Submodule.comap_map_eq, h]