Grace/Cumulus/Algebra/Field/Powers.g17

Open in Workbench Download source

Imports

Construction · Ring.Homomorphism · Group.Power

Declarations

• IsRingHom.power theorem derivation
• IsField.power_nonzero theorem derivation

Source

1-- Homomorphisms preserve powers, and nonzero field elements have nonzero powers.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Field.Powers8import Construction9import Ring.Homomorphism10import Group.Power1112section Maps13variable (A add zero neg mul one B plus z minus times unit f a : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring S := (B, plus, z, minus, times, unit)16hypothesis source : IsCommRing(R)17hypothesis target : IsCommRing(S)18hypothesis hom : IsRingHom(f, R, S)19hypothesis element : a ∈ R2021theorem IsRingHom.power (n : Nat)22  shows f(monoidPow(R, a, n)) = monoidPow(S, f(a), n)23proof24  induction n25  | zero =>26    rw [monoidPow.zero, monoidPow.zero]27    exact IsRingHom.one with hom28  | succ(k) using ih =>29    have ordinary := IsCommRing.ring with source30    have monoid := IsRing.multiplicative with ordinary31    have closed := monoidPow.closed at A, mul, one, a, k with *32    have mapped := IsRingHom.mul with hom, element, closed33    rw [monoidPow.succ, monoidPow.succ, mapped, ih]34    rfl3536end Maps3738section Fields39variable (A add zero neg mul one a : Set)40notation ring R := (A, add, zero, neg, mul, one)41hypothesis field : IsField(R)42hypothesis element : a ∈ R43hypothesis nonzero : a ≠ R[0]4445theorem IsField.power_nonzero (n : Nat)46  shows monoidPow(R, a, n) ≠ R[0]47proof48  induction n49  | zero =>50    have distinct := IsField.nontrivial with field51    have unequal := Nontrivial.distinct with distinct52    rw monoidPow.zero53    intro equal54    have reversed : R[0] = R[1] by cc55    exact unequal with reversed56  | succ(k) using ih =>57    have noZero := IsField.no_zero_divisors with field58    have ring := IsField.comm_ring with field59    have ordinary := IsCommRing.ring with ring60    have monoid := IsRing.multiplicative with ordinary61    have closed := monoidPow.closed at A, mul, one, a, k with *62    rw monoidPow.succ63    intro vanishes64    have alternatives := noZero with a, element, monoidPow(R, a, k), closed, vanishes65    cases alternatives with first | second66    . exact nonzero with first67    . exact ih with second6869end Fields70