TensorProduct is zero iff

Stream: new members

[Richard Copley]

Can you give me any hints on how to state and prove that if an element of the tensor product is zero, it can be written as a sum of generators of the kernel of the defining congruence?
On paper this is usually taken as the definition. In Lean I think it may need some tricky functional programming. Here's what I have. I'm not hopeful it can be made to work.

import Mathlib.LinearAlgebra.TensorProduct

set_option autoImplicit false
noncomputable section
suppress_compilation
open TensorProduct

variable (R : Type*) [CommRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]
variable (N : Type*) [AddCommGroup N] [Module R N]

theorem eq_zero_iff (x : M ⊗[R] N) :
    x = 0 ↔ ∃ l : List (FreeAddMonoid (M × N)),
      x = AddCon.mk' _ l.sum ∧ ∀ p ∈ l,
        (∃ (m₁ m₂ : M) (n : N), p = .ofList [(m₁ + m₂, n), (m₁, -n), (m₂, -n)])
          ∨ (∃ (m : M) (n₁ n₂ : N), p = .ofList [(m, n₁ + n₂), (-m, n₁), (-m, n₂)])
            ∨ (∃ (r : R) (m : M) (n : N), p = .ofList [(r • m, n), (-m, r • n)]) := by
  constructor
  . intro hx
    induction x using TensorProduct.induction_on with
    | zero => exact ⟨[], rfl, fun.⟩
    | add x y ihx ihy =>
      sorry
    | tmul m n =>
      cases Quotient.exact hx with
      | of x y h' =>
        cases h' with
        | of_zero_left n => exact ⟨[], by rw [List.sum_nil, map_zero, zero_tmul], fun.⟩
        | of_zero_right => exact ⟨[], by rw [List.sum_nil, map_zero, tmul_zero], fun.⟩
        -- | of_add_left =>  -- (not needed)
        -- | of_add_right => -- (not needed)
        -- | of_smul =>      -- (not needed)
        | add_comm => sorry -- error:
          -- dependent elimination failed, failed to solve equation
          -- [(m, n)] = List.append (FreeAddMonoid.toList w) (FreeAddMonoid.toList y)
      | symm h => exact (eq_zero_iff (m ⊗ₜ[R] n)).mp hx      -- not well founded?
      | trans h₁ h₂ => exact (eq_zero_iff (m ⊗ₜ[R] n)).mp hx -- not well founded?
      | add h₁ h₂ => sorry -- error:
        -- dependent elimination failed, failed to solve equation
        --   [(m, n)] = List.append (FreeAddMonoid.toList x) (FreeAddMonoid.toList y)
  . rintro ⟨l, rfl, hl⟩
    induction l with
    | nil => rfl
    | cons head tail ih =>
      rw [List.sum_cons, map_add, ih fun p hp => hl p (List.mem_cons_of_mem head hp), add_zero]
      rcases hl head (List.mem_cons_self head tail) with
          (⟨m₁, m₂, n, rfl⟩ | ⟨m, n₁, n₂, rfl⟩ | ⟨r, m, n, rfl⟩)
      . change (m₁ + m₂) ⊗ₜ[R] n + (m₁ ⊗ₜ[R] (-n) + m₂ ⊗ₜ[R] (-n)) = 0
        rw [add_tmul, tmul_neg, tmul_neg, ← neg_add, add_neg_eq_zero]
      . change m ⊗ₜ[R] (n₁ + n₂) + ((-m) ⊗ₜ[R] n₁ + ((-m) ⊗ₜ[R] n₂)) = 0
        rw [tmul_add, neg_tmul, neg_tmul, ← neg_add, add_neg_eq_zero]
      . change (r • m) ⊗ₜ[R] n + (-m) ⊗ₜ (r • n) = 0
        rw [smul_tmul, neg_tmul, add_neg_eq_zero]

[Joël Riou]

First, you have not stated what you intented to state (this often happens!), because if x = 0, then it is the sum over the empty list:

theorem eq_zero_iff (x : M ⊗[R] N) :
    x = 0 ↔ ∃ l : List (FreeAddMonoid (M × N)),
      x = AddCon.mk' _ l.sum ∧ ∀ p ∈ l,
        (∃ (m₁ m₂ : M) (n : N), p = .ofList [(m₁ + m₂, n), (m₁, -n), (m₂, -n)])
          ∨ (∃ (m : M) (n₁ n₂ : N), p = .ofList [(m, n₁ + n₂), (-m, n₁), (-m, n₂)])
            ∨ (∃ (r : R) (m : M) (n : N), p = .ofList [(r • m, n), (-m, r • n)]) := by
  constructor
  · rintro rfl
    exact ⟨List.nil, rfl, by tauto⟩
  · sorry

[Richard Copley]

Joël Riou said:

First, you have not stated what you intented to state (this often happens!)

Almost always

[Joël Riou]

Then, a correct statement should be something about the representatives of elements in the tensor product, and for that, we may have to go into the internals of the definition of the tensor product as a quotient of a free monoid (and not a free abelian group): by definition, this is a quotient by an equivalence relation generated by many relations, it is not exactly like a quotient of an abelian group by a subgroup. Then, in order to phrase what you want, you may introduce the free abelian group on the product of M and N, introduce a subgroup, and then show that the quotient is isomorphic with the tensor product...

[Richard Copley]

Possibly this, but just now I'm tired and not really thinking.

theorem eq_zero_iff (x : FreeAddMonoid (M × N)) :
    (AddCon.mk' _ x : M ⊗[R] N) = 0 ↔ ∃ l : List (FreeAddMonoid (M × N)),
      addConGen (Eqv R M N) x l.sum ∧ ∀ p ∈ l,
        (∃ (m₁ m₂ : M) (n : N), p = .ofList [(m₁ + m₂, n), (m₁, -n), (m₂, -n)]) ∨
          (∃ (m : M) (n₁ n₂ : N), p = .ofList [(m, n₁ + n₂), (-m, n₁), (-m, n₂)]) ∨
            (∃ (r : R) (m : M) (n : N), p = .ofList [(r • m, n), (-m, r • n)]) := by sorry

[Richard Copley]

Thank you for the thoughts! I will give them due attention. Later.

[Joël Riou]

Now, the proof is:

  · intro h
    exact ⟨List.nil, (AddCon.eq _).mp h, by tauto⟩

I do not think there is a nice statement unless it is rephrased using quotients of abelian groups (or modules). Note also that FreeAddMonoid is the free (non abelian!) additive monoid.

[Richard Copley]

Excellent. At least now I know it is not worth sorrying this and continuing the argument. I really need to get it down.

[Richard Copley]

The result I want is what Dummit and Foote use here. I'd say it's moderately subtle and easily overlooked, but I don't fault D&F or Mathlib. Just a bit of an impedance mismatch.

image.png

[Richard Copley]

In case anyone wants to follow along using the book, I can save you some time by saying that "Equation 6 in the previous section ..." means equation 10.6 on p.364, here:

image.png