-- Bundled modules over a ring: a module as a structure extending the
-- abelian group of its vectors by a scalar action of the ring, the module
-- notation read off the hypothesis in scope, the first laws of the action,
-- and a ring as a module over itself
-- 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.Module.Basic
import Ring.Basic

-- A module over a ring R extends the abelian group of its vectors, whose
-- operation, unit, and inverse are the module's add, zero, and neg, by the
-- scalar action smul, a function from R.carrier × carrier to carrier. A
-- module is built by Module.mk(A, add, zero, neg, smul) and read back by
-- M.carrier, M.add, M.zero, M.neg, and M.smul; its additive group is the
-- value M.additive = Group.mk(M.carrier, M.add, M.zero, M.neg). Module(M, R)
-- says that R is a ring, that M is such a structure with
-- AbelianGroup(M.additive), and that the action distributes over both
-- additions, composes with the ring's multiplication, and fixes every
-- vector at the ring's one.
structure Module (R : Ring) extends
    AbelianGroup as additive (mul := add, one := zero, inv := neg)
  | smul : R.carrier × carrier → carrier
  where
    smul_add : ∀ r ∈ R.carrier, ∀ v w ∈ carrier,
      smul(r, add(v, w)) = add(smul(r, v), smul(r, w))
    add_smul : ∀ r s ∈ R.carrier, ∀ v ∈ carrier,
      smul(r + s, v) = add(smul(r, v), smul(s, v))
    mul_smul : ∀ r s ∈ R.carrier, ∀ v ∈ carrier,
      smul(r * s, v) = smul(r, smul(s, v))
    one_smul : ∀ v ∈ carrier, smul(R.one, v) = v

-- The projection laws of a constructed module as one rewrite set, and the
-- projections of the additive group as the module's own fields, so that a
-- fact about M.additive reads in M.add, M.zero, and M.neg.
tactic module_projections := simp [Module.mk.carrier, Module.mk.add, Module.mk.zero, Module.mk.neg, Module.mk.smul]
tactic module_additive := simp [Module.additive.carrier, Module.additive.mul, Module.additive.one, Module.additive.inv]

-- The addition is written v + w, the negation -v, and the action r • v
-- wherever a hypothesis in scope supplies the module; the operands'
-- membership in M.carrier selects the module's addition over the ring's.
-- Under the same hypothesis a binder (v : M) is a set variable with
-- v ∈ M.carrier.
notation infixl 60 "+" => call2(M.add, _, _) via hypothesis Module(M, R) for M.carrier
notation prefix 75 "-" => apply(M.neg, _) via hypothesis Module(M, R) for M.carrier
notation infixr 73 "•" => call2(M.smul, _, _) via hypothesis Module(M, R) for M.carrier

-- The ring of a module, read off the typing of its parameter.
instance Module.ring (M R : Set)
  requires module : Module(M, R)
  shows Ring(R)
proof
  obtain ⟨shape, ring, rest⟩ := module
  exact ring

section ModuleLaws
variable (R M : Set)
hypothesis ring : Ring(R)
hypothesis module : Module(M, R)

-- The additive group of the module as a group, for the group laws below.
theorem Module.additive_group
  shows Group(M.additive)
proof
  have abelian := Module.additive.abelian_group with module
  exact AbelianGroup.to_group with abelian

-- Closure: the operations and the zero stay in the carrier. These are
-- instances, so the membership of a compound term is synthesized. The
-- additive facts come from the group laws applied to M.additive, whose
-- membership is the instance Module.additive.mem.
instance Module.add_mem (v w : M)
  shows v + w ∈ M
proof
  have group := Module.additive_group with *
  have closed := Group.mul_mem at M.additive, v, w with group, *
  module_additive at closed
  exact closed

instance Module.neg_mem (v : M)
  shows -v ∈ M
proof
  have group := Module.additive_group with *
  have closed := Group.inv_mem at M.additive, v with group, *
  module_additive at closed
  exact closed

instance Module.zero_mem
  shows M.zero ∈ M
proof
  have group := Module.additive_group with *
  have closed := Group.one_mem at M.additive with group
  module_additive at closed
  exact closed

instance Module.smul_mem (r : R) (v : M)
  shows r • v ∈ M
proof
  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, rest⟩ := module
  unfold call2
  apply FunctionBetween.apply_closed with smulF
  exact product.pair with *

-- The laws of the structure under the notation.
theorem smul_add (r : R) (v w : M)
  shows r • (v + w) = r • v + r • w
