instance AlgebraInLean.subgroupOrder {G : Type u_1} [AlgebraInLean.Group G] : PartialOrder (AlgebraInLean.Subgroup G)

⊆ defines a partial order on the subgroups of G

Equations

• AlgebraInLean.subgroupOrder = PartialOrder.mk ⋯

theorem AlgebraInLean.Minimal_smallest {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : AlgebraInLean.Minimal G ≤ H

Let H ≤ G. Then, Minimal G ≤ H

theorem AlgebraInLean.Maximal_largest {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : H ≤ AlgebraInLean.Maximal G

Let H ≤ G. Then, H ≤ Minimal G

def AlgebraInLean.Intersect {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) (K : AlgebraInLean.Subgroup G) : AlgebraInLean.Subgroup G

The intersection of two subgroups is itself a subgroup. Prove this by completing the definition below.

Equations

• AlgebraInLean.Intersect H K = { carrier := ↑H ∩ ↑K, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

instance AlgebraInLean.instInterSubgroup {G : Type u_1} [AlgebraInLean.Group G] : Inter (AlgebraInLean.Subgroup G)

This allows us to use the H ∩ K notation.

Equations

• AlgebraInLean.instInterSubgroup = { inter := AlgebraInLean.Intersect }

theorem AlgebraInLean.subgroup_eq_Maximal_of_card_eq_G {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) [Fintype G] [Fintype ↑↑H] (h : Fintype.card G = Fintype.card ↑↑H) : H = AlgebraInLean.Maximal G

If G is a finite group, and H is a subgroup of G with |H| = |G|, then H = G. This will become important as we move into our discussion of generators and cyclic subgroups.

hint: consider the theorem set_fintype_card_eq_univ_iff defined in Mathlib.

theorem AlgebraInLean.inter_comm {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) (K : AlgebraInLean.Subgroup G) : H ∩ K = K ∩ H

∩ is commutative

theorem AlgebraInLean.inter_assoc {G : Type u_1} [AlgebraInLean.Group G] (H₁ : AlgebraInLean.Subgroup G) (H₂ : AlgebraInLean.Subgroup G) (H₃ : AlgebraInLean.Subgroup G) : H₁ ∩ H₂ ∩ H₃ = H₁ ∩ (H₂ ∩ H₃)

∩ is associative

theorem AlgebraInLean.le_intersect_self {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) (K : AlgebraInLean.Subgroup G) : H ∩ K ≤ H

def AlgebraInLean.Generate {G : Type u_1} [AlgebraInLean.Group G] (S : Set G) : AlgebraInLean.Subgroup G

The subgroup generated by a subset S is defined to be the smallest subgroup that contains all of S. This definition is equivalent to the intersection of all subgroups containing S.

Equations

• AlgebraInLean.Generate S = { carrier := {g : G | ∀ (H : AlgebraInLean.Subgroup G), S ⊆ ↑H → g ∈ H}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

theorem AlgebraInLean.Generate_empty {G : Type u_1} [AlgebraInLean.Group G] : AlgebraInLean.Generate ∅ = AlgebraInLean.Minimal G

The subgroup generated by ∅ is the minimal subgroup

theorem AlgebraInLean.Generate_contain_set {G : Type u_1} [AlgebraInLean.Group G] (S : Set G) : S ⊆ ↑(AlgebraInLean.Generate S)

S is a subset of the subgroup generated by S

theorem AlgebraInLean.Generate_self_eq_self {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : AlgebraInLean.Generate ↑H = H

Let H be a subgroup. The subgroup generated by H is H

theorem AlgebraInLean.Generate_smallest_closure {G : Type u_1} [AlgebraInLean.Group G] (S : Set G) (H : AlgebraInLean.Subgroup G) : S ⊆ ↑H ∧ H ≤ AlgebraInLean.Generate S → H = AlgebraInLean.Generate S

If S is a subset of H and H is a subgroup of the subgroup generated by S, then, H is equal to the subgroup generated by S

def AlgebraInLean.Pows {G : Type u_1} [AlgebraInLean.Group G] (x : G) : AlgebraInLean.Subgroup G

This subgroup is the set of all group elements that can be written as the power of some x in the group.

Equations

• AlgebraInLean.Pows x = { carrier := {g : G | ∃ (a : ℤ), AlgebraInLean.gpow x a = g}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

theorem AlgebraInLean.Pows_contain_self {G : Type u_1} [AlgebraInLean.Group G] (x : G) : x ∈ AlgebraInLean.Pows x

x is a power of itself

theorem AlgebraInLean.Pows_eq_Generate_singleton {G : Type u_1} [AlgebraInLean.Group G] (x : G) : AlgebraInLean.Pows x = AlgebraInLean.Generate {x}

This is an important theorem in relating the Generate subgroup, the powers of an element, and the cyclic group.

def AlgebraInLean.gpowMap {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℤ) : ↑↑(AlgebraInLean.Pows x)

Equations

• AlgebraInLean.gpowMap x n = ⟨AlgebraInLean.gpow x n, ⋯⟩

def AlgebraInLean.finPowMap {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℕ) (k : Fin n) : ↑↑(AlgebraInLean.Pows x)

Equations

• AlgebraInLean.finPowMap x n k = AlgebraInLean.gpowMap x ↑↑k

theorem AlgebraInLean.gpowMap_bijective_of_order_zero {G : Type u_1} [AlgebraInLean.Group G] {x : G} (h : AlgebraInLean.order x = 0) : AlgebraInLean.Bijective (AlgebraInLean.gpowMap x)

theorem AlgebraInLean.finPowMap_order_bijective {G : Type u_1} [AlgebraInLean.Group G] {x : G} (h : AlgebraInLean.order x ≠ 0) : AlgebraInLean.Bijective (AlgebraInLean.finPowMap x (AlgebraInLean.order x))

theorem AlgebraInLean.Pows_card_eq_order {G : Type u_1} [AlgebraInLean.Group G] (x : G) : Nat.card ↑↑(AlgebraInLean.Pows x) = AlgebraInLean.order x

theorem AlgebraInLean.Pows_iso_Int_of_zero_order {G : Type u_1} [AlgebraInLean.Group G] {x : G} (hx : AlgebraInLean.order x = 0) : ∃ (φ : ℤ → ↑↑(AlgebraInLean.Pows x)), AlgebraInLean.Isomorphism φ

theorem AlgebraInLean.Pows_iso_Cn_order {G : Type u_1} [AlgebraInLean.Group G] (x : G) [h : NeZero (AlgebraInLean.order x)] : ∃ (φ : Fin (AlgebraInLean.order x) → ↑↑(AlgebraInLean.Pows x)), AlgebraInLean.Isomorphism φ