[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)
[PROOFSTEP]
rcases l.surjective_or_eq_zero with (hl | rfl)
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
hl : Function.Surjective ↑l
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)
[PROOFSTEP]
exact l.ker.isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑(ker 0) ∨ Dense ↑(ker 0)
[PROOFSTEP]
rw [LinearMap.ker_zero]
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤ ∨ Dense ↑⊤
[PROOFSTEP]
left
[GOAL]
case inr.h
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤
[PROOFSTEP]
exact isClosed_univ
