-- Subgroups: subsets of a group containing the unit and closed under the
-- operation and inverses, the subgroups every group has, intersections,
-- and the one-step criterion
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Group.Subgroup
import Basic
import Set.Core

-- Subgroup(H, G): H is a subgroup of the group G. Under this hypothesis a
-- binder (h : H) is a set variable with h ∈ H, and h * k and h⁻¹ are the
-- operation and inverse of G.
predicate Subgroup (H G : Set) :=
  Group(G) ∧ H ⊆ G.carrier ∧ G.one ∈ H ∧
  (∀ x y ∈ H, x * y ∈ H) ∧ (∀ x ∈ H, x⁻¹ ∈ H)

notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis Subgroup(H, G) for H
notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis Subgroup(H, G) for H

theorem Subgroup.group (H G : Set)
  requires subgroup : Subgroup(H, G)
  shows Group(G)
proof
  obtain ⟨group, rest⟩ := subgroup
  exact group

section SubgroupLaws
variable (G H : Set)
hypothesis subgroup : Subgroup(H, G)

theorem Subgroup.subset
  shows H ⊆ G.carrier
proof
  obtain ⟨g, bounded, rest⟩ := subgroup
  exact bounded

-- Closure: the carrier membership of a subgroup element is a typing rule,
-- and the subgroup membership of a product, the unit, and an inverse are
-- instances, so each is synthesized.
theorem Subgroup.mem_carrier (h : H)
  shows h ∈ G.carrier
proof
  have bounded := Subgroup.subset with subgroup
  have hIn : h ∈ H by assumption
  exact bounded with h, hIn

instance Subgroup.one_mem
  shows G.one ∈ H
proof
  obtain ⟨g, bounded, unitIn, rest⟩ := subgroup
  exact unitIn

instance Subgroup.mul_mem (h k : H)
  shows h * k ∈ H
proof
  obtain ⟨g, bounded, unitIn, closed, inverses⟩ := subgroup
  have hIn : h ∈ H by assumption
  have kIn : k ∈ H by assumption
  exact closed with h, hIn, k, kIn

instance Subgroup.inv_mem (h : H)
  shows h⁻¹ ∈ H
proof
  obtain ⟨g, bounded, unitIn, closed, inverses⟩ := subgroup
  have hIn : h ∈ H by assumption
  exact inverses with h, hIn

theorem Subgroup.nonempty
  shows Nonempty(H)
proof
  have unitIn : G.one ∈ H := Subgroup.one_mem with *
  exact ⟨G.one, unitIn⟩

theorem Subgroup.trivial_subset
  shows {G.one} ⊆ H
proof
  intros x hx
  have equal := singleton.membership.forward with hx
  rw equal
  exact Subgroup.one_mem with *

theorem Subgroup.eq_trivial_iff
  shows H = {G.one} ↔ ∀ x ∈ H, x = G.one
proof
  have trivialSubset := Subgroup.trivial_subset with subgroup
  constructor
  . intros equal x hx
    rw equal at hx
    exact singleton.membership.forward with hx
  . intro trivial
    apply Subset.antisymmetric
    . intros x hx
      have equal := trivial with x, hx
      rw equal
      exact singleton.self
    . exact trivialSubset

end SubgroupLaws

section SubgroupCancellation
variable (G H : Set)
hypothesis group : Group(G)
hypothesis subgroup : Subgroup(H, G)

-- Membership in a subgroup is unchanged by a factor from the subgroup.
theorem Subgroup.mul_mem_cancel_left (h : H) (x : G)
  shows h * x ∈ H ↔ x ∈ H
proof
  constructor
  . intro member
    have product : h⁻¹ * (h * x) ∈ H := Subgroup.mul_mem with *
    rwa inv_mul_cancel_left at product
  . intro member
    exact Subgroup.mul_mem with *

theorem Subgroup.mul_mem_cancel_right (h : H) (x : G)
  shows x * h ∈ H ↔ x ∈ H
proof
  constructor
  . intro member
    have product : x * h * h⁻¹ ∈ H := Subgroup.mul_mem with *
    rwa mul_inv_cancel_right at product
  . intro member
    exact Subgroup.mul_mem with *

