-- Multiplication can be checked on generators of a relative linear span.
-- 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.LinearSpanMultiplication
import LinearSpan

def rightMultipliers (B times T y : Set) : Set := {u ∈ B | times(u, y) ∈ T}

section Algebras
variable (A add zero neg mul one B plus z minus times unit f T y : 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)
hypothesis submodule : Submodule(f, R, S, T)
hypothesis element : y ∈ S

theorem rightMultipliers.submodule
  shows Submodule(f, R, S, rightMultipliers(B, times, T, y))
proof
  have ordinary := IsCommRing.ring with target
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroMem := Submodule.zero_mem with source, target, hom, submodule
  have negClosed := Submodule.neg_closed with source, target, hom, submodule
  have addClosed := Submodule.add_closed with source, target, hom, submodule
  have bounded : rightMultipliers(B, times, T, y) ⊆ B by simp [Subset, rightMultipliers]
  have zeroMember : S[0] ∈ rightMultipliers(B, times, T, y)
    have value : S[0 * y] = S[0] by ring
    apply rightMultipliers.membership.backward
    rw value
    refine ⟨zeroIn, zeroMem⟩
  have negative : ClosedUnary(rightMultipliers(B, times, T, y), minus)
    intros u hu
    obtain ⟨member, product⟩ := rightMultipliers.membership.forward with hu
    have closed := IsRing.neg_closed with ordinary, member
    have included := ClosedUnary.mem with negClosed, product
    have equation : S[(-u) * y] = S[-(u * y)] by ring
    apply rightMultipliers.membership.backward
    rw equation
    refine ⟨closed, included⟩
  have addition : ClosedBinary(rightMultipliers(B, times, T, y), plus)
    intros u hu v hv
    obtain ⟨memberU, productU⟩ := rightMultipliers.membership.forward with hu
    obtain ⟨memberV, productV⟩ := rightMultipliers.membership.forward with hv
    have closed := IsRing.add_closed with ordinary, memberU, memberV
    have included := ClosedBinary.mem with addClosed, productU, productV
    have equation : S[(u + v) * y] = S[u * y + v * y] by ring
    apply rightMultipliers.membership.backward
    rw equation
    refine ⟨closed, included⟩
  have scalars : ∀ a ∈ R, ∀ u ∈ rightMultipliers(B, times, T, y), S[f(a) * u] ∈ rightMultipliers(B, times, T, y)
    intros a ha u hu
    obtain ⟨member, product⟩ := rightMultipliers.membership.forward with hu
    have image := IsRingHom.closed with hom, ha
    have closed := IsRing.mul_closed with ordinary, image, member
    have included := Submodule.scalar_mul_mem with source, target, hom, submodule, ha, product
    have equation : S[(f(a) * u) * y] = S[f(a) * (u * y)] by ring
    apply rightMultipliers.membership.backward
    rw equation
    refine ⟨closed, included⟩
  unfold Submodule
  refine ⟨bounded, zeroMember, negative, addition, scalars⟩

theorem linearSpan.mul_mem (G x : Set)
  requires bounded : G ⊆ S
  requires generators : ∀ g ∈ G, S[g * y] ∈ T
  requires member : x ∈ linearSpan(f, R, S, G)
  shows S[x * y] ∈ T
proof
  have multipliers := rightMultipliers.submodule with *
  have included : G ⊆ rightMultipliers(B, times, T, y)
    intros g hg
    have inB := bounded with g, hg
    have product := generators with g, hg
    exact rightMultipliers.membership.backward with ⟨inB, product⟩
  have span := linearSpan.least with source, target, hom, multipliers, included
  have multiplier := span with x, member
  have data := rightMultipliers.membership.forward with multiplier
  exact data.right

end Algebras