Closed submodules of a topological module #

This file builds the frame of closed R-submodules of a topological module M.

One can turn s : Submodule R E + hs : IsClosed s into s : ClosedSubmodule R E in a tactic block by doing lift s to ClosedSubmodule R E using hs.

TODO #

Actually provide the Order.Frame (ClosedSubmodule R M) instance.

source

structure ClosedSubmodule (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] extends Submodule R M, TopologicalSpace.Closeds M :

Type u_3

The type of closed submodules of a topological module.

carrier : Set M
add_mem' {a b : M} : a ∈ (↑self).carrier → b ∈ (↑self).carrier → a + b ∈ (↑self).carrier
zero_mem' : 0 ∈ (↑self).carrier
smul_mem' (c : R) {x : M} : x ∈ (↑self).carrier → c • x ∈ (↑self).carrier
isClosed' : IsClosed (↑self).carrier

Instances For

source

theorem ClosedSubmodule.ext {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : TopologicalSpace M} {inst✝³ : Module R M} {x y : ClosedSubmodule R M} (carrier : (↑x).carrier = (↑y).carrier) :

x = y

source

theorem ClosedSubmodule.ext_iff {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : TopologicalSpace M} {inst✝³ : Module R M} {x y : ClosedSubmodule R M} :

x = y ↔ (↑x).carrier = (↑y).carrier

source

