-- Finitely many integral generators give a finite module (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- 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.IntegralFinite
import FiniteSpan
import Field.Algebraic

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 IntegralOver.finite_span_adjoin (x : Set)
  requires integral : IntegralOver(f, R, S, x)
  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, {x}))
proof
  have data := integral
  unfold IntegralOver at data
  exact IntegralOver.finite_adjoin at
    A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x with *

theorem integralList.finite_adjoin (K : Set) (xs : List(K))
  requires bounded : K ⊆ S
  requires integral : ∀ x ∈ K, IntegralOver(f, R, S, x)
  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, listSupport{K}(xs)))
proof
  induction xs
  | List.nil =>
    rw listSupport
    exact FiniteSpan.empty_adjoin at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *
  | List.cons(x, tail) using ih =>
    have xIn : x ∈ S by simp [Subset]
    have singleBound : {x} ⊆ S
      intros u hu
      have equal := singleton.membership.forward with hu
      rwa equal
    have tailSubset := listSupport.subset at K, tail with *
    have tailBound := Subset.transitive with tailSubset, bounded
    have root := integral with x, assumption
    have single := IntegralOver.finite_span_adjoin with source, target, hom, root
    have joined := FiniteSpan.adjoin_union with source, target, hom, tailBound, singleBound, ih, single
    have equation : listSupport{K}(tail) ∪ {x} = insert(x, listSupport{K}(tail))
      ext u
      simp [union2.membership, singleton.membership, insert.membership]
    rw equation at joined
    rwa listSupport

theorem integralGenerators.finite_adjoin (K : Set)
  requires finite : Finite(K)
  requires bounded : K ⊆ S
  requires integral : ∀ x ∈ K, IntegralOver(f, R, S, x)
  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, K))
proof
  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite
  have subset := listSupport.subset with *
  have equal := Subset.antisymmetric with subset, covers
  have result := integralList.finite_adjoin with *
  rwa equal at result

theorem integralGenerators.finite_module (K : Set)
  requires finite : Finite(K)
  requires bounded : K ⊆ S
  requires integral : ∀ x ∈ K, IntegralOver(f, R, S, x)
  requires generates : algebraAdjoin(f, R, S, K) = S
  shows FiniteAlgebraModule(f, R, S)
proof
  have result := integralGenerators.finite_adjoin with *
  rw generates at result
  exact FiniteSpan.target_iff.forward with source, target, hom, result

theorem FinitelyGeneratedAlgebra.finite_module_of_integral
  requires generated : FinitelyGeneratedAlgebra(f, R, S)
  requires integral : ∀ x ∈ S, IntegralOver(f, R, S, x)
  shows FiniteAlgebraModule(f, R, S)
proof
  obtain ⟨K, finite, bounded, generates⟩ := generated
  have roots : ∀ x ∈ K, IntegralOver(f, R, S, x)
    intros x hx
    have member : x ∈ S by simp [Subset]
    exact integral with x, member
  exact integralGenerators.finite_module with source, target, hom, finite, bounded, roots, generates

section BaseExtension
variable (T : Set)
notation ring L := S ↾ T

theorem integralGenerators.finite_module_enlarged (K : Set)
  requires subring : IsSubring(S, T)
  requires coefficients : functionImage(f, R, S) ⊆ T
  requires finite : Finite(K)
  requires bounded : K ⊆ S
  requires integral : ∀ x ∈ K, IntegralOver(identity(T), L, S, x)
  requires generates : algebraAdjoin(f, R, S, K) = S
  shows FiniteAlgebraModule(identity(T), L, S)
proof
  have smaller : IsCommRing(L)
    exact IsSubring.comm_ring with *
  have inclusion : IsRingHom(identity(T), L, S)
    exact IsSubring.inclusion_hom with *
  have larger : Subalgebra(identity(T), L, S, algebraAdjoin(identity(T), L, S, K))
    exact algebraAdjoin.subalgebra with *
  have largerRing := Subalgebra.subring with smaller, target, inclusion, larger
  have includes : functionImage(f, R, S) ⊆ algebraAdjoin(identity(T), L, S, K)
    intros c member
    have inT : c ∈ T by exact coefficients with c, member
    have value := identity.apply at c, T with *
    have included := algebraAdjoin.coefficient at T, restrict(plus, T × T), z, restrict(minus, T), restrict(times, T × T), unit, B, plus, z, minus, times, unit, identity(T), K, c with *
    rwa value at included
  have oldAlgebra : Subalgebra(f, R, S, algebraAdjoin(identity(T), L, S, K))
    unfold Subalgebra
    refine ⟨largerRing, includes⟩
  have generators : K ⊆ algebraAdjoin(identity(T), L, S, K)
    exact algebraAdjoin.contains with *
  have first := algebraAdjoin.least with source, target, hom, oldAlgebra, generators
  rw generates at first
  have second : algebraAdjoin(identity(T), L, S, K) ⊆ S
    exact algebraAdjoin.subset with *
  have equality := Subset.antisymmetric with second, first
  exact integralGenerators.finite_module with *

end BaseExtension

end Algebras

section Fields
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 field : IsField(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)

theorem algebraicGenerators.finite_adjoin (K : Set)
  requires finite : Finite(K)
  requires bounded : K ⊆ S
  requires algebraic : ∀ x ∈ K, AlgebraicOver(f, R, S, x)
  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, K))
proof
  have source := IsField.comm_ring with field
  have integral : ∀ x ∈ K, IntegralOver(f, R, S, x)
    intros x hx
    have root := algebraic with x, hx
    exact AlgebraicOver.integral with field, target, hom, root
  exact integralGenerators.finite_adjoin with source, target, hom, finite, bounded, integral

theorem algebraicGenerators.finite_module (K : Set)
  requires finite : Finite(K)
  requires bounded : K ⊆ S
  requires algebraic : ∀ x ∈ K, AlgebraicOver(f, R, S, x)
  requires generates : algebraAdjoin(f, R, S, K) = S
  shows FiniteAlgebraModule(f, R, S)
proof
  have source := IsField.comm_ring with field
  have result := algebraicGenerators.finite_adjoin with *
  rw generates at result
  exact FiniteSpan.target_iff.forward with source, target, hom, result

theorem FinitelyGeneratedAlgebra.finite_module_of_algebraic
  requires generated : FinitelyGeneratedAlgebra(f, R, S)
  requires algebraic : ∀ x ∈ S, AlgebraicOver(f, R, S, x)
  shows FiniteAlgebraModule(f, R, S)
proof
  have source := IsField.comm_ring with field
  have integral : ∀ x ∈ S, IntegralOver(f, R, S, x)
    intros x hx
    have root := algebraic with x, hx
    exact AlgebraicOver.integral with field, target, hom, root
  exact FinitelyGeneratedAlgebra.finite_module_of_integral with source, target, hom, generated, integral

end Fields