-- Group isomorphisms f : G ≃* H and automorphisms: inverses and composites
-- of isomorphisms, isomorphism as an equivalence between groups, transfer
-- of commutativity, and conjugation as an inner automorphism
-- 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.Isomorphism
import Restricted
import Cardinal.Finite

-- f : G ≃* H: a bijective homomorphism. G ≃* H: some isomorphism exists.
predicate GroupIso (f G H : Set) :=
  GroupHom(f, G, H) ∧ BijectiveBetween(f, G.carrier, H.carrier)

predicate IsomorphicGroups (G H : Set) := ∃ f, GroupIso(f, G, H)

predicate GroupAutomorphism (f G : Set) := GroupIso(f, G, G)

notation guard "_ : _ ≃* _" => GroupIso
notation infix 50 "≃*" => IsomorphicGroups

theorem GroupIso.mk (f G H : Set)
  requires hom : f : G →* H
  requires bijective : BijectiveBetween(f, G.carrier, H.carrier)
  shows f : G ≃* H
proof
  unfold GroupIso
  exact ⟨hom, bijective⟩

section IsoLaws
variable (f G H : Set)
hypothesis iso : f : G ≃* H

theorem GroupIso.hom
  shows f : G →* H
proof
  obtain ⟨hom, bijective⟩ := iso
  exact hom

theorem GroupIso.bijective
  shows BijectiveBetween(f, G.carrier, H.carrier)
proof
  obtain ⟨hom, bijective⟩ := iso
  exact bijective

theorem GroupIso.function
  shows f : G.carrier → H.carrier
proof
  have hom := GroupIso.hom with iso
  exact GroupHom.function with hom

theorem GroupIso.injective
  shows InjectiveBetween(f, G.carrier, H.carrier)
proof
  have bijective := GroupIso.bijective with iso
  exact Bijective.injective with bijective

theorem GroupIso.surjective
  shows SurjectiveBetween(f, G.carrier, H.carrier)
proof
  have bijective := GroupIso.bijective with iso
  exact Bijective.surjective with bijective

theorem GroupIso.map_mul (a b : G)
  shows f(a * b) = f(a) * f(b)
proof
  have hom := GroupIso.hom with iso
  exact GroupHom.map_mul with *

theorem GroupIso.equipotent
  shows G.carrier ≃ H.carrier
proof
  have bijective := GroupIso.bijective with iso
  witness f
  exact bijective

theorem GroupIso.kernel_trivial
  shows ker(f) = {G.one}
proof
  have hom := GroupIso.hom with iso
  have injective := GroupIso.injective with iso
  have criterion := GroupHom.injective_iff_kernel_trivial with hom
  exact criterion.forward with injective

theorem GroupIso.range
  shows functionImage(f, G.carrier, H.carrier) = H.carrier
proof
  have hom := GroupIso.hom with iso
  have surjective := GroupIso.surjective with iso
  have criterion := GroupHom.surjective_iff_range with hom
  exact criterion.forward with surjective

-- The inverse of an isomorphism is an isomorphism.
theorem GroupIso.symm
  shows converse(f, G.carrier, H.carrier) : H ≃* G
proof
  have hom := GroupIso.hom with iso
  have group := GroupHom.source with hom
  have target := GroupHom.target with hom
  have bijective := GroupIso.bijective with iso
  have inverse := converse.function_of_bijective with bijective
  have inverseBijective := converse.bijective with bijective
  have inverseHom : converse(f, G.carrier, H.carrier) : H →* G
    apply GroupHom.mk with target, group, inverse
    intros y hy w hw
    have py := FunctionBetween.apply_closed with inverse, hy
    have pw := FunctionBetween.apply_closed with inverse, hw
    have fy := Bijective.apply_inverse with bijective, hy
    have fw := Bijective.apply_inverse with bijective, hw
    have closed : converse(f, G.carrier, H.carrier)(y) * converse(f, G.carrier, H.carrier)(w) ∈ G.carrier by typecheck
    have mapped : f(converse(f, G.carrier, H.carrier)(y) * converse(f, G.carrier, H.carrier)(w)) =
        f(converse(f, G.carrier, H.carrier)(y)) * f(converse(f, G.carrier, H.carrier)(w)) :=
      GroupHom.map_mul with *
    have recovered := Bijective.inverse_apply with bijective, closed
    cc
  exact GroupIso.mk with inverseHom, inverseBijective

-- Commutativity transfers along an isomorphism.
theorem GroupIso.commutative
  requires commutative : Commutative(G.carrier, G.mul)
  shows Commutative(H.carrier, H.mul)
proof
  have function := GroupIso.function with iso
  have surjective := GroupIso.surjective with iso
  intros y hy w hw
  obtain ⟨x, hx, xEdge⟩ := surjective.right with y, hy
  obtain ⟨u, hu, uEdge⟩ := surjective.right with w, hw
  have yEq := FunctionBetween.apply_value with function, hx, xEdge
  have wEq := FunctionBetween.apply_value with function, hu, uEdge
  have first : f(x * u) = f(x) * f(u) := GroupIso.map_mul with *
  have second : f(u * x) = f(u) * f(x) := GroupIso.map_mul with *
  have swap := Commutative.law with commutative, hx, hu
  cc

theorem GroupIso.abelian
  requires abelian : AbelianGroup(G)
  shows AbelianGroup(H)
proof
  have hom := GroupIso.hom with iso
  have target := GroupHom.target with hom
  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)
  have transferred := GroupIso.commutative with iso, commutative
  unfold Basic.AbelianGroup
  exact ⟨target, transferred⟩

end IsoLaws