proof
  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, law,
    rest⟩ := module
  exact law with r, v, w, *

theorem add_smul (r s : R) (v : M)
  shows (r + s) • v = r • v + s • v
proof
  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, smulAdd, law,
    rest⟩ := module
  exact law with r, s, v, *

theorem mul_smul (r s : R) (v : M)
  shows (r * s) • v = r • s • v
proof
  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, smulAdd, addSmul,
    law, oneSmul⟩ := module
  exact law with r, s, v, *

theorem one_smul (v : M)
  shows R.one • v = v
proof
  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, smulAdd, addSmul,
    mulSmul, law⟩ := module
  exact law with v, *

-- The additive laws, each a group law applied to M.additive.
theorem Module.add_comm (v w : M)
  shows v + w = w + v
proof
  have abelian := Module.additive.abelian_group with module
  have swap := mul_comm at M.additive, v, w with abelian, *
  module_additive at swap
  exact swap

theorem Module.add_assoc (u v w : M)
  shows u + v + w = u + (v + w)
proof
  have group := Module.additive_group with *
  have assoc := mul_assoc at M.additive, u, v, w with group, *
  module_additive at assoc
  exact assoc

theorem Module.zero_add (v : M)
  shows M.zero + v = v
proof
  have group := Module.additive_group with *
  have unit := one_mul at M.additive, v with group, *
  module_additive at unit
  exact unit

theorem Module.add_zero (v : M)
  shows v + M.zero = v
proof
  have group := Module.additive_group with *
  have unit := mul_one at M.additive, v with group, *
  module_additive at unit
  exact unit

theorem Module.neg_add (v : M)
  shows -v + v = M.zero
proof
  have group := Module.additive_group with *
  have cancel := Group.inv_mul at M.additive, v with group, *
  module_additive at cancel
  exact cancel

theorem Module.eq_zero_of_add_self (v : M)
  requires doubled : v + v = v
  shows v = M.zero
proof
  have group := Module.additive_group with *
  have criterion := mul_self_eq_self at M.additive, v with group, *
  module_additive at criterion
  exact criterion.forward with doubled

-- The action at the ring's zero and at the module's zero.
theorem zero_smul (v : M)
  shows R.zero • v = M.zero
proof
  have zeroAdd : R.zero + R.zero = R.zero :=
    IsRing.add_left_identity with (Ring.parts with ring), *
  have doubled : R.zero • v + R.zero • v = R.zero • v
    rw [← add_smul, zeroAdd]
  exact Module.eq_zero_of_add_self with *

theorem smul_zero (r : R)
  shows r • M.zero = M.zero
proof
  have zeroAdd : M.zero + M.zero = M.zero := Module.zero_add with *
  have doubled : r • M.zero + r • M.zero = r • M.zero
    rw [← smul_add, zeroAdd]
  exact Module.eq_zero_of_add_self with *

end ModuleLaws

-- A ring is a module over itself: the ring's addition, zero, and negation
-- with its multiplication as the action.
def selfModule (R : Set) : Set :=
  Module.mk(Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R))

instance Ring.to_module (R : Set)
  requires ring : Ring(R)
  shows Module(selfModule(R), R)
proof
  have parts := Ring.parts with ring
  obtain ⟨addF, zeroIn, negF, mulF, oneIn⟩ := IsRing.typing_of_parts with parts
  have abelian := Ring.additive.abelian_group with ring
  rw Ring.additive.value at abelian
  have monoid := IsRing.multiplicative with parts
  have associative := IsMonoid.associative with monoid
  have distributive := IsRing.distributive with parts
  have smulAdd : ∀ r v w ∈ R, r * (v + w) = r * v + r * w
    intros r rIn v vIn w wIn
    obtain ⟨left, right⟩ := distributive with r, rIn, v, vIn, w, wIn
    exact left
  have addSmul : ∀ r s v ∈ R, (r + s) * v = r * v + s * v
    intros r rIn s sIn v vIn
    obtain ⟨left, right⟩ := distributive with r, rIn, s, sIn, v, vIn
    exact right
  have mulSmul : ∀ r s v ∈ R, r * s * v = r * (s * v)
    intros r rIn s sIn v vIn
    exact Associative.law with associative, rIn, sIn, vIn
  have oneSmul : ∀ v ∈ R, R.one * v = v
    intros v vIn
    exact IsMonoid.left_identity with monoid, vIn
  unfold selfModule
  exact Module.intro with ring, addF, zeroIn, negF, mulF, abelian, smulAdd,
    addSmul, mulSmul, oneSmul