Finding homes for lemmas

Stream: general

[Eric Wieser]

With the new import graph and the corresponding data file hosted on the mathlib docs, it's now not too hard to answer the question "which file can my lemma go in":

import networkx as nx
import requests
import io
import operator
from functools import reduce

with requests.get("https://leanprover-community.github.io/mathlib_docs/import.gexf") as r:
    g = nx.read_gexf(io.StringIO(r.text))

# where you need the lemma, and which files it needs
needed_in = ('mathlib:ring_theory.finiteness',)
needs = ('mathlib:data.mv_polynomial.basic', 'mathlib:ring_theory.ideal.basic')

ok = (reduce(operator.and_, [nx.ancestors(g, n) for n in needs]) &
      reduce(operator.and_, [nx.descendants(g, n) for n in needed_in]))
print(ok)

This prints out

{'mathlib:ring_theory.algebra_tower', 'mathlib:ring_theory.polynomial.basic', 'mathlib:ring_theory.adjoin.polynomial', 'mathlib:ring_theory.adjoin.fg'}

[Johan Commelin]

That's awesome! Can this become part of LP?

[Eric Wieser]

LP already has python API for this, but the problem is that it has to compute the import graph from scratch, and that's really slow

[Johan Commelin]

It could have a flag to use the online gexf file, instead of computing it from scratch.

[Eric Wieser]

Alternative, maybe we should output a gexf file or similar as part of the cache

[Johan Commelin]

Maybe not as part of the same bundle, but it certainly makes sense to host them and reuse the caching mechanism.

[Eric Wieser]