theorem GroupIso.id (G : Set)
  requires group : Group(G)
  shows identity(G.carrier) : G ≃* G
proof
  have hom := GroupHom.id with group
  have bijective := identity.bijective at G.carrier
  exact GroupIso.mk with hom, bijective

theorem GroupIso.trans (f g G H K : Set)
  requires first : f : G ≃* H
  requires second : g : H ≃* K
  shows compose(g, f, G.carrier, H.carrier, K.carrier) : G ≃* K
proof
  have hom := GroupHom.comp with (GroupIso.hom with first), (GroupIso.hom with second)
  have bijective := compose.bijective with (GroupIso.bijective with first), (GroupIso.bijective with second)
  exact GroupIso.mk with hom, bijective

-- An injective homomorphism is an isomorphism onto its image.
theorem GroupHom.iso_onto_range (f G H : Set)
  requires hom : f : G →* H
  requires injective : InjectiveBetween(f, G.carrier, H.carrier)
  shows f : G ≃* subgroupGroup(H, functionImage(f, G.carrier, H.carrier))
proof
  have corestricted := GroupHom.corestrict with hom
  have injectiveImage := Injective.corestrict with injective
  have surjectiveImage := GroupHom.corestrict_surjective with hom
  have bijective : BijectiveBetween(f, G.carrier, Group.carrier(subgroupGroup(H, functionImage(f, G.carrier, H.carrier))))
    rw subgroupGroup.carrierOf
    exact ⟨injectiveImage, surjectiveImage⟩
  exact GroupIso.mk with corestricted, bijective

theorem IsomorphicGroups.refl (G : Set)
  requires group : Group(G)
  shows G ≃* G
proof
  have iso := GroupIso.id with group
  witness identity(G.carrier)
  exact iso

theorem IsomorphicGroups.symm (G H : Set)
  requires isomorphic : G ≃* H
  shows H ≃* G
proof
  obtain ⟨f, iso⟩ := isomorphic
  have inverse := GroupIso.symm with iso
  witness converse(f, G.carrier, H.carrier)
  exact inverse

theorem IsomorphicGroups.trans (G H K : Set)
  requires first : G ≃* H
  requires second : H ≃* K
  shows G ≃* K
proof
  obtain ⟨f, isoF⟩ := first
  obtain ⟨g, isoG⟩ := second
  have composed := GroupIso.trans with isoF, isoG
  witness compose(g, f, G.carrier, H.carrier, K.carrier)
  exact composed

theorem IsomorphicGroups.equipotent (G H : Set)
  requires isomorphic : G ≃* H
  shows G.carrier ≃ H.carrier
proof
  obtain ⟨f, iso⟩ := isomorphic
  exact GroupIso.equipotent with iso

theorem IsomorphicGroups.abelian (G H : Set)
  requires isomorphic : G ≃* H
  requires abelian : AbelianGroup(G)
  shows AbelianGroup(H)
proof
  obtain ⟨f, iso⟩ := isomorphic
  exact GroupIso.abelian with iso, abelian

-- Automorphisms.
theorem GroupAutomorphism.iso (f G : Set)
  requires automorphism : GroupAutomorphism(f, G)
  shows f : G ≃* G
proof
  exact automorphism

theorem GroupAutomorphism.id (G : Set)
  requires group : Group(G)
  shows GroupAutomorphism(identity(G.carrier), G)
proof
  unfold GroupAutomorphism
  exact GroupIso.id with group

theorem GroupAutomorphism.symm (f G : Set)
  requires automorphism : GroupAutomorphism(f, G)
  shows GroupAutomorphism(converse(f, G.carrier, G.carrier), G)
proof
  have iso := GroupAutomorphism.iso with automorphism
  unfold GroupAutomorphism
  exact GroupIso.symm with iso

theorem GroupAutomorphism.trans (f g G : Set)
  requires first : GroupAutomorphism(f, G)
  requires second : GroupAutomorphism(g, G)
  shows GroupAutomorphism(compose(g, f, G.carrier, G.carrier, G.carrier), G)
proof
  have isoF := GroupAutomorphism.iso with first
  have isoG := GroupAutomorphism.iso with second
  unfold GroupAutomorphism
  exact GroupIso.trans with isoF, isoG

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

theorem conjugation.automorphism (g : G)
  shows GroupAutomorphism(conjugation(G, g), G)
proof
  have hom := conjugation.hom with *
  have bijective := conjugation.bijective with *
  unfold GroupAutomorphism
  exact GroupIso.mk with hom, bijective

theorem GroupAutomorphism.map_one (f : Set)
  requires automorphism : GroupAutomorphism(f, G)
  shows f(G.one) = G.one
proof
  have hom := GroupIso.hom with (GroupAutomorphism.iso with automorphism)
  exact GroupHom.map_one with hom

theorem GroupAutomorphism.image_subgroup (f H : Set)
  requires automorphism : GroupAutomorphism(f, G)
  requires subgroup : Subgroup(H, G)
  shows Subgroup(functionImage(f, H, G.carrier), G)
proof
  have hom := GroupIso.hom with (GroupAutomorphism.iso with automorphism)
  exact GroupHom.image_subgroup with hom, subgroup

theorem GroupAutomorphism.image_normal (f N : Set)
  requires automorphism : GroupAutomorphism(f, G)
  requires normal : NormalSubgroup(N, G)
  shows NormalSubgroup(functionImage(f, N, G.carrier), G)
proof
  have iso := GroupAutomorphism.iso with automorphism
  have hom := GroupIso.hom with iso
  have surjective := GroupIso.surjective with iso
  exact NormalSubgroup.image_of_surjective with hom, surjective, normal

end Automorphisms