Skip to main content

Submodule

structure Submodule[R: Ring, M: AddCommGroup] {
    carrier: Module[R, M]
    contains: M -> Bool
} constraint {
    is_submodule(carrier, contains)
}

A submodule of a module, represented as a subset closed under the module operations.

GitHub

as_set​

define as_set(self) -> Set[M] {
    Set[M].new(self.contains)
}

The subset of module elements belonging to this submodule.

carrier​

Submodule.carrier: Submodule[R, M] -> Module[R, M]

The ambient module.

closure​

let closure: (Module[R, M], Set[M]) -> Submodule[R, M] = submodule_closure

The smallest submodule containing a set.

contains​

Submodule.contains: (Submodule[R, M], M) -> Bool

True if the given element is a member of this submodule.

ext​

let ext = submodule_ext[R, M]

Submodule extensionality from equality of ambient modules and pointwise equality of membership.

intersection​

let intersection: (Submodule[R, M], Submodule[R, M]) -> Submodule[R, M] = submodule_intersection

The common part of this submodule and another submodule.

sup​

let sup: (Submodule[R, M], Submodule[R, M]) -> Submodule[R, M] = submodule_sup

The least submodule containing this submodule and another submodule.