-- Homomorphisms descend to quotients by normal subgroups of their kernel,
-- and the first isomorphism theorem: a group modulo the kernel of a
-- homomorphism is isomorphic to the image
-- 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.FirstIsomorphism
import Quotient
import Isomorphism
import Relation.QuotientMap

-- The map a homomorphism induces on the quotient by its kernel is written
-- inducedMap(f) under f : G →* H: the descent of f along the projection,
-- quotientMap(f, G.carrier, H.carrier, cosetRelation(G, ker(f))).
notation function "inducedMap(f)" => quotientMap(f, G.carrier, H.carrier, cosetRelation(G, ker(f))) via hypothesis GroupHom(f, G, H)

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

theorem GroupHom.respects_coset_relation (N : Set)
  requires subgroup : Subgroup(N, G)
  requires killed : N ⊆ ker(f)
  shows Respects(f, G.carrier, cosetRelation(G, N))
proof
  have group := GroupHom.source with hom
  intros x hx y hy related
  have criterion : relates(cosetRelation(G, N), x, y) ↔ x⁻¹ * y ∈ N := cosetRelation.relates with *
  have inKernel := killed with x⁻¹ * y, (criterion.forward with related)
  have images : f(x) = f(y) ↔ x⁻¹ * y ∈ ker(f) := GroupHom.apply_eq_iff with *
  exact images.backward with inKernel

theorem GroupHom.reflects_kernel_relation (x y : G)
  requires equal : f(x) = f(y)
  shows relates(cosetRelation(G, ker(f)), x, y)
proof
  have group := GroupHom.source with hom
  have subgroup := GroupHom.kernel_subgroup with hom
  have criterion : relates(cosetRelation(G, ker(f)), x, y) ↔ x⁻¹ * y ∈ ker(f) :=
    cosetRelation.relates with *
  have images : f(x) = f(y) ↔ x⁻¹ * y ∈ ker(f) := GroupHom.apply_eq_iff with *
  exact criterion.backward with (images.forward with equal)

-- The descended map is a homomorphism out of the quotient group.
theorem GroupHom.quotient_hom (N : Set)
  requires normal : NormalSubgroup(N, G)
  requires killed : N ⊆ ker(f)
  shows quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)) : G ⧸ N →* H
proof
  have group := GroupHom.source with hom
  have target := GroupHom.target with hom
  have function := GroupHom.function with hom
  have subgroup := NormalSubgroup.subgroup with normal
  have equivalence := cosetRelation.equivalence with group, subgroup
  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed
  have mapped := quotientMap.function at f, G.carrier, H.carrier, cosetRelation(G, N) with *
  have qgroup := quotientGroup.group with group, normal
  have magma := IsGroup.magma with (Group.parts with group)
  have compatible := cosetRelation.mul_compatible with group, normal
  have descended : quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)) : Group.carrier(G ⧸ N) → H.carrier
    rw quotientGroup.carrierOf
    exact mapped
  obtain ⟨source, target2, function2, preserves⟩ := hom
  apply GroupHom.mk with qgroup, target, descended
  intros X hX Y hY
  rw quotientGroup.carrierOf at hX
  rw quotientGroup.carrierOf at hY
  rw quotientGroup.operation
  exact quotientMap.binary with function, equivalence, respects, magma, compatible, preserves, hX, hY

theorem GroupHom.quotient_factorization (N : Set)
  requires subgroup : Subgroup(N, G)
  requires killed : N ⊆ ker(f)
  shows compose(quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)),
    quotientProjection(G.carrier, cosetRelation(G, N)), G.carrier,
    (G.carrier ⧸ cosetRelation(G, N)), H.carrier) = f
proof
  have group := GroupHom.source with hom
  have function := GroupHom.function with hom
  have equivalence := cosetRelation.equivalence with group, subgroup
  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed
  exact quotientMap.factorization with function, equivalence, respects

theorem GroupHom.quotient_class (N : Set) (x : G)
  requires subgroup : Subgroup(N, G)
  requires killed : N ⊆ ker(f)
  shows quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N))(⟦x⟧[G.carrier, cosetRelation(G, N)]) = f(x)
proof
  have group := GroupHom.source with hom
  have function := GroupHom.function with hom
  have equivalence := cosetRelation.equivalence with group, subgroup
  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed
  exact quotientMap.class with function, equivalence, respects, *

theorem GroupHom.quotient_unique (N g : Set)
  requires subgroup : Subgroup(N, G)
  requires killed : N ⊆ ker(f)
  requires candidate : g : (G.carrier ⧸ cosetRelation(G, N)) → H.carrier
  requires factors : ∀ x ∈ G, g(⟦x⟧[G.carrier, cosetRelation(G, N)]) = f(x)
  shows g = quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N))