theorem ClosedSubmodule.toSubmodule_injective {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

Function.Injective toSubmodule

source

instance ClosedSubmodule.instSetLike {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

SetLike (ClosedSubmodule R M) M

Equations

source

instance ClosedSubmodule.instPartialOrder {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

PartialOrder (ClosedSubmodule R M)

Equations

source

theorem ClosedSubmodule.toCloseds_injective {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

Function.Injective toCloseds

source

instance ClosedSubmodule.instAddSubmonoidClass {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

AddSubmonoidClass (ClosedSubmodule R M) M

source

instance ClosedSubmodule.instSMulMemClass {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

SMulMemClass (ClosedSubmodule R M) R M

source

instance ClosedSubmodule.instCoeSubmodule {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

Coe (ClosedSubmodule R M) (Submodule R M)

Equations

source

@[simp]

theorem ClosedSubmodule.carrier_eq_coe {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s : ClosedSubmodule R M) :

(↑s).carrier = ↑s

source

@[simp]

theorem ClosedSubmodule.mem_mk {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {x : M} {s : Submodule R M} {hs : IsClosed s.carrier} :

x ∈ { toSubmodule := s, isClosed' := hs } ↔ x ∈ s

source

@[simp]

theorem ClosedSubmodule.coe_toSubmodule {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s : ClosedSubmodule R M) :

↑↑s = ↑s

source

@[simp]

theorem ClosedSubmodule.mem_toSubmodule_iff {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (x : M) (s : ClosedSubmodule R M) :

x ∈ ↑s ↔ x ∈ s

source

@[simp]

theorem ClosedSubmodule.coe_toCloseds {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s : ClosedSubmodule R M) :

↑↑s = ↑s

source

theorem ClosedSubmodule.isClosed {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s : ClosedSubmodule R M) :

IsClosed ↑s

source

instance ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

CanLift (Submodule R M) (ClosedSubmodule R M) toSubmodule fun (x : Submodule R M) => IsClosed ↑x

source

@[simp]

theorem ClosedSubmodule.toSubmodule_le_toSubmodule {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {s t : ClosedSubmodule R M} :

↑s ≤ ↑t ↔ s ≤ t

source

def ClosedSubmodule.comap {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] (f : M →L[R] N) (s : ClosedSubmodule R N) :

ClosedSubmodule R M

The preimage of a closed submodule under a continuous linear map as a closed submodule.

Equations

Instances For

source

@[simp]

theorem ClosedSubmodule.coe_comap {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] (f : M →L[R] N) (s : ClosedSubmodule R N) :

↑(comap f s) = ⇑f ⁻¹' ↑s

source

@[simp]

theorem ClosedSubmodule.mem_comap {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] {f : M →L[R] N} {s : ClosedSubmodule R N} {x : M} :

x ∈ comap f s ↔ f x ∈ s

source

@[simp]

theorem ClosedSubmodule.toSubmodule_comap {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] (f : M →L[R] N) (s : ClosedSubmodule R N) :

↑(comap f s) = Submodule.comap ↑f ↑s

source

@[simp]

theorem ClosedSubmodule.comap_id {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s : ClosedSubmodule R M) :

comap (ContinuousLinearMap.id R M) s = s

source

theorem ClosedSubmodule.comap_comap {R : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [AddCommMonoid O] [TopologicalSpace O] [Module R O] (g : N →L[R] O) (f : M →L[R] N) (s : ClosedSubmodule R O) :

comap f (comap g s) = comap (g.comp f) s

source

instance ClosedSubmodule.instInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

Min (ClosedSubmodule R M)

Equations

source

instance ClosedSubmodule.instInfSet {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

InfSet (ClosedSubmodule R M)

Equations

source

@[simp]

theorem ClosedSubmodule.toSubmodule_sInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (S : Set (ClosedSubmodule R M)) :

↑(sInf S) = ⨅ s ∈ S, ↑s

source

@[simp]

theorem ClosedSubmodule.toSubmodule_iInf {ι : Sort u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (f : ι → ClosedSubmodule R M) :

↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

source

@[simp]

theorem ClosedSubmodule.coe_sInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (S : Set (ClosedSubmodule R M)) :

↑(sInf S) = ⨅ s ∈ S, ↑s

source

@[simp]

theorem ClosedSubmodule.coe_iInf {ι : Sort u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (f : ι → ClosedSubmodule R M) :

↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

source

@[simp]

theorem ClosedSubmodule.mem_sInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {x : M} {S : Set (ClosedSubmodule R M)} :

x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

source

@[simp]

theorem ClosedSubmodule.mem_iInf {ι : Sort u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {x : M} {f : ι → ClosedSubmodule R M} :

x ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), x ∈ f i

source

instance ClosedSubmodule.instSemilatticeInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

SemilatticeInf (ClosedSubmodule R M)

Equations

source

@[simp]

theorem ClosedSubmodule.toSubmodule_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s t : ClosedSubmodule R M) :

↑(s ⊓ t) = ↑s ⊓ ↑t

source

@[simp]

theorem ClosedSubmodule.coe_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s t : ClosedSubmodule R M) :

↑(s ⊓ t) = ↑s ⊓ ↑t

source

@[simp]

theorem ClosedSubmodule.mem_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {s t : ClosedSubmodule R M} {x : M} :

x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

source

instance ClosedSubmodule.instCompleteSemilatticeInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

CompleteSemilatticeInf (ClosedSubmodule R M)

Equations

source

instance ClosedSubmodule.instOrderTop {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

OrderTop (ClosedSubmodule R M)

Equations

source

@[simp]

theorem ClosedSubmodule.toSubmodule_top {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

↑⊤ = ⊤

source

@[simp]

theorem ClosedSubmodule.coe_top {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

↑⊤ = Set.univ

source

@[simp]

theorem ClosedSubmodule.mem_top {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {x : M} :

x ∈ ⊤

source

instance ClosedSubmodule.instOrderBot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [T1Space M] :

OrderBot (ClosedSubmodule R M)

Equations

source

@[simp]

theorem ClosedSubmodule.toSubmodule_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [T1Space M] :

↑⊥ = ⊥

source

@[simp]

theorem ClosedSubmodule.coe_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [T1Space M] :

↑⊥ = {0}

source

@[simp]

theorem ClosedSubmodule.mem_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {x : M} [T1Space M] :

x ∈ ⊥ ↔ x = 0

source

def Submodule.closure {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] (s : Submodule R M) :

ClosedSubmodule R M

The closure of a submodule as a closed submodule.

Equations

Instances For

source

@[simp]

theorem Submodule.coe_closure {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] (s : Submodule R M) :

↑s.closure = closure ↑s

source

@[simp]

theorem Submodule.closure_le {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] {s : Submodule R M} {t : ClosedSubmodule R M} :

s.closure ≤ t ↔ s ≤ ↑t

source

@[simp]

theorem Submodule.mem_closure_iff {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] {x : M} {s : Submodule R M} :

x ∈ s.closure ↔ x ∈ s.topologicalClosure

source

@[simp]

theorem Submodule.closure_eq {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] {s : ClosedSubmodule R M} :

(↑s).closure = s

source

theorem Submodule.closure_eq' {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] {s : Submodule R M} (hs : IsClosed s.carrier) :

s.closure = { toSubmodule := s, isClosed' := hs }

source

theorem ClosedSubmodule.closure_toSubmodule_eq {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {s : ClosedSubmodule R N} :

(↑s).closure = s

source

def ClosedSubmodule.map {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : M →L[R] N) (s : ClosedSubmodule R M) :

ClosedSubmodule R N

The closure of the image of a closed submodule under a continuous linear map is a closed submodule.

ClosedSubmodule.map f is left-adjoint to ClosedSubmodule.comap f. See ClosedSubmodule.gc_map_comap.

Equations

Instances For

source

@[simp]

theorem ClosedSubmodule.map_id {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] (s : ClosedSubmodule R M) :

map (ContinuousLinearMap.id R M) s = s

source

theorem ClosedSubmodule.map_le_iff_le_comap {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {f : M →L[R] N} {s : ClosedSubmodule R M} {t : ClosedSubmodule R N} :

map f s ≤ t ↔ s ≤ comap f t

source

theorem ClosedSubmodule.gc_map_comap {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {f : M →L[R] N} :

GaloisConnection (map f) (comap f)

source

instance ClosedSubmodule.instMax {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] :

Max (ClosedSubmodule R N)

Equations

source

@[simp]

theorem ClosedSubmodule.toSubmodule_sup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {s t : ClosedSubmodule R N} :

↑(s ⊔ t) = ↑(↑s ⊔ ↑t).closure

source

@[simp]

theorem ClosedSubmodule.coe_sup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {s t : ClosedSubmodule R N} :

↑(s ⊔ t) = closure (↑s ⊔ ↑t).carrier

source

@[simp]

theorem ClosedSubmodule.mem_sup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {s t : ClosedSubmodule R N} {x : N} :

x ∈ s ⊔ t ↔ x ∈ closure (↑s ⊔ ↑t).carrier

source

instance ClosedSubmodule.instSupSet {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] :

SupSet (ClosedSubmodule R N)

Equations

source

@[simp]

theorem ClosedSubmodule.toSubmodule_sSup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (S : Set (ClosedSubmodule R N)) :

↑(sSup S) = ↑(⨆ s ∈ S, ↑s).closure

source

@[simp]

theorem ClosedSubmodule.toSubmodule_iSup {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : ι → ClosedSubmodule R N) :

↑(⨆ (i : ι), f i) = ↑(⨆ (i : ι), ↑(f i)).closure

source

@[simp]

theorem ClosedSubmodule.coe_sSup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (S : Set (ClosedSubmodule R N)) :

↑(sSup S) = closure (⨆ s ∈ S, ↑s).carrier

source

@[simp]

theorem ClosedSubmodule.coe_iSup {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : ι → ClosedSubmodule R N) :

↑(⨆ (i : ι), f i) = closure (⨆ (i : ι), ↑(f i)).carrier

source

@[simp]

theorem ClosedSubmodule.mem_sSup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {x : N} {S : Set (ClosedSubmodule R N)} :

x ∈ sSup S ↔ x ∈ closure (⨆ s ∈ S, ↑s).carrier

source

@[simp]

theorem ClosedSubmodule.mem_iSup {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {x : N} {f : ι → ClosedSubmodule R N} :

x ∈ ⨆ (i : ι), f i ↔ x ∈ closure (⨆ (i : ι), ↑(f i)).carrier

source

instance ClosedSubmodule.instSemilatticeSup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] :

SemilatticeSup (ClosedSubmodule R N)

Equations

source

instance ClosedSubmodule.instCompleteSemilatticeSup {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] :

CompleteSemilatticeSup (ClosedSubmodule R N)

Equations

source

instance ClosedSubmodule.instLattice {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] :

Lattice (ClosedSubmodule R N)

Equations

source

instance ClosedSubmodule.instCompleteLatticeOfT1Space {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] [T1Space N] :

CompleteLattice (ClosedSubmodule R N)

Equations

source

instance instCompleteSpaceSubtypeMemClosedSubmodule {𝕜 : Type u_6} {H : Type u_7} [Semiring 𝕜] [AddCommMonoid H] [UniformSpace H] [Module 𝕜 H] [CompleteSpace H] (K : ClosedSubmodule 𝕜 H) :

CompleteSpace ↥K

Documentation

Mathlib.Topology.Algebra.Module.ClosedSubmodule

Closed submodules of a topological module #

TODO #