Intersections of subgroups of abelian groups

Content created by Fredrik Bakke, Egbert Rijke, Maša Žaucer and Gregor Perčič.

Created on 2023-06-08.
Last modified on 2023-09-21.

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-addition-intersection-Subgroup-Ab :
    is-closed-under-addition-subset-Ab A subset-intersection-Subgroup-Ab
  is-closed-under-addition-intersection-Subgroup-Ab =
    is-closed-under-multiplication-intersection-Subgroup (group-Ab A) B C

  is-closed-under-negatives-intersection-Subgroup-Ab :
    is-closed-under-negatives-subset-Ab A subset-intersection-Subgroup-Ab
  is-closed-under-negatives-intersection-Subgroup-Ab =
    is-closed-under-inverses-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