How to prove linear form of element given a PowerBasis?

Stream: new members

[Chung Thai Nguyen]

Hi everyone,
I'm trying to show that every element in an algebra with a power basis of dimension 2 can be written as a * gen + b. Specifically, I have the following minimal working example (#mwe):

import Mathlib.RingTheory.PowerBasis

universe u v

open PowerBasis Set

example (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
    (pb : PowerBasis R S) (h_dim : pb.dim = 2) (s : S) :
    ∃ a b : R, s = a • pb.gen + algebraMap R S b := by
  let repr : Fin pb.dim →₀ R := pb.basis.repr s
  have s_repr : s = ∑ i : Fin pb.dim, repr i • pb.basis i := (pb.basis.sum_repr s).symm
  let a := repr ⟨1, h_dim.symm ▸ one_lt_two⟩
  let b := repr ⟨0, h_dim.symm ▸ zero_lt_two⟩
  use a, b
  rw [s_repr]
  simp only [Finset.sum_fin_eq_sum_range, Fin.sum_univ_succ]
  -- ⊢ (∑ i ∈ Finset.range pb.dim, if h : i < pb.dim then repr ⟨i, h⟩ • pb.basis ⟨i, h⟩ else 0) = a • pb.gen + (algebraMap R S) b
  -- TODO: convert ∑ form to linear sum form of 2 components
  sorry

Here the dimension of the algebra S (over R) is 2, and I can extract the sum representation of the element s: S (∑ form) already. However I don't know how to prove that it's the same as a * gen + b. How can I correctly simplify the sum notation in Lean 4 so that it directly matches this form?

Any help would be greatly appreciated! Thanks in advance. :blush:

[Riccardo Brasca]

Are you looking for Fin.sum_univ_two?

[Chung Thai Nguyen]

I tried it, however it takes indices from Fin 2. But I only have indices from Fin pb.dim (e.g. let repr : Fin pb.dim →₀ R := pb.basis.repr s). I don't know how to make Lean understand that they are equivalent, rw didn't work. Do you have any ideas?

@[to_additive (attr := simp)]
theorem prod_univ_two [CommMonoid β] (f : Fin 2 → β) : ∏ i, f i = f 0 * f 1 := by
  simp [prod_univ_succ]

[Riccardo Brasca]

You can use something like

import Mathlib

open BigOperators

@[to_additive]
lemma prod_univ_two' {M : Type*} [CommMonoid M] {n : ℕ} (hn : n = 2) (f : Fin n → M) :
    ∏ i, f i = f (Fin.cast hn.symm 0) * f (Fin.cast hn.symm 1) := by
  simp [← Fin.prod_congr' f hn.symm]

[Chung Thai Nguyen]

Riccardo Brasca said:

You can use something like

import Mathlib

open BigOperators

@[to_additive]
lemma prod_univ_two' {M : Type*} [CommMonoid M] {n : ℕ} (hn : n = 2) (f : Fin n → M) :
    ∏ i, f i = f (Fin.cast hn.symm 0) * f (Fin.cast hn.symm 1) := by
  simp [← Fin.prod_congr' f hn.symm]

Thanks. This looks really useful. Let me try it.

[Chung Thai Nguyen]

Update: I've just finished the proof based on @Riccardo Brasca's lemma prod_univ_two'. I learned a lot from this, especially on how to use Fin.cast properly. Thank you very much! If anyone has suggestions on how to make the proof even cleaner, I’d love to hear them!

This is the #mwe.

import Mathlib.RingTheory.PowerBasis

open BigOperators PowerBasis Set
universe u v

@[to_additive]
lemma prod_univ_two' {M : Type*} [CommMonoid M] {n : ℕ} (hn : n = 2) (f : Fin n → M) :
    ∏ i, f i = f (Fin.cast hn.symm 0) * f (Fin.cast hn.symm 1) := by
  simp [← Fin.prod_congr' f hn.symm]

example (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
    (pb : PowerBasis R S) (h_dim : pb.dim = (2: ℕ)) (s : S) :
    ∃ a b : R, s = a • pb.gen + algebraMap R S b := by
  let repr : (Fin pb.dim) →₀ R := pb.basis.repr s
  have s_repr : s = ∑ i : Fin pb.dim, repr i • pb.basis i := (pb.basis.sum_repr s).symm

  -- Step 1: introduce shorthands for indices and coefficients of the basis
  set i0 := Fin.cast h_dim.symm 0 with i0_def
  set i1 := Fin.cast h_dim.symm 1 with i1_def
  set a := repr i1 with a_def
  set b := repr i0 with b_def

  -- Step 2: state that a and b satisfy the existential quantifier
  use a, b
  rw [s_repr]
  let f: Fin pb.dim → S := fun i => repr i • pb.basis i

  -- Step 3: convert to size-2 linear-sum form
  have sum_repr_eq: ∑ i : Fin pb.dim, repr i • pb.basis i = f i0 + f i1 := by
    exact sum_univ_two' (hn := h_dim) (f := f)
  rw [sum_repr_eq]
  -- ⊢ f i0 + f i1 = a • pb.gen + (algebraMap R S) b

  -- Step 4: prove equality for each operand
  have left_operand: f i1 = a • pb.gen := by
    unfold f
    have oright: pb.basis i1 = pb.gen := by
      rw [pb.basis_eq_pow]
      rw [i1_def] -- ⊢ pb.gen ^ ↑(Fin.cast ⋯ 1) = pb.gen
      norm_num
    rw [a_def, oright]
  rw [left_operand]
  have right_operand : f i0 = algebraMap R S b := by
    unfold f
    have oright : pb.basis i0 = 1 := by
      rw [pb.basis_eq_pow]
      rw [i0_def] -- ⊢ pb.gen ^ ↑(Fin.cast ⋯ 0) = 1
      norm_num
    rw [b_def, oright]
    have b_mul_one: b • 1 = ((algebraMap R S) b) * 1 := Algebra.smul_def (r := b) (x := (1: S))
    rw [b_mul_one] -- ⊢ (algebraMap R S) b * 1 = (algebraMap R S) b
    rw [mul_one]
  rw [right_operand]
  -- ⊢ (algebraMap R S) b + a • pb.gen = a • pb.gen + (algebraMap R S) b
  exact add_comm (algebraMap R S b) (a • pb.gen)