proof
  have group := GroupHom.source with hom
  have function := GroupHom.function with hom
  have equivalence := cosetRelation.equivalence with group, subgroup
  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed
  exact quotientMap.unique with function, equivalence, respects, candidate, factors

-- Modulo the kernel the descended map is injective.
theorem GroupHom.quotient_injective
  shows InjectiveBetween(inducedMap(f),
    Group.carrier(G ⧸ ker(f)), H.carrier)
proof
  have group := GroupHom.source with hom
  have function := GroupHom.function with hom
  have subgroup := GroupHom.kernel_subgroup with hom
  have killed := Subset.reflexive at ker(f)
  have equivalence := cosetRelation.equivalence with group, subgroup
  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed
  have reflects : ∀ x ∈ G, ∀ y ∈ G, f(x) = f(y) →
      relates(cosetRelation(G, ker(f)), x, y)
    intros x hx y hy equal
    exact GroupHom.reflects_kernel_relation with *
  rw quotientGroup.carrierOf
  exact quotientMap.injective with function, equivalence, respects, reflects

theorem GroupHom.quotient_surjective (N : Set)
  requires subgroup : Subgroup(N, G)
  requires killed : N ⊆ ker(f)
  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)
  shows SurjectiveBetween(quotientMap(f, G.carrier, H.carrier, cosetRelation(G, N)),
    Group.carrier(G ⧸ N), H.carrier)
proof
  have group := GroupHom.source with hom
  have function := GroupHom.function with hom
  have equivalence := cosetRelation.equivalence with group, subgroup
  have respects := GroupHom.respects_coset_relation with hom, subgroup, killed
  rw quotientGroup.carrierOf
  exact quotientMap.surjective with function, equivalence, respects, onto

-- The first isomorphism theorem for a surjective homomorphism.
theorem GroupHom.first_isomorphism
  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)
  shows inducedMap(f) : G ⧸ ker(f) ≃* H
proof
  have normal := GroupHom.kernel_normal with hom
  have subgroup := NormalSubgroup.subgroup with normal
  have killed := Subset.reflexive at ker(f)
  have quotientHom := GroupHom.quotient_hom with hom, normal, killed
  have injective := GroupHom.quotient_injective with hom
  have surjective := GroupHom.quotient_surjective with hom, subgroup, killed, onto
  have bijective : BijectiveBetween(inducedMap(f), Group.carrier(G ⧸ ker(f)), H.carrier)
    unfold BijectiveBetween
    exact ⟨injective, surjective⟩
  exact GroupIso.mk with quotientHom, bijective

theorem GroupHom.quotient_isomorphic
  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)
  shows G ⧸ ker(f) ≃* H
proof
  have iso := GroupHom.first_isomorphism with hom, onto
  witness inducedMap(f)
  exact iso

theorem GroupHom.quotient_equipotent
  requires onto : SurjectiveBetween(f, G.carrier, H.carrier)
  shows Group.carrier(G ⧸ ker(f)) ≃ H.carrier
proof
  have iso := GroupHom.first_isomorphism with hom, onto
  exact GroupIso.equipotent with iso

-- Without surjectivity, the quotient is isomorphic to the image.
theorem GroupHom.first_isomorphism_range
  shows quotientMap(f, G.carrier, functionImage(f, G.carrier, H.carrier), cosetRelation(G, ker(f))) :
    G ⧸ ker(f) ≃* subgroupGroup(H, functionImage(f, G.carrier, H.carrier))
proof
  have corestricted := GroupHom.corestrict with hom
  have onto := GroupHom.corestrict_surjective with hom
  have onto2 : SurjectiveBetween(f, G.carrier, Group.carrier(subgroupGroup(H, functionImage(f, G.carrier, H.carrier))))
    rw subgroupGroup.carrierOf
    exact onto
  have same : kernel(f, G, subgroupGroup(H, functionImage(f, G.carrier, H.carrier))) = kernel(f, G, H)
    ext x
    constructor
    . intro hx
      obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx
      rw subgroupGroup.unit at vx
      exact kernel.of_value with xIn, vx
    . intro hx
      obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx
      have value : f(x) = Group.one(subgroupGroup(H, functionImage(f, G.carrier, H.carrier)))
        rw subgroupGroup.unit
        exact vx
      exact kernel.of_value with xIn, value
  have iso := GroupHom.first_isomorphism with corestricted, onto2
  rw [same, subgroupGroup.carrierOf] at iso
  exact iso

end Descent