-- The subgroup generated by a subset: the intersection of all subgroups
-- containing it, with its universal property
-- 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.Generated
import Normal

def generatedSubgroup (G S : Set) : Set :=
  { x ∈ G.carrier | ∀ H, Subgroup(H, G) → S ⊆ H → x ∈ H }

theorem generatedSubgroup.subset (G S : Set)
  shows generatedSubgroup(G, S) ⊆ G.carrier
proof
  intros x hx
  have parts := generatedSubgroup.membership.forward with hx
  exact parts.left

theorem generatedSubgroup.contains (G S : Set)
  requires bounded : S ⊆ G.carrier
  shows S ⊆ generatedSubgroup(G, S)
proof
  intros x hx
  apply generatedSubgroup.membership.backward
  constructor
  . exact bounded with x, hx
  . intros H subgroup included
    exact included with x, hx

theorem generatedSubgroup.least (G S H : Set)
  requires subgroup : Subgroup(H, G)
  requires included : S ⊆ H
  shows generatedSubgroup(G, S) ⊆ H
proof
  intros x hx
  have parts := generatedSubgroup.membership.forward with hx
  exact parts.right with H, subgroup, included

theorem generatedSubgroup.mono (G S T : Set)
  requires included : S ⊆ T
  shows generatedSubgroup(G, S) ⊆ generatedSubgroup(G, T)
proof
  intros x hx
  have parts := generatedSubgroup.membership.forward with hx
  apply generatedSubgroup.membership.backward
  refine ⟨parts.left, ?_⟩
  intros H subgroup containsT
  have containsS := Subset.transitive with included, containsT
  exact parts.right with H, subgroup, containsS

theorem generatedSubgroup.eq_of_subgroup (G H : Set)
  requires subgroup : Subgroup(H, G)
  shows generatedSubgroup(G, H) = H
proof
  have bounded := Subgroup.subset with subgroup
  have includes := generatedSubgroup.contains at G, H with bounded
  have least := generatedSubgroup.least with subgroup, (Subset.reflexive at H)
  exact Subset.antisymmetric with least, includes

theorem generatedSubgroup.singleton_mem (G g : Set)
  requires bounded : g ∈ G.carrier
  shows g ∈ generatedSubgroup(G, {g})
proof
  have subset : {g} ⊆ G.carrier
    intros x hx
    have equal := singleton.membership.forward with hx
    rwa equal
  have contains := generatedSubgroup.contains at G, {g} with subset
  exact contains with g, singleton.self at g

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

theorem generatedSubgroup.subgroup (S : Set)
  shows Subgroup(generatedSubgroup(G, S), G)
proof
  have unitIn : G.one ∈ generatedSubgroup(G, S)
    apply generatedSubgroup.membership.backward
    refine ⟨(Group.one_mem with group), ?_⟩
    intros H subgroup included
    exact Subgroup.one_mem with subgroup
  apply Subgroup.mk with group, (generatedSubgroup.subset at G, S), unitIn
  . intros x hx y hy
    have px := generatedSubgroup.membership.forward with hx
    have py := generatedSubgroup.membership.forward with hy
    have xIn := px.left
    have yIn := py.left
    apply generatedSubgroup.membership.backward
    refine ⟨(Group.mul_mem with *), ?_⟩
    intros H subgroup included
    have xH := px.right with H, subgroup, included
    have yH := py.right with H, subgroup, included
    exact Subgroup.mul_mem with *
  . intros x hx
    have px := generatedSubgroup.membership.forward with hx
    have xIn := px.left
    apply generatedSubgroup.membership.backward
    refine ⟨(Group.inv_mem with *), ?_⟩
    intros H subgroup included
    have xH := px.right with H, subgroup, included
    exact Subgroup.inv_mem with *

theorem generatedSubgroup.idempotent (S : Set)
  shows generatedSubgroup(G, generatedSubgroup(G, S)) = generatedSubgroup(G, S)
proof
  have subgroup := generatedSubgroup.subgroup at G, S with group
  exact generatedSubgroup.eq_of_subgroup with subgroup