theorem Subgroup.inv_mem_iff (x : G)
  shows x⁻¹ ∈ H ↔ x ∈ H
proof
  constructor
  . intro member
    have twice : (x⁻¹)⁻¹ ∈ H := Subgroup.inv_mem with *
    rwa inv_inv at twice
  . intro member
    exact Subgroup.inv_mem with *

end SubgroupCancellation

section SubgroupConstructions
variable (G : Set)
hypothesis group : Group(G)

-- The constructor.
theorem Subgroup.mk (H : Set)
  requires bounded : H ⊆ G
  requires unitIn : G.one ∈ H
  requires closed : ∀ x y ∈ H, x * y ∈ H
  requires inverses : ∀ x ∈ H, x⁻¹ ∈ H
  shows Subgroup(H, G)
proof
  unfold Subgroup
  refine ⟨group, bounded, unitIn, closed, inverses⟩

-- The subgroups every group has.
theorem Subgroup.whole
  shows Subgroup(G.carrier, G)
proof
  have reflexive := Subset.reflexive at G.carrier
  have unitIn : G.one ∈ G := Group.one_mem with *
  apply Subgroup.mk with group, reflexive, unitIn
  . intros x hx y hy
    exact Group.mul_mem with *
  . intros x hx
    exact Group.inv_mem with *

theorem Subgroup.trivial
  shows Subgroup({G.one}, G)
proof
  have unitIn : G.one ∈ G := Group.one_mem with *
  have selfIn := singleton.self at G.one
  have bounded : {G.one} ⊆ G
    intros x hx
    have equal := singleton.membership.forward with hx
    rwa equal
  apply Subgroup.mk with group, bounded, selfIn
  . intros x hx y hy
    have ex := singleton.membership.forward with hx
    have ey := singleton.membership.forward with hy
    rw [ex, ey, one_mul]
    exact selfIn
  . intros x hx
    have ex := singleton.membership.forward with hx
    rw [ex, inv_one]
    exact selfIn

theorem Subgroup.intersection (H K : Set)
  requires subgroupH : Subgroup(H, G)
  requires subgroupK : Subgroup(K, G)
  shows Subgroup(H ∩ K, G)
proof
  have bounded := Subset.transitive with (intersection.subset_left at H, K), (Subgroup.subset with subgroupH)
  have unitIn : G.one ∈ H ∩ K := intersection.membership.backward with ⟨(Subgroup.one_mem with subgroupH), (Subgroup.one_mem with subgroupK)⟩
  apply Subgroup.mk with group, bounded, unitIn
  . intros x hx y hy
    obtain ⟨xH, xK⟩ := intersection.membership.forward with hx
    obtain ⟨yH, yK⟩ := intersection.membership.forward with hy
    exact intersection.membership.backward with ⟨(Subgroup.mul_mem with *), (Subgroup.mul_mem with *)⟩
  . intros x hx
    obtain ⟨xH, xK⟩ := intersection.membership.forward with hx
    exact intersection.membership.backward with ⟨(Subgroup.inv_mem with *), (Subgroup.inv_mem with *)⟩

-- The one-step subgroup criterion: a nonempty subset closed under
-- x, y ↦ x * y⁻¹ is a subgroup.
theorem Subgroup.of_mul_inv (H : Set)
  requires bounded : H ⊆ G
  requires inhabited : Nonempty(H)
  requires closed : ∀ x y ∈ H, x * y⁻¹ ∈ H
  shows Subgroup(H, G)
proof
  obtain ⟨h, hH⟩ := inhabited
  have hIn := bounded with h, hH
  have unitIn : G.one ∈ H
    have product := closed with h, hH, h, hH
    rwa Group.mul_inv at product
  have inverses : ∀ x ∈ H, x⁻¹ ∈ H
    intros x hx
    have xIn := bounded with x, hx
    have product := closed with G.one, unitIn, x, hx
    rwa one_mul at product
  apply Subgroup.mk with group, bounded, unitIn
  . intros x hx y hy
    have yIn := bounded with y, hy
    have invY := inverses with y, hy
    have product := closed with x, hx, y⁻¹, invY
    rwa inv_inv at product
  . exact inverses

end SubgroupConstructions