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...)

[Oliver Nash]

If anyone has spare cycles I'd be grateful for a proof of the following:

import Mathlib

open ConditionallyCompleteLattice Set in
lemma Int.eq_Icc_of_foo
    {I : Set ℤ} (h₀ : I.Nonempty) (h₁ : BddBelow I) (h₂ : BddAbove I)
    (h₃ : ∀ᵉ (x ∈ I) (y ∈ I), Ioo x y ⊆ Iᶜ → Ioo x y = ∅) :
    I = Icc (sInf I) (sSup I) := by
  refine le_antisymm (subset_Icc_csInf_csSup h₁ h₂) fun z ⟨hl, hr⟩ ↦ ?_
  -- Your proof here :-)
  sorry

[Michael Stoll]

import Mathlib

open ConditionallyCompleteLattice Set in
lemma Int.eq_Icc_of_foo
    {I : Set ℤ} (h₀ : I.Nonempty) (h₁ : BddBelow I) (h₂ : BddAbove I)
    (h₃ : ∀ᵉ (x ∈ I) (y ∈ I), Ioo x y ⊆ Iᶜ → Ioo x y = ∅) :
    I = Icc (sInf I) (sSup I) := by
  refine le_antisymm (subset_Icc_csInf_csSup h₁ h₂) fun z ⟨hl, hr⟩ ↦ ?_
  have H₁ : sInf I ∈ I := csInf_mem h₀ h₁
  have H₂ : sSup I ∈ I := csSup_mem h₀ h₂
  rcases Int.le_iff_eq_or_lt.mp hl with rfl | hl
  · exact H₁
  rcases Int.le_iff_eq_or_lt.mp hr with rfl | hr
  · exact H₂
  by_contra hzI
  let x := sSup (I ∩ Iio z)
  let y := sInf (I ∩ Ioi z)
  have hx₀ : x ∈ I ∩ Iio z :=
    csSup_mem (inter_nonempty.mpr ⟨sInf I, H₁, hl⟩) (BddAbove.inter_of_left h₂)
  have hy₀ : y ∈ I ∩ Ioi z :=
    csInf_mem (inter_nonempty.mpr ⟨sSup I, H₂, hr⟩) (BddBelow.inter_of_left h₁)
  have H : Ioo x y ⊆ Iᶜ := by
    intro w hw hw'
    rcases lt_trichotomy w z with H | rfl | H
    · have : w ≤ x := le_csSup _ _ (BddAbove.inter_of_left h₂) (mem_inter hw' H)
      exact (hw.1.trans_le this).false
    · exact hzI hw'
    · have : y ≤ w := csInf_le _ _ (BddBelow.inter_of_left h₁) (mem_inter hw' H)
      exact (this.trans_lt hw.2).false
  specialize h₃ x (mem_of_mem_inter_left hx₀) y (mem_of_mem_inter_left hy₀) H
  have Hz : z ∈ Ioo x y :=
    ⟨mem_Iio.mp <| mem_of_mem_inter_right hx₀, mem_Ioi.mp <| mem_of_mem_inter_right hy₀⟩
  rwa [h₃] at Hz

Probably further golfable...

[Kevin Buzzard]

I got this:

import Mathlib

open ConditionallyCompleteLattice Set in
lemma Int.eq_Icc_of_foo
    {I : Set ℤ} (h₀ : I.Nonempty) (h₁ : BddBelow I) (h₂ : BddAbove I)
    (h₃ : ∀ᵉ (x ∈ I) (y ∈ I), Ioo x y ⊆ Iᶜ → Ioo x y = ∅) :
    I = Icc (sInf I) (sSup I) := by
  refine le_antisymm (subset_Icc_csInf_csSup h₁ h₂) fun z ⟨hl, hr⟩ ↦ ?_
  by_contra h
  let x₀ := sSup {i ∈ I | i ≤ z}
  let y₀ := sInf {i ∈ I | z ≤ i}
  have hb₁ : BddAbove {i | i ∈ I ∧ i ≤ z} := ⟨z, fun _ ⟨_, h⟩ ↦ h⟩
  have hb₂ : BddBelow {i | i ∈ I ∧ z ≤ i} := ⟨z, fun _ ⟨_, h⟩ ↦ h⟩
  obtain ⟨hx₀I, hx₀z⟩ : x₀ ∈ {i ∈ I | i ≤ z} := csSup_mem ⟨sInf I, csInf_mem h₀ h₁, hl⟩ hb₁
  obtain ⟨hy₀I, hy₀z⟩ : y₀ ∈ {i ∈ I | z ≤ i} := csInf_mem ⟨sSup I, csSup_mem h₀ h₂, hr⟩ hb₂
  specialize h₃ x₀ hx₀I y₀ hy₀I
  suffices z ∈ Ioo x₀ y₀ by
    rwa [h₃] at this
    intro t ⟨ht1, ht2⟩ ht
    obtain htz | hzt := z.le_total t
    · exact not_mem_of_lt_csInf ht2 hb₂ ⟨ht, htz⟩
    · exact not_mem_of_csSup_lt ht1 hb₁ ⟨ht, hzt⟩
  rcases lt_or_eq_of_le hx₀z with hx | hx
  · rcases lt_or_eq_of_le hy₀z with hy | hy
    · exact ⟨hx, hy⟩
    · cases h (hy ▸ hy₀I)
  · cases h (hx ▸ hx₀I)

[Kevin Buzzard]

(looks like mathematically the same argument)

[Eric Wieser]

Is h3 the same as  Convex ℚ (Int.cast '' I : Set ℚ)? edit: nope, we need a different meaning of Convex

[Bhavik Mehta]

Eric, maybe you were thinking about OrdConnected? I'd think that that's the convenient way to phrase h3:
In this way, it divides into two lemmas, one for linear orders and the other for locally finite orders.

import Mathlib

open ConditionallyCompleteLattice Set

lemma finite_of_bddBelow_of_bddAbove {α : Type*} [Preorder α] [LocallyFiniteOrder α] {I : Set α}
    (h₁ : BddBelow I) (h₂ : BddAbove I) :
    I.Finite := by
  obtain ⟨x, hx⟩ := h₁
  obtain ⟨y, hy⟩ := h₂
  exact (finite_Icc x y).subset fun z hz ↦ ⟨hx hz, hy hz⟩

lemma ordConnected_of_foo {α : Type*} [LinearOrder α] {I : Set α} (h₁ : I.Finite)
    (h₂ : ∀ᵉ (x ∈ I) (y ∈ I), Ioo x y ⊆ Iᶜ → Ioo x y = ∅) :
    OrdConnected I := by
  classical
  apply Set.ordConnected_of_Ioo
  intro x hx y hy hxy z hz
  simp only [mem_Ioo] at hz
  by_contra! hz'
  obtain ⟨x', hx', hx''⟩ := (h₁.inter_of_left (Iic z)).exists_le_maximal ⟨hx, hz.1.le⟩
  have hxz : x' < z := lt_of_le_of_ne hx''.1.2 (ne_of_mem_of_not_mem hx''.1.1 hz')
  obtain ⟨y', hy', hy''⟩ := (h₁.inter_of_left (Ici z)).exists_minimal_le ⟨hy, hz.2.le⟩
  have hzy : z < y' := lt_of_le_of_ne' hy''.1.2 (ne_of_mem_of_not_mem hy''.1.1 hz')
  have h₃ : Ioc x' z ⊆ Iᶜ := fun t ht ht' ↦ hx''.not_gt (by simp_all) ht.1
  have h₄ : Ico z y' ⊆ Iᶜ := fun t ht ht' ↦ hy''.not_lt (by simp_all) ht.2
  have h₅ : Ioo x' y' ⊆ Iᶜ := by
    simp only [← Ioc_union_Ico_eq_Ioo hxz hzy, union_subset_iff, and_true, *]
  exact Set.eq_empty_iff_forall_not_mem.1 (h₂ x' hx''.1.1 y' hy''.1.1 h₅) z ⟨hxz, hzy⟩

open ConditionallyCompleteLattice Set in
lemma Int.eq_Icc_of_foo
    {I : Set ℤ} (h₀ : I.Nonempty) (h₁ : BddBelow I) (h₂ : BddAbove I)
    (h₃ : ∀ᵉ (x ∈ I) (y ∈ I), Ioo x y ⊆ Iᶜ → Ioo x y = ∅) :
    I = Icc (sInf I) (sSup I) := by
  have h₄ := finite_of_bddBelow_of_bddAbove h₁ h₂
  have h₅ : OrdConnected I := ordConnected_of_foo h₄ h₃
  exact le_antisymm (subset_Icc_csInf_csSup h₁ h₂)
    (Set.Icc_subset I (h₀.csInf_mem h₄) (h₀.csSup_mem h₄))

[Oliver Nash]

Thank you all very, very much, especially Michael, Kevin, and Bhavik!

I have opened #23910 to try to capture these results.