Subsets of abelian groups
Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.
Created on 2023-06-08.
Last modified on 2023-06-08.
module group-theory.subsets-abelian-groups where
Imports
open import foundation.sets open import foundation.universe-levels open import group-theory.abelian-groups open import group-theory.subsets-groups
Idea
A subset of an abelian group A
is a
subtype of the underlying type of A
.
Definitions
Subsets of abelian groups
subset-Ab : (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1) subset-Ab l A = subset-Group l (group-Ab A) is-set-subset-Ab : (l : Level) {l1 : Level} (A : Ab l1) → is-set (subset-Ab l A) is-set-subset-Ab l A = is-set-subset-Group (group-Ab A)
Recent changes
- 2023-06-08. Egbert Rijke, Maša Žaucer and Fredrik Bakke. The Zariski locale of a commutative ring (#619).