-- Homomorphisms preserve powers, and nonzero field elements have nonzero powers.
-- 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.Field.Powers
import Construction
import Ring.Homomorphism
import Group.Power

section Maps
variable (A add zero neg mul one B plus z minus times unit f a : 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 element : a ∈ R

theorem IsRingHom.power (n : Nat)
  shows f(monoidPow(R, a, n)) = monoidPow(S, f(a), n)
proof
  induction n
  | zero =>
    rw [monoidPow.zero, monoidPow.zero]
    exact IsRingHom.one with hom
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with source
    have monoid := IsRing.multiplicative with ordinary
    have closed := monoidPow.closed at A, mul, one, a, k with *
    have mapped := IsRingHom.mul with hom, element, closed
    rw [monoidPow.succ, monoidPow.succ, mapped, ih]
    rfl

end Maps

section Fields
variable (A add zero neg mul one a : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis field : IsField(R)
hypothesis element : a ∈ R
hypothesis nonzero : a ≠ R[0]

theorem IsField.power_nonzero (n : Nat)
  shows monoidPow(R, a, n) ≠ R[0]
proof
  induction n
  | zero =>
    have distinct := IsField.nontrivial with field
    have unequal := Nontrivial.distinct with distinct
    rw monoidPow.zero
    intro equal
    have reversed : R[0] = R[1] by cc
    exact unequal with reversed
  | succ(k) using ih =>
    have noZero := IsField.no_zero_divisors with field
    have ring := IsField.comm_ring with field
    have ordinary := IsCommRing.ring with ring
    have monoid := IsRing.multiplicative with ordinary
    have closed := monoidPow.closed at A, mul, one, a, k with *
    rw monoidPow.succ
    intro vanishes
    have alternatives := noZero with a, element, monoidPow(R, a, k), closed, vanishes
    cases alternatives with first | second
    . exact nonzero with first
    . exact ih with second

end Fields