-- A subgroup as a group of its own, with the operations restricted to it;
-- the inclusion of a subgroup is a homomorphism, and homomorphisms restrict
-- to subgroups and corestrict to their images
-- 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.Restricted
import Normal
import Algebra.Restriction

-- The group on a subgroup H of G: the carrier H with the operation and
-- inverse of G restricted to it.
def subgroupGroup (G H : Set) : Set :=
  Group.mk(H, restrict(G.mul, H × H), G.one, restrict(G.inv, H))

theorem subgroupGroup.carrierOf (G H : Set)
  shows Group.carrier(subgroupGroup(G, H)) = H
proof
  simp [subgroupGroup, Group.mk.carrier]

theorem subgroupGroup.operation (G H : Set)
  shows Group.mul(subgroupGroup(G, H)) = restrict(G.mul, H × H)
proof
  simp [subgroupGroup, Group.mk.mul]

theorem subgroupGroup.unit (G H : Set)
  shows Group.one(subgroupGroup(G, H)) = G.one
proof
  simp [subgroupGroup, Group.mk.one]

theorem subgroupGroup.inverse (G H : Set)
  shows Group.inv(subgroupGroup(G, H)) = restrict(G.inv, H)
proof
  simp [subgroupGroup, Group.mk.inv]

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

theorem Subgroup.closed_binary
  shows ClosedBinary(H, G.mul)
proof
  intros x hx y hy
  exact Subgroup.mul_mem with *

theorem Subgroup.closed_unary
  shows ClosedUnary(H, G.inv)
proof
  intros x hx
  exact Subgroup.inv_mem with *

theorem subgroupGroup.mul (h k : H)
  shows Group.mul(subgroupGroup(G, H))(h, k) = h * k
proof
  have magma := IsGroup.magma with (Group.parts with group)
  have subset := Subgroup.subset with subgroup
  have closed := Subgroup.closed_binary with group, subgroup
  rw subgroupGroup.operation
  exact restrictBinary.value with magma, subset, closed, *

theorem subgroupGroup.inverse_value (h : H)
  shows Group.inv(subgroupGroup(G, H))(h) = h⁻¹
proof
  have function := Group.inverse_function with group
  have subset := Subgroup.subset with subgroup
  have closed := Subgroup.closed_unary with group, subgroup
  rw subgroupGroup.inverse
  exact restrictUnary.value with function, subset, closed, *

theorem Subgroup.restricted_group
  shows IsGroup(H, restrict(G.mul, H × H), G.one, restrict(G.inv, H))
proof
  have parts := Group.parts with group
  have magma := IsGroup.magma with parts
  have monoid := IsGroup.monoid with parts
  have associative := IsMonoid.associative with monoid
  have identity := IsMonoid.identity with monoid
  have inverse := IsGroup.inverse with parts
  have negation := inverse.left
  have subset := Subgroup.subset with subgroup
  have unitIn : G.one ∈ H := Subgroup.one_mem with *
  have opClosed := Subgroup.closed_binary with group, subgroup
  have invClosed := Subgroup.closed_unary with group, subgroup
  have function := restrictBinary.function with magma, subset, opClosed
  have rMagma : IsMagma(H, restrict(G.mul, H × H)) by exact function
  have rAssociative := restrictBinary.associative with magma, subset, opClosed, associative
  have rIdentity := restrictBinary.identity with magma, subset, opClosed, identity, unitIn
  have rInverse := restrictUnary.inverse with magma, negation, subset, opClosed, invClosed, inverse
  simp [IsGroup, IsMonoid, IsSemigroup]

theorem subgroupGroup.group
  shows Group(subgroupGroup(G, H))
proof
  have restricted := Subgroup.restricted_group with group, subgroup
  unfold subgroupGroup
  exact Group.of_parts with restricted

theorem subgroupGroup.abelian
  requires abelian : AbelianGroup(G)
  shows AbelianGroup(subgroupGroup(G, H))
proof
  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)
  have magma := IsGroup.magma with (Group.parts with group)
  have subset := Subgroup.subset with subgroup
  have opClosed := Subgroup.closed_binary with group, subgroup
  have restricted := Subgroup.restricted_group with group, subgroup
  have rCommutative := restrictBinary.commutative with magma, subset, opClosed, commutative
  unfold subgroupGroup
  apply AbelianGroup.of_parts
  unfold IsAbelianGroup
  exact ⟨restricted, rCommutative⟩

-- The inclusion of a subgroup is an injective homomorphism.
theorem Subgroup.inclusion_hom
  shows identity(H) : subgroupGroup(G, H) →* G
proof
  have subgroupGroupIs := subgroupGroup.group with group, subgroup
  have subset := Subgroup.subset with subgroup
  have function : identity(H) : Group.carrier(subgroupGroup(G, H)) → G.carrier
    rw subgroupGroup.carrierOf
    exact identity.inclusion with subset
  apply GroupHom.mk with subgroupGroupIs, group, function
  intros x hx y hy
  rw subgroupGroup.carrierOf at hx
  rw subgroupGroup.carrierOf at hy
  have restricted : Group.mul(subgroupGroup(G, H))(x, y) = G.mul(x, y) := subgroupGroup.mul with *
  have vx := identity.apply with hx
  have vy := identity.apply with hy
  have closed : G.mul(x, y) ∈ H := Subgroup.mul_mem with *
  have output := identity.apply with closed
  rw [restricted, output, vx, vy]
  rfl

theorem Subgroup.inclusion_injective
  shows InjectiveBetween(identity(H), H, G.carrier)
