golf request

Stream: general

[Andrew Yang]

I need the following result when showing that for $A$ an $R$-algebra of finite type, then a $A$-module is finitely presented if it is finitely presented over $R$. (following stacks#0561)

import data.mv_polynomial
import linear_algebra.smodeq

lemma exists_smodeq_of_X_exists_smodeq {I J R : Type*} [fintype I] [decidable_eq I] [comm_ring R]
   (p : submodule (mv_polynomial J R) (I → mv_polynomial J R))
   (h : ∀ i j, ∃ r : I → R, pi.single i (X j) ≡ C ∘ r [SMOD p]) :
   ∀ x, ∃ r : I → R, x ≡ C ∘ r [SMOD p] := sorry

The informal proof is just "By applying the relations given in h, we can inductively lower the degree of the polynomials", and I have a lean proof of it in #15901. However, the proof seems to be unreasonably long, and I wonder if there is a better approach to it?

[Junyan Xu]

@Andrew Yang
Here's a golf:

import data.mv_polynomial
import linear_algebra.smodeq

lemma smul_mem_induction {R M} [semiring R] [add_comm_monoid M] (N : add_submonoid M)
  [module R M] (s : set R) (hs : ∀ (a ∈ s) (m ∈ N), a • m ∈ N) :
  ∀ (a ∈ subsemiring.closure s) (m ∈ N), a • m ∈ N :=
begin
  intros a ha, apply subsemiring.closure_induction ha hs,
  { intros, rw zero_smul, exact N.zero_mem },
  { intro, rw one_smul, exact id },
  all_goals { intros x y hx hy m hm },
  { rw add_smul, exact N.add_mem (hx m hm) (hy m hm) },
  { rw mul_smul, exact hx _ (hy m hm) },
end

open mv_polynomial

variables {I J R : Type*} [fintype I] [decidable_eq I] [comm_ring R]
  (p : submodule (mv_polynomial J R) (I → mv_polynomial J R))

def smodeq_C_add_submonoid : add_submonoid (I → mv_polynomial J R) :=
{ carrier := {x | ∃ r : I → R, x ≡ C ∘ r [SMOD p]},
  add_mem' := λ x y ⟨rx, hx⟩ ⟨ry, hy⟩, ⟨rx + ry, by { convert hx.add hy, ext1, exact C_add }⟩,
  zero_mem' := ⟨0, by { convert smodeq.refl, ext1, exact C_0 }⟩ }

variable {p}
lemma mem_smodeq_C_add_submonoid_of_smodeq {x y} (h : x ≡ y [SMOD p]) :
  x ∈ smodeq_C_add_submonoid p ↔ y ∈ smodeq_C_add_submonoid p :=
⟨λ ⟨r, hx⟩, ⟨r, h.symm.trans hx⟩, λ ⟨r, hy⟩, ⟨r, h.trans hy⟩⟩

/- compiles in about 8 seconds -/
lemma exists_smodeq_of_X_exists_smodeq
  (h : ∀ i j, ∃ r : I → R, pi.single i (X j) ≡ C ∘ r [SMOD p]) :
  ∀ x, ∃ r : I → R, x ≡ C ∘ r [SMOD p] :=
begin
  intro x, rw pi_eq_sum_univ x,
  apply @finset.sum_induction _ _ _ _ _ (λ m, ∃ r, m ≡ C ∘ r [SMOD p]) _ _,
  { rintro i -,
    suffices : ∀ xi, ∃ r, pi.single i xi ≡ C ∘ r [SMOD p],
    { obtain ⟨r, hr⟩ := this (x i), use r, convert hr, ext1, rw pi.single_apply,
      simp only [pi.smul_apply, algebra.id.smul_eq_mul, mul_boole, eq_comm] },
    intro xi,
    have : xi ∈ (⊤ : subalgebra R _) := algebra.mem_top,
    rw ← adjoin_range_X at this,
    rw [← mul_one xi, ← smul_eq_mul, pi.single_smul'],
    apply smul_mem_induction (smodeq_C_add_submonoid p) _ _ _ this,
    { use pi.single i 1, convert smodeq.refl, ext1,
      simp only [pi.single_apply, apply_ite C, function.comp_app, C_1, C_0] },
    { rintro x (⟨s,rfl⟩|⟨j,rfl⟩) m ⟨r, hr⟩,
      { use s • r, convert hr.smul _, ext1, exact C_mul },
      { rw [mem_smodeq_C_add_submonoid_of_smodeq (hr.smul $ X j),
          pi_eq_sum_univ (C ∘ r), finset.smul_sum],
        apply sum_mem, rintro i -,
        obtain ⟨r', hr'⟩ := h i j, use r i • r',
        convert hr'.smul (C $ r i) using 1,
        { ext1, simp only [pi.single_apply, function.comp_app, pi.smul_apply,
            algebra.id.smul_eq_mul, mul_boole, mul_ite, mul_zero],
          rw [mul_one, mul_comm], congr' 1, rw @eq_comm _ i },
        { ext1, exact C_mul } } } },
  { rintro a b ⟨ra, ha⟩ ⟨rb, hb⟩, use ra + rb, convert ha.add hb, ext1, exact C_add },
  { use 0, convert smodeq.refl, ext1, exact C_0 },
end

[Junyan Xu]

@Andrew Yang
Turns out this is not specific to mv_polynomial and any algebra over R works; I think maybe you can prove the stacks#0561 result using the following directly without going through mv_polynomial?

import algebra.algebra.subalgebra.basic
import linear_algebra.smodeq

variables {I R A M : Type*} [comm_ring R] [comm_ring A] [algebra R A] {p : submodule A (I → A)}
  [add_comm_group M] [module A M]

lemma algebra_map_comp_smul {a : I → R} {r : R} :
  algebra_map R A ∘ (r • a) = algebra_map R A r • (algebra_map R A ∘ a) :=
funext (λ _, map_mul _ _ _)

lemma exists_smodeq_of_X_exists_smodeq [finite I] [decidable_eq I] (s : set A)
  (h : ∀ i (x ∈ s), ∃ r : I → R, pi.single i x ≡ algebra_map R A ∘ r [SMOD p]) :
  ∀ x : I → A, (∀ i, x i ∈ algebra.adjoin R s) → ∃ r : I → R, x ≡ algebra_map R A ∘ r [SMOD p] :=
begin
  let q := ((algebra_map R A).comp_left I).srange.to_add_submonoid.smodeq_closure p,
  have hq : ∀ x, x ∈ q ↔ ∃ r : I → R, x ≡ algebra_map R A ∘ r [SMOD p] := λ x, ⟨_, _⟩,
  rotate, { rintro ⟨_, ⟨r, rfl⟩, hr⟩, exact ⟨r, hr⟩ }, { rintros ⟨r, hr⟩, exact ⟨_, ⟨r, rfl⟩, hr⟩ },
  casesI nonempty_fintype I,
  intros x hx, rw [← hq, pi_eq_sum_univ_single x],
  refine @finset.sum_induction _ _ _ _ _ (∈ q) (λ _ _, q.add_mem) q.zero_mem (λ i _, _),
  apply subsemiring.smul_mem_of_mem_closure q _ _ _ (hx i); simp_rw hq,
  { use pi.single i 1, convert smodeq.refl, ext1,
    simp only [pi.single_apply, apply_ite (algebra_map R A), function.comp_app, map_one, map_zero] },
  rintro a (⟨r', rfl⟩ | ha) m ⟨r, hr⟩,
  { use r' • r, rw algebra_map_comp_smul, apply hr.smul },
  { rw [← hq, add_submonoid.mem_smodeq_closure_of_smodeq _ (hr.smul a),
      pi_eq_sum_univ_single (algebra_map R A ∘ r), finset.smul_sum],
    apply sum_mem,
    rintro i -,
    obtain ⟨r', hr'⟩ := h i a ha,
    rw hq,
    use r i • r',
    rw [smul_comm, ← pi.single_smul', smul_eq_mul, mul_one, algebra_map_comp_smul],
    apply hr'.smul },
end

[Luisitoon]

Hi, all! I am Luis from Barcelona! I am just trying to run Lean 3 on Debian-based Linux (Ubuntu) with VS Code and the Lean Infoview shows me the following error: "excessive memory consumption detected at expression traversal (potential solution: increase memory consumption threshold)". Have you ever got across this error? Everything is fine but this... (I have both Windows and Ubuntu on the laptop, everything runs perfectly on Windows, but not on Ubuntu...)