-- Coefficient-relative subalgebras and adjoining generators (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.Adjoin
import Ring.GeneratedSubring
import Ring.Image
import Cardinal.Finite

-- Relative to a specified coefficient map; algebra theorems assume it is a homomorphism.
predicate Subalgebra (f A B plus z minus times unit T : Set) :=
  IsSubring(B, plus, z, minus, times, unit, T) ∧ functionImage(f, A, B) ⊆ T

notation scoped Subalgebra(f, R, S, T) => Subalgebra(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, S.one, T)

def algebraAdjoin (f A B plus z minus times unit G : Set) : Set :=
  generatedSubring(B, plus, z, minus, times, unit, functionImage(f, A, B) ∪ G)

notation scoped algebraAdjoin(f, R, S, G) => algebraAdjoin(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, S.one, G)

predicate FinitelyGeneratedAlgebra (f A B plus z minus times unit : Set) :=
  ∃ G, Finite(G) ∧ G ⊆ B ∧ algebraAdjoin(f, A, B, plus, z, minus, times, unit, G) = B

notation scoped FinitelyGeneratedAlgebra(f, R, S) => FinitelyGeneratedAlgebra(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, S.one)

section Algebras
variable (A add zero neg mul one B plus z minus times unit f : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)

theorem Subalgebra.subring (T : Set)
  requires subalgebra : Subalgebra(f, R, S, T)
  shows IsSubring(S, T)
proof
  exact subalgebra.left

theorem Subalgebra.coefficients (T : Set)
  requires subalgebra : Subalgebra(f, R, S, T)
  shows functionImage(f, A, B) ⊆ T
proof
  exact subalgebra.right

theorem algebraAdjoin.subset (G : Set)
  shows algebraAdjoin(f, R, S, G) ⊆ S
proof
  unfold algebraAdjoin
  exact generatedSubring.subset with target

theorem algebraAdjoin.subalgebra (G : Set)
  requires bounded : G ⊆ S
  shows Subalgebra(f, R, S, algebraAdjoin(f, R, S, G))
proof
  have imageBound := functionImage.subset at f, A, B
  have allBound : functionImage(f, A, B) ∪ G ⊆ S
    settle with Subset, union2.membership
  have subring := generatedSubring.subring at B, plus, z, minus, times, unit, functionImage(f, A, B) ∪ G with target
  have contains := generatedSubring.contains with target, allBound
  have coefficients : functionImage(f, A, B) ⊆ generatedSubring(S, functionImage(f, A, B) ∪ G)
    intros x hx
    have member := union2.left at x, functionImage(f, A, B), G with hx
    exact contains with x, member
  unfold algebraAdjoin
  unfold Subalgebra
  refine ⟨subring, coefficients⟩

theorem algebraAdjoin.contains (G : Set)
  requires bounded : G ⊆ S
  shows G ⊆ algebraAdjoin(f, R, S, G)
proof
  have imageBound := functionImage.subset at f, A, B
  have allBound : functionImage(f, A, B) ∪ G ⊆ S
    settle with Subset, union2.membership
  have contains := generatedSubring.contains with target, allBound
  unfold algebraAdjoin
  intros x hx
  have member := union2.right at x, functionImage(f, A, B), G with hx
  exact contains with x, member

theorem algebraAdjoin.least (G T : Set)
  requires subalgebra : Subalgebra(f, R, S, T)
  requires generators : G ⊆ T
  shows algebraAdjoin(f, R, S, G) ⊆ T
proof
  have subring := Subalgebra.subring with *
  have coefficients := Subalgebra.coefficients with *
  have included : functionImage(f, A, B) ∪ G ⊆ T by simp [Subset, union2.membership]
  unfold algebraAdjoin
  exact generatedSubring.least with *

theorem algebraAdjoin.mono (G H : Set)
  requires included : G ⊆ H
  shows algebraAdjoin(f, R, S, G) ⊆ algebraAdjoin(f, R, S, H)
proof
  have larger : functionImage(f, A, B) ∪ G ⊆ functionImage(f, A, B) ∪ H by simp [Subset, union2.membership]
  have monotone := generatedSubring.mono at B, plus, z, minus, times, unit, functionImage(f, A, B) ∪ G, functionImage(f, A, B) ∪ H with *
  simpa [algebraAdjoin] using monotone

theorem algebraAdjoin.eq_of_subalgebra (T : Set)
  requires subalgebra : Subalgebra(f, R, S, T)
  shows algebraAdjoin(f, R, S, T) = T
proof
  have subring := Subalgebra.subring with *
  have bounded := IsSubring.subset_carrier with subring
  have contains := algebraAdjoin.contains with *
  have reflexive : T ⊆ T by simp [Subset]
  have least := algebraAdjoin.least with *
  exact Subset.antisymmetric with least, contains

theorem algebraAdjoin.idempotent (G : Set)
  requires bounded : G ⊆ S
  shows algebraAdjoin(f, R, S, algebraAdjoin(f, R, S, G)) = algebraAdjoin(f, R, S, G)
proof
  have subalgebra := algebraAdjoin.subalgebra with *
  exact algebraAdjoin.eq_of_subalgebra with *

theorem algebraAdjoin.empty
  shows algebraAdjoin(f, R, S, ∅) = functionImage(f, A, B)
proof
  have image := IsRingHom.image_subring with source, target, hom
  have same : functionImage(f, A, B) ∪ ∅ = functionImage(f, A, B)
    ext x
    simp
  simp [algebraAdjoin]
  exact generatedSubring.eq_of_subring with *

theorem Subalgebra.scalar_mul_mem (T a x : Set)
  requires subalgebra : Subalgebra(f, R, S, T)
  requires coefficient : a ∈ R
  requires member : x ∈ T
  shows S[f(a) * x] ∈ T
proof
  have function := IsRingHom.function with hom
  have image := functionImage.value with *
  have included := Subalgebra.coefficients with *
  have scalar := included with f(a), image
  have subring := Subalgebra.subring with *
  have closed := IsSubring.mul_closed with subring
  exact ClosedBinary.mem with closed, scalar, member

theorem algebraAdjoin.coefficient (G a : Set)
  requires bounded : G ⊆ S
  requires coefficient : a ∈ R
  shows f(a) ∈ algebraAdjoin(f, R, S, G)
proof
  have subalgebra := algebraAdjoin.subalgebra with *
  have included := Subalgebra.coefficients with *
  have function := IsRingHom.function with hom
  have image := functionImage.value with *
  exact included with f(a), image

theorem algebraAdjoin.union (G H : Set)
  requires boundedG : G ⊆ S
  requires boundedH : H ⊆ S
  shows algebraAdjoin(f, R, S, algebraAdjoin(f, R, S, G) ∪ H) = algebraAdjoin(f, R, S, G ∪ H)
proof
  have boundedUnion : G ∪ H ⊆ S
    settle with Subset, union2.membership
  have unionAlgebra := algebraAdjoin.subalgebra at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G ∪ H with *
  have includesG := algebraAdjoin.contains at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *
  have includesUnion := algebraAdjoin.contains at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G ∪ H with *
  have subsetG : G ⊆ G ∪ H
    settle with Subset, union2.membership
  have generatedG := algebraAdjoin.mono at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G, G ∪ H with *
  have generators : algebraAdjoin(f, R, S, G) ∪ H ⊆ algebraAdjoin(f, R, S, G ∪ H) by simp
  have left := algebraAdjoin.least at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, algebraAdjoin(f, R, S, G) ∪ H, algebraAdjoin(f, R, S, G ∪ H) with *
  have larger : G ∪ H ⊆ algebraAdjoin(f, R, S, G) ∪ H by simp [Subset, union2.membership]
  have right := algebraAdjoin.mono at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G ∪ H, algebraAdjoin(f, R, S, G) ∪ H with *
  exact Subset.antisymmetric with left, right

theorem algebraAdjoin.comm_ring (G : Set)
  requires bounded : G ⊆ S
  shows IsCommRing(algebraAdjoin(f, R, S, G), restrict(plus, algebraAdjoin(f, R, S, G) × algebraAdjoin(f, R, S, G)), z, restrict(minus, algebraAdjoin(f, R, S, G)), restrict(times, algebraAdjoin(f, R, S, G) × algebraAdjoin(f, R, S, G)), unit)
proof
  have subalgebra := algebraAdjoin.subalgebra with *
  have subring := Subalgebra.subring with *
  exact IsSubring.comm_ring with target, subring

theorem algebraAdjoin.eq_target_of_surjective (G : Set)
  requires onto : SurjectiveBetween(f, A, B)
  requires bounded : G ⊆ S
  shows algebraAdjoin(f, R, S, G) = B
proof
  have subset := algebraAdjoin.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *
  have function := IsRingHom.function with hom
  apply Subset.antisymmetric
  . exact subset
    intros b hb
    have surjection := onto
    obtain ⟨a, ha, edge⟩ := surjection.right with b, hb
    have value := FunctionBetween.apply_value with *
    have member := algebraAdjoin.coefficient at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G, a with *
    rwa value at member

theorem FinitelyGeneratedAlgebra.of_surjective
  requires onto : SurjectiveBetween(f, A, B)
  shows FinitelyGeneratedAlgebra(f, R, S)
proof
  have finite := Finite.empty
  have bounded : ∅ ⊆ S by simp [Subset, set.empty]
  have generated := algebraAdjoin.eq_target_of_surjective with *
  unfold FinitelyGeneratedAlgebra
  refine ⟨∅, finite, bounded, generated⟩

end Algebras