Compact submodules #
theorem
Submodule.isCompact_of_fg
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[TopologicalSpace R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
[ContinuousAdd M]
[ContinuousSMul R M]
[CompactSpace R]
{N : Submodule R M}
(hN : N.FG)
:
IsCompact ↑N
theorem
Ideal.isCompact_of_fg
{R : Type u_1}
[CommSemiring R]
[TopologicalSpace R]
[IsTopologicalSemiring R]
[CompactSpace R]
{I : Ideal R}
(hI : I.FG)
:
IsCompact ↑I
theorem
Module.Finite.compactSpace
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[TopologicalSpace R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
[ContinuousAdd M]
[ContinuousSMul R M]
[CompactSpace R]
[Module.Finite R M]
:
@[instance 100]
instance
IsNoetherianRing.isClosed_ideal
{R : Type u_3}
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
[IsNoetherianRing R]
[CompactSpace R]
[T2Space R]
(I : Ideal R)
:
IsClosed ↑I