Intersections of subgroups of abelian groups

Content created by Fredrik Bakke, Egbert Rijke and Maša Žaucer

Created on 2023-06-08.
Last modified on 2023-06-28.

module group-theory.intersections-subgroups-abelian-groups where
Imports 
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.intersections-subgroups-groups
open import group-theory.subgroups-abelian-groups

Idea

The intersection of two subgroups of an abelian group A consists of the elements contained in both subgroups.

Definition

module _
  {l1 l2 l3 : Level} (A : Ab l1) (B : Subgroup-Ab l2 A) (C : Subgroup-Ab l3 A)
  where

  intersection-Subgroup-Ab : Subgroup-Ab (l2 ⊔ l3) A
  intersection-Subgroup-Ab = intersection-Subgroup (group-Ab A) B C

  subset-intersection-Subgroup-Ab : subtype (l2 ⊔ l3) (type-Ab A)
  subset-intersection-Subgroup-Ab =
    subset-intersection-Subgroup (group-Ab A) B C

  is-in-intersection-Subgroup-Ab : type-Ab A → UU (l2 ⊔ l3)
  is-in-intersection-Subgroup-Ab =
    is-in-intersection-Subgroup (group-Ab A) B C

  contains-zero-intersection-Subgroup-Ab :
    contains-zero-subset-Ab A subset-intersection-Subgroup-Ab
  contains-zero-intersection-Subgroup-Ab =
    contains-unit-intersection-Subgroup (group-Ab A) B C

  is-closed-under-add-intersection-Subgroup-Ab :
    is-closed-under-add-subset-Ab A subset-intersection-Subgroup-Ab
  is-closed-under-add-intersection-Subgroup-Ab =
    is-closed-under-multiplication-intersection-Subgroup (group-Ab A) B C

  is-closed-under-neg-intersection-Subgroup-Ab :
    is-closed-under-neg-subset-Ab A subset-intersection-Subgroup-Ab
  is-closed-under-neg-intersection-Subgroup-Ab =
    is-closed-under-inv-intersection-Subgroup (group-Ab A) B C

  is-subgroup-intersection-Subgroup-Ab :
    is-subgroup-Ab A subset-intersection-Subgroup-Ab
  is-subgroup-intersection-Subgroup-Ab =
    is-subgroup-intersection-Subgroup (group-Ab A) B C

Recent changes