English
In an integral domain, the sum over a finite group of a nontrivial homomorphism to the ring is zero.
Русский
В интегральной области сумма образов не тривиального гомоморфизма от конечной группы равна нулю.
LaTeX
$$$\text{Let } R \text{ be an integral domain } G \text{ finite } f:\, G \to R \text{ a monoid homomorphism with } f\neq 1.\\\sum_{g\in G} f(g)=0.$$$
Lean4
/-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.
-/
theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 := by
classical
obtain ⟨x, hx⟩ : ∃ x : MonoidHom.range f.toHomUnits, ∀ y : MonoidHom.range f.toHomUnits, y ∈ Submonoid.powers x :=
IsCyclic.exists_monoid_generator
have hx1 : x ≠ 1 := by
rintro rfl
apply hf
ext g
rw [MonoidHom.one_apply]
obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow, eq_comm] at hn
replace hx1 : (x.val : R) - 1 ≠ 0 := -- Porting note: was `(x : R)`
fun h => hx1 (Subtype.eq (Units.ext (sub_eq_zero.1 h)))
let c := #{g | f.toHomUnits g = 1}
calc
∑ g : G, f g = ∑ g : G, (f.toHomUnits g : R) := rfl
_ = ∑ u ∈ univ.image f.toHomUnits, #{g | f.toHomUnits g = u} • (u : R) := (sum_comp ((↑) : Rˣ → R) f.toHomUnits)
_ = ∑ u ∈ univ.image f.toHomUnits, c • (u : R) :=
(sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
-- remaining goal 1, proven below
-- Porting note: have to change `(b : R)` into `((b : Rˣ) : R)`
_ = ∑ b : MonoidHom.range f.toHomUnits, c • ((b : Rˣ) : R) := (Finset.sum_subtype _ (by simp) _)
_ = c • ∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R) := smul_sum.symm
_ = c • (0 : R) := (congr_arg₂ _ rfl ?_)
_ = (0 : R) := smul_zero _
· -- remaining goal 1
show #{g : G | f.toHomUnits g = u} = c
apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
· simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
·
exact
⟨1, f.toHomUnits.map_one⟩
-- remaining goal 2
show (∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R)) = 0
calc
(∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R)) = ∑ n ∈ range (orderOf x), ((x : Rˣ) : R) ^ n :=
Eq.symm <|
sum_nbij (x ^ ·) (by simp only [mem_univ, forall_true_iff]) (by simpa using pow_injOn_Iio_orderOf)
(fun b _ =>
let ⟨n, hn⟩ := hx b
⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)),
-- Porting note: have to `beta_reduce` to apply the function
by beta_reduce at hn ⊢; rw [pow_mod_orderOf, hn]⟩)
(by simp only [imp_true_iff, Subgroup.coe_pow, Units.val_pow_eq_pow_val])
_ = 0 := ?_
rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
norm_cast
simp [pow_orderOf_eq_one]
