Cyclic sublattices of abelian groups

DefinitionCyclic sublattice of a subgroup#✓fully proved

Let \(A\) be an abelian group and let \(L'\) and \(L\) be subgroups of \(A\). Then \(L'\) is a cyclic sublattice of \(L\) when \(L' \subseteq L\) and the quotient group \(L/L'\) is cyclic; formally the quotient is taken by \(L' \cap L\), regarded as a subgroup of \(L\).

def IsCyclicSublattice (L' L : AddSubgroup A) : Prop :=
  L' ≤ L ∧ IsAddCyclic (L ⧸ L'.addSubgroupOf L)

Used by 4

Used byThe quotient by a cyclic sublattice is cyclic · Characterization of cyclic sublattices · A cyclic sublattice is contained in its ambient subgroup · Criterion for a cyclic sublattice

TheoremCharacterization of cyclic sublattices#✓fully proved

Let \(L'\) and \(L\) be subgroups of an abelian group \(A\). Then \(L'\) is a cyclic sublattice of \(L\) if and only if \(L' \subseteq L\) and the quotient group \(L/(L' \cap L)\), with \(L' \cap L\) regarded as a subgroup of \(L\), is cyclic.

theorem isCyclicSublattice_iff {L' L : AddSubgroup A} :
    IsCyclicSublattice L' L ↔
      L' ≤ L ∧ IsAddCyclic (L ⧸ L'.addSubgroupOf L)

Uses 1

Statement usesCyclic sublattice of a subgroup

TheoremA cyclic sublattice is contained in its ambient subgroup#✓fully proved

Let \(L'\) and \(L\) be subgroups of an abelian group \(A\). If \(L'\) is a cyclic sublattice of \(L\), then \(L' \subseteq L\).

theorem IsCyclicSublattice.le {L' L : AddSubgroup A}
    (h : IsCyclicSublattice L' L) : L' ≤ L

Uses 1

Statement usesCyclic sublattice of a subgroup

TheoremThe quotient by a cyclic sublattice is cyclic#✓fully proved

Let \(L'\) and \(L\) be subgroups of an abelian group \(A\). If \(L'\) is a cyclic sublattice of \(L\), then the quotient group \(L/L'\) is cyclic.

theorem IsCyclicSublattice.isAddCyclic_quotient {L' L : AddSubgroup A}
    (h : IsCyclicSublattice L' L) :
    IsAddCyclic (L ⧸ L'.addSubgroupOf L)

Uses 1

Statement usesCyclic sublattice of a subgroup

TheoremCriterion for a cyclic sublattice#✓fully proved

Let \(L'\) and \(L\) be subgroups of an abelian group \(A\). If \(L' \subseteq L\) and the quotient group \(L/L'\) is cyclic, then \(L'\) is a cyclic sublattice of \(L\).

theorem IsCyclicSublattice.mk {L' L : AddSubgroup A} (hle : L' ≤ L)
    (hcyc : IsAddCyclic (L ⧸ L'.addSubgroupOf L)) :
    IsCyclicSublattice L' L

Uses 1

Statement usesCyclic sublattice of a subgroup

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.