fintype_functor

Stream: condensed mathematics

[Kevin Buzzard]

I see things like (fintype_functor «r» ⋙ to_CHFPNG₁ «r») ⋙ enlarging_functor which look quite intimidating to me at first. Here is a renaming proposal.

Should

@[simps] def laurent_measures.fintype_functor (r' : nnreal) : Fintype.{u} ⥤ ProFiltPseuNormGrpWithTinv₁.{u} r' :=
{ obj := λ S, ⟨laurent_measures r' S, λ F, ⟨∥F∥₊, le_rfl⟩⟩, ...

be called something like Fintype.LaurentMeasure? This functor actually does something. The other functors are forgetful functors; they could live in a forgetful namespace which we don't open if we want to be guided about where the meat is. Would something like that be a welcome refactor? Doing stuff like this helps me learn the code base.

[Kevin Buzzard]

Oh the namespace is not quite the right idea. How about an annotation on the functor names? I'll try an experiment on a branch.

[Adam Topaz]

What about Fintype_to_PFPNGT₁?

[Adam Topaz]

And the forgetful functors could be called PFPNGT₁_to_CHFPNG₁ resp. CHFPNG₁_to_CHFPNG

[Adam Topaz]

I also think we don't use dot notation enough... In this case, we could define Fintype.to_PFPNGT₁ to get the object associated to a T : Fintype, so that

def Fintype_to_PFPNGT₁ :=
{ obj := Fintype.to_PFPNGT₁,
  map := ... }

[Johan Commelin]

Adam Topaz said:

What about Fintype_to_PFPNGT₁?

But the name should mention "laurent" somewhere. Because there's also one for "real measures", and one for "free_pfpng". Etc... And they are genuinely different functors.

[Adam Topaz]

Oh yeah good point

[Adam Topaz]

So change Fintype.to_PFPNGT₁ to Fintype.LaurentMeasure and Fintype_to_PFPNGT₁ to Fintype_LaurentMeasures

[Adam Topaz]

(Note the s)

[Adam Topaz]

And of course _root_.LaurentMeasures := Profinite.extend Fintype_LaurentMeasures

[Adam Topaz]

I don't know if any of these name changes make sense. The names are a complete mess, I agree, but I'm kind of used to them at this point...

[Kevin Buzzard]

@Adam Topaz @Johan Commelin I've just got the functor-refactor branch compiling. What do you think? The little el means that this is a forgetful functor. I wanted a little ge for "greater or equal", because forgetful functors lose information, but there didn't seem to be a unicode g subscript. Probably it will rot quickly but I think I know what I'm doing now. There is more to come -- I'm about to start on the enlarging_functors but that's the last thing.

[Kevin Buzzard]

@Filippo A. E. Nuccio this affects you too if you have diverged too much from master

[Kevin Buzzard]

Here's the diff.

[Filippo A. E. Nuccio]

@Kevin Buzzard Thanks, I have now pulled and everything is back on track again. I was shocked that something clearly looking defeq to me was not, but now I am confident again that I am understanding at least something of Type theory... :sweat_smile:

[Kevin Buzzard]

I am proposing changing a bunch of the functor names so they're easier for humans to understand.

[Filippo A. E. Nuccio]

It certainly seems a very good idea.

[Kevin Buzzard]

Bleurgh it might not compile and I have to go and do real life for a bit. Will be back later, hoping for an all nighter

[Filippo A. E. Nuccio]

Oh, wow, brave you! I am getting old, I can't go for an all nighter tonight, I am almost collapsing after 10 hours of Lean (minus a dinner)...

[Kevin Buzzard]

OK so the functor-refactor branch is compiling and will rot fast. Should I merge it?

[Johan Commelin]

@Kevin Buzzard LGTM!

[Kevin Buzzard]

OK so I pushed a bunch of changes to master including the functor name refactor. Enough stuff compiles for me to be cautiously optimistic that I didn't break the build; I'll check now and fix anything up which is broken, quickly.

[Adam Topaz]

Thanks Kevin! The names are indeed much more sensible now.
One question: How useful do you think the subscripts el actually are? It seems to me that it's only used in situations where the fact that the functor in question is forgetting something can be deduced from the name of the functor itself. E.g. I think CHFPNG₁_to_CHFPNG is clear enough that it's just the forgetful functor.

[Adam Topaz]

My main objection is that it takes a total of 6 key presses to write a subscript el.

[Adam Topaz]

Well, maybe I should just finally figure out how to make custom snippets in vscode. Is there some package for vscode that's similar to emacs yasnippet?

[Kevin Buzzard]

I wanted to make a random annotation to indicate "this is a forgetful functor" because it helped me understand the code base. I'm quite happy for it to be removed.

[Adam Topaz]

No, I agree that such an annotation is good in principle, but i find typing those two subscripts to be cumbersome.

[Yaël Dillies]

You can also add \el as an abbreviation to the extensions. See vscode-lean#298

[Yaël Dillies]

@Bryan Gin-ge Chen, can you make the linkifier point to the correct repo when it's on leanprover rather than leanprover-community?

[Bryan Gin-ge Chen]

It'd be tough I think. You can do leanprover/vscode-lean#298 though.

[Adam Topaz]

There must be a way to do this locally as opposed to changing the vscode-lean package for everyone. Besides, a good snippet package would be useful for other reasons as well.

[Adam Topaz]

Looks like vscode has snippets built in

https://code.visualstudio.com/docs/editor/userdefinedsnippets

[Adam Topaz]

@Filippo A. E. Nuccio I think one needs to assume that 0 < r for is_open_U (in which case, I have a proof) Oops! I had the inequality backwards. Ignore me.

[Filippo A. E. Nuccio]

No problem! At any rate, I am advancing well with the proof (and having quite some fun opposing and unopposing categories :smile: ), so I hope to push it soon.

[Adam Topaz]

@Filippo A. E. Nuccio I think 0 < r may actually be needed?

[Adam Topaz]

Maybe I'm missing something.

[Filippo A. E. Nuccio]

Well, at any rate we have it in the setting where I am working (because the parameter p defines r and we have lemma r_pos. Or are you speaking of something else?

[Adam Topaz]

Oh ok, I thought r was just some random element of $\mathbb{R}_{\ge 0}$.

[Filippo A. E. Nuccio]

No, we have

local notation `r` := @r p

where def r : ℝ≥0 := 2⁻¹ ^ (p : ℝ).

[Adam Topaz]

Yeah I see it now.

[Adam Topaz]

Here's the proof I came up with (modulo one small sorry, which uses that 0 < r < 1):

lemma is_open_U (F : filtration (ℒ ϖ) c) (B : ℤ) : is_open (U c F B) :=
begin
  let ι : filtration (ℒ ϖ) c → Π (i : ℤ), ℤ :=
    λ t i, truncate {i} t punit.star ⟨i,by simp⟩,
  have hι : continuous ι,
  { rw continuous_pi_iff, intros i,
    dsimp [ι],
    change continuous ((λ (t : laurent_measures_bdd r ϖ {i} c),
      t punit.star ⟨i,by simp⟩) ∘ truncate {i}),
    refine continuous.comp continuous_bot (truncate_continuous «r» (Fintype.of punit) c {i}) },
  obtain ⟨n₀,h₀⟩ : ∃ n₀ : ℤ, ∀ (m : ℤ) (H : ℒ ϖ) (hH : H ∈ filtration (ℒ ϖ) c),
    m < n₀ → H punit.star m = 0,
  { obtain ⟨n₀,h₀⟩ : ∃ n₀ : ℤ, ∀ (m : ℤ), m < n₀ → c < r^m := sorry,
    use n₀, intros m H hH hm,
    exact eq_zero_of_filtration H _ hH punit.star m (h₀ m hm) },
  classical,
  let UU : set (Π (i : ℤ), ℤ) :=
    set.pi (set.Ico n₀ B) (λ i, if i ∈ set.Ico n₀ B then { F punit.star i } else ⊤),
  have hUU : is_open UU,
  { apply is_open_set_pi, exact finite_Ico n₀ B,
    intros a ha, trivial },
  convert hUU.preimage hι,
  ext G,
  split,
  { intros hG, dsimp [U, UU, ι] at ⊢ hG,
    rw [set.mem_preimage, set.mem_pi],
    intros i hi, rw if_pos hi,
    simp only [mem_singleton_iff],
    symmetry,
    apply hG, exact hi.2 },
  { intros hG, dsimp [U, UU, ι] at ⊢ hG,
    rintros ⟨⟩ n hn,
    rw [set.mem_preimage, set.mem_pi] at hG,
    symmetry,
    by_cases hn' : n < n₀,
    { erw [h₀ n G.1 G.2 hn', h₀ n F.1 F.2 hn'] },
    have hn'' : n ∈ set.Ico n₀ B := ⟨by simpa using hn', hn⟩,
    specialize hG n hn'', rw if_pos hn'' at hG, simpa using hG },
end

[Filippo A. E. Nuccio]

Oh thanks!

[Filippo A. E. Nuccio]

I think I will finish mine and then compare it with yours!

[Adam Topaz]

I can push it if you want.

[Filippo A. E. Nuccio]

OK, go ahead.

[Filippo A. E. Nuccio]

@Adam Topaz Are you taking care of the remaining sorry or should I?

[Adam Topaz]

Please go ahead!