-- Image subrings and the general first isomorphism theorem in ZF.
-- 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.Ring.Image
import FirstIsomorphism
import Subring

theorem IsRingHom.image_subring (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsSubring(B, plus, z, minus, times, unit, functionImage(f, A, B))
proof
  have function := IsRingHom.function with hom
  have ring := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ring
  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsMonoid, Identity]
  have zeroValue := IsRingHom.zero with hom
  have oneValue := IsRingHom.one with hom
  have zeroImage := functionImage.value at f, A, B, zero with *
  have oneImage := functionImage.value at f, A, B, one with *
  have subset := functionImage.subset at f, A, B
  unfold IsSubring
  refine ⟨subset, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩
  . cc
  . cc
    intros y hy
    obtain ⟨yIn, x, hx, shape⟩ := functionImage.membership.forward with hy
    have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, x with *
    have mapped := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
    have output := functionImage.value at f, A, B, neg(x) with *
    cc
    intros y hy w hw
    obtain ⟨yIn, a, ha, sy⟩ := functionImage.membership.forward with hy
    obtain ⟨wIn, b, hb, sw⟩ := functionImage.membership.forward with hw
    have closed := IsRing.add_closed at A, add, zero, neg, mul, one, a, b with *
    have mapped := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, a, b with *
    have output := functionImage.value at f, A, B, call2(add, a, b) with *
    cc
    intros y hy w hw
    obtain ⟨yIn, c, hc, sy⟩ := functionImage.membership.forward with hy
    obtain ⟨wIn, d, hd, sw⟩ := functionImage.membership.forward with hw
    have closed := IsRing.mul_closed at A, add, zero, neg, mul, one, c, d with *
    have mapped := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, c, d with *
    have output := functionImage.value at f, A, B, call2(mul, c, d) with *
    cc

theorem IsRingHom.image_comm_ring (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsCommRing(functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)
proof
  have subring := IsRingHom.image_subring with source, target, hom
  exact IsSubring.comm_ring with target, subring

theorem IsRingHom.corestrict (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsRingHom(f, A, add, zero, neg, mul, one, functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)
proof
  have function := IsRingHom.function with hom
  have corestricted := functionImage.corestrict with *
  have imageRing := IsRingHom.image_comm_ring with source, target, hom
  have subring := IsRingHom.image_subring with source, target, hom
  have subset := functionImage.subset at f, A, B
  have addClosed := IsSubring.add_closed with *
  have mulClosed := IsSubring.mul_closed with *
  have addition : IsMagma(B, plus) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have multiplication : IsMagma(B, times) by simp [IsCommRing, IsRing, IsMonoid, IsSemigroup]
  apply IsRingHom.of_add_mul_one with source, imageRing, corestricted
  . intros x hx y hy
    have fx := functionImage.value with function, hx
    have fy := functionImage.value with function, hx
    have mapped := IsRingHom.add with hx, hy
    have restricted := restrictBinary.value at B, functionImage(f, A, B), plus, f(x), f(y) with *
    cc
  . intros x hx y hy
    have fx := functionImage.value with function, hx
    have fy := functionImage.value with function, hx
    have mapped := IsRingHom.mul with hx, hy
    have restricted := restrictBinary.value at B, functionImage(f, A, B), times, f(x), f(y) with *
    cc
  . exact IsRingHom.one with hom

-- No surjectivity hypothesis: the target is the image subring.
theorem IsRingHom.first_isomorphism_image (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsRingIso(quotientMap(f, A, functionImage(f, A, B), idealRelation(A, add, neg, ringKernel(f, A, z))), (A ⧸ idealRelation(A, add, neg, ringKernel(f, A, z))),
    quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), add), ⟦zero⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],
    quotientUnary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), neg), quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), mul), ⟦one⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],
    functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)
proof
  have function := IsRingHom.function with hom
  have imageRing := IsRingHom.image_comm_ring with source, target, hom
  have corestricted := IsRingHom.corestrict with source, target, hom
  have onto := functionImage.surjective with *
  exact idealQuotient.first_isomorphism with source, imageRing, corestricted, onto

-- Every homomorphism factors as a surjection followed by an inclusion.
theorem IsRingHom.image_factorization (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows compose(identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B) = f
proof
  have function := IsRingHom.function with hom
  have corestricted := functionImage.corestrict with function
  have subring := IsRingHom.image_subring with source, target, hom
  have inclusion := IsSubring.inclusion_function with subring
  have composed := compose.function at identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B with *
  apply FunctionBetween.ext with composed, function
  intros x hx
  have fx := functionImage.value with function, hx
  have value := compose.apply at identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B, x with *
  have included := identity.apply with fx
  cc