(also, note that the gexf file is incorrect, as it doesn't know about files with transitive imports but no definitions or docstrings, xref leanprover-community/lean#645)

[Johan Commelin]

I think it's fine to only compute these gexf files for master.

[Eric Wieser]

I guess to me leanproject is a tool for working on local projects, so any command line feature that ignores the local project name and revision and just looks at mathlib master is a bad fit

[Eric Wieser]

We could also put this in a web UI somewhere (swapping networkx for graphology which is what the ball of yarn visualization uses), depending on people's attachment to the command line

[Johan Commelin]

Most of all, I just want a very easy way to use this script. Web or cmdline, I don't care

[Johan Commelin]

So maybe we can put it in scripts/ for now?

[Riccardo Brasca]

That's wonderful!!

[Alex J. Best]

Johan Commelin said:

Most of all, I just want a very easy way to use this script. Web or cmdline, I don't care

We should really implement this as a lean user command!

[Eric Wieser]

Is the import graph accessible to lean in an easy way?

[Alex J. Best]

Iirc scott wrote a version called home_finder a while ago, that doesn't do any actual graph theory

[Alex J. Best]

Actually @Rob Lewis wrote the one I was thinking of, I think that https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/lemma.20distribution/near/212269975 could be combined with something like https://github.com/alexjbest/lean-generalisation/blob/main/src/dag.lean#L247 to implement this in lean itself

[Yaël Dillies]

Where should those three lemmas about linear maps and topology go?

import analysis.normed_space.basic

variables {𝕜 E : Type*}

lemma continuous_at_of_exists_open [normed_ring 𝕜] [normed_group E] [module 𝕜 E] (f : E →ₗ[𝕜] 𝕜)
  (hf : ∀ ε, 0 < ε → ∃ (U : set E), (0 : E) ∈ U ∧ is_open U ∧ ∀ y ∈ U, ∥f y∥ < ε) :
  continuous_at f 0 :=
begin
  intros U hU,
  rw metric.nhds_basis_ball.1 at hU,
  rcases hU with ⟨ε, hε₁, hε₂⟩,
  simp only [filter.mem_map],
  obtain ⟨V, hV₁, hV₂, hV₃⟩ := hf ε hε₁,
  rw mem_nhds_iff,
  refine ⟨V, λ y hy, hε₂ _, hV₂, hV₁⟩,
  rw [metric.mem_ball, f.map_zero, dist_zero_right],
  exact hV₃ _ hy,
end

lemma continuous_at_of_exists_open' [normed_ring 𝕜] [normed_group E] [module 𝕜 E] (f : E →ₗ[𝕜] 𝕜) {x : E}
  (hf : ∀ ε, 0 < ε → ∃ (U : set E), x ∈ U ∧ is_open U ∧ ∀ y ∈ U, ∥f y - f x∥ < ε) :
  continuous_at f x :=
begin
  intros U hU,
  rw metric.nhds_basis_ball.1 at hU,
  rcases hU with ⟨ε, hε₁, hε₂⟩,
  simp only [filter.mem_map],
  obtain ⟨V, hV₁, hV₂, hV₃⟩ := hf ε hε₁,
  rw mem_nhds_iff,
  refine ⟨V, λ y hy, hε₂ _, hV₂, hV₁⟩,
  rw [metric.mem_ball, dist_eq_norm],
  exact hV₃ _ hy,
end

/-- A nonzero continuous linear functional is open. -/
lemma nonzero_linear_map_is_open_map [topological_space 𝕜] [division_ring 𝕜]
  [topological_ring 𝕜] [add_comm_group E] [topological_space E] [topological_add_group E]
  [module 𝕜 E] [has_continuous_smul 𝕜 E] (f : E →L[𝕜] 𝕜) (hf : f ≠ 0) :
  is_open_map f :=
begin
  obtain ⟨x₀, hx₀⟩ : ∃ x₀, f x₀ ≠ 0,
  { by_contra h,
    push_neg at h,
    exact hf (continuous_linear_map.ext (λ x, by simp [h]) )},
  intros A hA,
  rw is_open_iff_mem_nhds,
  rintro _ ⟨a, ha, rfl⟩,
  let g : 𝕜 → E := λ x, a + (x - f a) • (f x₀)⁻¹ • x₀,
  have := (show continuous g, by continuity).is_open_preimage _ ‹is_open A›,
  rw is_open_iff_mem_nhds at this,
  exact filter.sets_of_superset _ (this (f a) (by simpa [set.mem_preimage, g]))
    (λ x hx, ⟨_, hx, by simp [hx₀]⟩),
end

I'm happy to hear any golf.

[Patrick Massot]

I would say the first two lemmas probably shouldn't go anywhere. Why do you want them?

[Yaël Dillies]

They are used in #7288 but I can probably inline them.

[Heather Macbeth]

I think I'm not parsing your statement right, can you help me? Why is projection from $\mathbb{R}^2$ onto the first coordinate an open map? Or why does the last statement not apply to that function? oh i see

[Heather Macbeth]

OK, can't you get the last result from the Banach open mapping theorem? docs#open_mapping

[Heather Macbeth]

You just need to establish that a nonzero functional onto 𝕜 is surjective ...

[Yaël Dillies]

Hmm... that's an interesting result.

[Patrick Massot]

Sorry, I got interrupted. You can rewrite a cleaner proof:

/-- A nonzero continuous linear functional is open. -/
lemma nonzero_linear_map_is_open_map [topological_space 𝕜] [division_ring 𝕜]
  [topological_ring 𝕜] [add_comm_group E] [topological_space E] [topological_add_group E]
  [module 𝕜 E] [has_continuous_smul 𝕜 E] (f : E →L[𝕜] 𝕜) (hf : f ≠ 0) :
  is_open_map f :=
begin
  obtain ⟨x₀, hx₀⟩ : ∃ x₀, f x₀ ≠ 0,
  { by_contra h,
    push_neg at h,
    exact hf (continuous_linear_map.ext (λ x, by simp [h]) )},
  apply is_open_map.of_nhds_le,
  intros a,
  let g : 𝕜 → E := λ x, a + (x - f a) • (f x₀)⁻¹ • x₀,
  have cont_g : continuous g, by continuity,
  have comp : f ∘ g = id, by { ext, simp [hx₀] },
  have comp_a : g (f a) = a, by simp [hx₀],
  calc 𝓝 (f a) = map f (map g (𝓝 $ f a)) : by rw [map_map, comp, map_id]
           ... ≤ map f (𝓝 $ g (f a))      : map_mono cont_g.continuous_at
           ... = map f (𝓝 a)              : by rw comp_a
end

[Patrick Massot]

I'll have a look at what you try to do with the other two lemmas later.

[Patrick Massot]

In the mean time you can extract two lemmas from the above proof (one for the obtain and one from the calc block which has clearly nothing to do with linear maps).

[Heather Macbeth]

@Patrick Massot I think it's easier to use the open mapping theorem, though.

[Oliver Nash]

I agree but OTOH Patrick's proof doesn't require completeness (or indeed any structure beyond a topology).

[Patrick Massot]

Heather, I don't see why you would want a completeness assumption here.

[Patrick Massot]

Yaël, I had a look at the proof where you use continuous_at_of_exists_open and I don't understand why it's so complicated. Since C is open and contains zero, it contains some ball 0 r for a positive r. Hence gauge X <= gauge (ball 0 r) = norm/r, right? Then your assumption on phi implies that phi is a bounded linear map hence continuous. Am I missing something?

[Oliver Nash]

I'm pretty sure we've all written proofs that used unnecessary assumptions or started out more complicated than they needed to be.

[Patrick Massot]

By the way, what is this seminorm.lean which seems completely unrelated to our semi_normed_group?

[Patrick Massot]

Is it because you typically want to study a family of seminorms on a given type?

[Bhavik Mehta]

Patrick Massot said:

Yaël, I had a look at the proof where you use continuous_at_of_exists_open and I don't understand why it's so complicated. Since C is open and contains zero, it contains some ball 0 r for a positive r. Hence gauge X <= gauge (ball 0 r) = norm/r, right? Then your assumption on phi implies that phi is a bounded linear map hence continuous. Am I missing something?

I think I wrote the original version of some of these proofs, the answer is that it's complicated because I didn't understand how to use analysis in mathlib properly, I just needed some version of that result for later things

[Yaël Dillies]

It is not completely unrelated. The situation is the same as between ring_hom and algebra. semi_normed_group gives a distinguished seminorm through TC inference (although it's not using seminorm currently because Riccardo didn't know about analysis.seminorm at the time, so we could probably use a refactor) while seminorm is a way to create and consume several seminorms on the same group. That's what the proof does.

[Yaël Dillies]

Problem is, up to first order approximation I'm the only one aware of that file.

[Patrick Massot]

Oliver Nash said:

I'm pretty sure we've all written proofs that used unnecessary assumptions or started out more complicated than they needed to be.

Yes, of course. I'm not blaming anyone, I'm still trying to answer Yaël's question about those lemmas.

[Yaël Dillies]

Patrick Massot said:

Is it because you typically want to study a family of seminorms on a given type?

My internet is pretty bad, hadn't seen that message. Yes, you're exactly right.

[Yaël Dillies]

I tried splitting your proof into 3 lemmas but I am not convinced.

[Yaël Dillies]

Patrick Massot said:

Yaël, I had a look at the proof where you use continuous_at_of_exists_open and I don't understand why it's so complicated. Since C is open and contains zero, it contains some ball 0 r for a positive r. Hence gauge X <= gauge (ball 0 r) = norm/r, right? Then your assumption on phi implies that phi is a bounded linear map hence continuous. Am I missing something?

Aren't we missing some API for that?

[Heather Macbeth]

Have you seen docs#linear_map.mk_continuous

[Yaël Dillies]

Oh interesting! But my assumption is ∀ x, φ x ≤ gauge C x, so I somehow need to prove that gauge C is continuous?

[Andrew Yang]

Should this lemma be provided? If so, where should it go? Should it go in one of the four imports (which?), or should it go into a new file containing this lemma only?

import category_theory.limits.constructions.finite_products_of_binary_products
import category_theory.limits.constructions.equalizers
import category_theory.limits.constructions.binary_products
import category_theory.limits.constructions.limits_of_products_and_equalizers

open category_theory category_theory.limits

namespace category_theory.limits

lemma has_finite_limits_of_has_terminal_has_pullbacks
  {C : Type*} [category C] [has_terminal C] [has_pullbacks C] : has_finite_limits C :=
@@finite_limits_from_equalizers_and_finite_products _
  (@@has_finite_products_of_has_binary_and_terminal _
    (has_binary_products_of_terminal_and_pullbacks C) infer_instance)
  (@@has_equalizers_of_pullbacks_and_binary_products _
    (has_binary_products_of_terminal_and_pullbacks C) infer_instance)

end category_theory.limits

[Adam Topaz]

IMO in the same file that provides finite limits from binary products and equalizers.

[Adam Topaz]

The analogous lemma for preserving finite limits would also be useful.