theorem generatedSubgroup.empty
  shows generatedSubgroup(G, ∅) = {G.one}
proof
  have trivial := Subgroup.trivial with group
  have least := generatedSubgroup.least with trivial, (empty.subset at {G.one})
  have subgroup := generatedSubgroup.subgroup at G, ∅ with group
  have includes := Subgroup.trivial_subset with subgroup
  exact Subset.antisymmetric with least, includes

theorem generatedSubgroup.whole
  shows generatedSubgroup(G, G.carrier) = G.carrier
proof
  have whole := Subgroup.whole with group
  exact generatedSubgroup.eq_of_subgroup with whole

theorem generatedSubgroup.one_mem (S : Set)
  shows G.one ∈ generatedSubgroup(G, S)
proof
  have subgroup := generatedSubgroup.subgroup at G, S with group
  exact Subgroup.one_mem with subgroup

theorem generatedSubgroup.pow_mem (g : G) (n : Nat)
  shows g ^ n ∈ generatedSubgroup(G, {g})
proof
  have subgroup := generatedSubgroup.subgroup at G, {g} with group
  have member : g ∈ generatedSubgroup(G, {g}) := generatedSubgroup.singleton_mem with *
  exact Subgroup.pow_mem with *

-- The join of two subgroups is generated by their union.
theorem generatedSubgroup.union_left (H K : Set)
  requires subgroupH : Subgroup(H, G)
  shows H ⊆ generatedSubgroup(G, H ∪ K)
proof
  have mono := generatedSubgroup.mono at G, H, H ∪ K with (union2.subset_left at H, K)
  have same := generatedSubgroup.eq_of_subgroup with subgroupH
  rwa same at mono

theorem generatedSubgroup.union_right (H K : Set)
  requires subgroupK : Subgroup(K, G)
  shows K ⊆ generatedSubgroup(G, H ∪ K)
proof
  have mono := generatedSubgroup.mono at G, K, H ∪ K with (union2.subset_right at H, K)
  have same := generatedSubgroup.eq_of_subgroup with subgroupK
  rwa same at mono

theorem generatedSubgroup.union_least (H K L : Set)
  requires subgroupL : Subgroup(L, G)
  requires includesH : H ⊆ L
  requires includesK : K ⊆ L
  shows generatedSubgroup(G, H ∪ K) ⊆ L
proof
  have included := union2.subset with includesH, includesK
  exact generatedSubgroup.least with subgroupL, included

end GeneratedLaws

-- The image of a generated subgroup is generated by the image.
theorem generatedSubgroup.image_subset (f G H S : Set)
  requires hom : f : G →* H
  requires bounded : S ⊆ G.carrier
  shows functionImage(f, generatedSubgroup(G, S), H.carrier) ⊆
    generatedSubgroup(H, functionImage(f, S, H.carrier))
proof
  have group := GroupHom.source with hom
  have target := GroupHom.target with hom
  have targetSubgroup := generatedSubgroup.subgroup at H, functionImage(f, S, H.carrier) with target
  have preimage := GroupHom.preimage_subgroup with hom, targetSubgroup
  have contains : S ⊆ functionPreimage(f, G.carrier, generatedSubgroup(H, functionImage(f, S, H.carrier)))
    intros x hx
    have xIn := bounded with x, hx
    have fx : f(x) ∈ H.carrier by typecheck
    have imageIn : f(x) ∈ functionImage(f, S, H.carrier)
      apply functionImage.membership.backward
      refine ⟨fx, x, hx, rfl⟩
    have generated := generatedSubgroup.contains at H, functionImage(f, S, H.carrier) with (functionImage.subset at f, S, H.carrier)
    have value := generated with f(x), imageIn
    exact functionPreimage.of_apply with xIn, value
  have least := generatedSubgroup.least with preimage, contains
  intros y hy
  obtain ⟨yIn, x, hx, yEq⟩ := functionImage.membership.forward with hy
  have inPreimage := least with x, hx
  have parts := functionPreimage.membership.forward with inPreimage
  rw yEq
  exact parts.right