Closed submodules of a topological module #

This files 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

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

ClosedSubmodule.instSetLike = { coe := fun (s : ClosedSubmodule R M) => ↑↑s, coe_injective' := ⋯ }

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

ClosedSubmodule.instCoeSubmodule = { coe := ClosedSubmodule.toSubmodule }

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.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

ClosedSubmodule.comap f s = { toSubmodule := Submodule.comap f ↑s, isClosed' := ⋯ }

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

ClosedSubmodule.instInf = { min := fun (s t : ClosedSubmodule R M) => { toSubmodule := ↑s ⊓ ↑t, isClosed' := ⋯ } }

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

ClosedSubmodule.instInfSet = { sInf := fun (S : Set (ClosedSubmodule R M)) => { toSubmodule := ⨅ s ∈ S, ↑s, isClosed' := ⋯ } }

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

ClosedSubmodule.instSemilatticeInf = Function.Injective.semilatticeInf ClosedSubmodule.toSubmodule ⋯ ⋯

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.instTop {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] :

Top (ClosedSubmodule R M)

Equations

ClosedSubmodule.instTop = { top := { toSubmodule := ⊤, isClosed' := ⋯ } }

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

ClosedSubmodule.instOrderBot = { bot := { toSubmodule := ⊥, isClosed' := ⋯ }, bot_le := ⋯ }

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

s.closure = { toSubmodule := s.topologicalClosure, isClosed' := ⋯ }

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

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

ClosedSubmodule.map f s = (Submodule.map f ↑s).closure

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)

Documentation

Mathlib.Topology.Algebra.Module.ClosedSubmodule

Closed submodules of a topological module #

TODO #