proof
  have subset := Subgroup.subset with subgroup
  have function := identity.inclusion with subset
  constructor
  . exact function
  . intros x hx y hy z hz hxz hyz
    have vx := identity.apply with hx
    have vy := identity.apply with hy
    have ex := FunctionBetween.apply_value with function, hx, hxz
    have ey := FunctionBetween.apply_value with function, hy, hyz
    cc

end Restricted

section RestrictedHoms
variable (f G H : Set)
hypothesis hom : f : G →* H

-- A homomorphism restricted to a subgroup, as a homomorphism out of the
-- subgroup's group.
theorem GroupHom.restrict (K : Set)
  requires subgroup : Subgroup(K, G)
  shows restrict(f, K) : subgroupGroup(G, K) →* H
proof
  have group := GroupHom.source with hom
  have target := GroupHom.target with hom
  have function := GroupHom.function with hom
  have subset := Subgroup.subset with subgroup
  have subgroupGroupIs := subgroupGroup.group with group, subgroup
  have restricted := restrict.domain_function with function, subset
  have restrictedFunction : restrict(f, K) : Group.carrier(subgroupGroup(G, K)) → H.carrier
    rw subgroupGroup.carrierOf
    exact restricted
  apply GroupHom.mk with subgroupGroupIs, target, restrictedFunction
  intros x hx y hy
  rw subgroupGroup.carrierOf at hx
  rw subgroupGroup.carrierOf at hy
  have xIn : x ∈ G := Subgroup.mem_carrier with *
  have yIn : y ∈ G := Subgroup.mem_carrier with *
  have closed : G.mul(x, y) ∈ K := Subgroup.mul_mem with *
  have mulValue : Group.mul(subgroupGroup(G, K))(x, y) = G.mul(x, y) := subgroupGroup.mul with *
  have vx := restrict.domain_apply with function, subset, hx
  have vy := restrict.domain_apply with function, subset, hy
  have output := restrict.domain_apply with function, subset, closed
  have preserved : f(G.mul(x, y)) = f(x) * f(y) := GroupHom.map_mul with *
  rw [mulValue, output, vx, vy]
  exact preserved

-- The corestriction of a homomorphism to its image.
theorem GroupHom.corestrict
  shows f : G →* subgroupGroup(H, functionImage(f, G.carrier, H.carrier))
proof
  have group := GroupHom.source with hom
  have target := GroupHom.target with hom
  have function := GroupHom.function with hom
  have rangeSubgroup := GroupHom.range_subgroup with hom
  have rangeGroup := subgroupGroup.group with target, rangeSubgroup
  have corestricted : f : G.carrier → Group.carrier(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))
    rw subgroupGroup.carrierOf
    exact functionImage.corestrict with function
  apply GroupHom.mk with group, rangeGroup, corestricted
  intros x hx y hy
  have fx := functionImage.value with function, hx
  have fy := functionImage.value with function, hy
  have mulValue : Group.mul(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))(f(x), f(y)) =
      H.mul(f(x), f(y)) := subgroupGroup.mul with *
  have preserved : f(x * y) = H.mul(f(x), f(y)) := GroupHom.map_mul with *
  rw mulValue
  exact preserved

theorem GroupHom.range_group
  shows Group(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))
proof
  have target := GroupHom.target with hom
  have rangeSubgroup := GroupHom.range_subgroup with hom
  exact subgroupGroup.group with target, rangeSubgroup

theorem GroupHom.image_factorization
  shows compose(identity(functionImage(f, G.carrier, H.carrier)), f, G.carrier,
    functionImage(f, G.carrier, H.carrier), H.carrier) = f
proof
  have function := GroupHom.function with hom
  have corestricted := functionImage.corestrict with function
  have subset := functionImage.subset at f, G.carrier, H.carrier
  have inclusion := identity.inclusion with subset
  have composed := compose.function with corestricted, inclusion
  apply FunctionBetween.ext with composed, function
  intros x hx
  have fx := functionImage.value with function, hx
  have value := compose.apply at identity(functionImage(f, G.carrier, H.carrier)), f, G.carrier, functionImage(f, G.carrier, H.carrier), H.carrier, x with *
  have included := identity.apply with fx
  cc

-- The kernel of a restricted homomorphism is the restricted kernel.
theorem GroupHom.kernel_restrict (K : Set)
  requires subgroup : Subgroup(K, G)
  shows kernel(restrict(f, K), subgroupGroup(G, K), H) = ker(f) ∩ K
proof
  have function := GroupHom.function with hom
  have subset := Subgroup.subset with subgroup
  ext x
  constructor
  . intro hx
    obtain ⟨xK, vx⟩ := kernel.membership.forward with hx
    rw subgroupGroup.carrierOf at xK
    have xIn := subset with x, xK
    have restricted := restrict.domain_apply with function, subset, xK
    have vanishes : f(x) = H.one by cc
    have inKernel := kernel.of_value with xIn, vanishes
    exact intersection.membership.backward with ⟨inKernel, xK⟩
  . intro hx
    obtain ⟨inKernel, xK⟩ := intersection.membership.forward with hx
    have vx := kernel.value with inKernel
    have restricted := restrict.domain_apply with function, subset, xK
    have vanishes : restrict(f, K)(x) = H.one by cc
    have xIn : x ∈ Group.carrier(subgroupGroup(G, K))
      rw subgroupGroup.carrierOf
      exact xK
    exact kernel.of_value with xIn, vanishes

end RestrictedHoms