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

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