Zulip Chat Archive

Stream: condensed mathematics

Topic: theorem 9.5 (statement)


view this post on Zulip Johan Commelin (Feb 05 2021 at 12:25):

To get the statement of 9.5, we'll need to fill in the following two sorrys:

variables (Λ : Type*) (r' : 0) (M : Type*)
variables [normed_group Λ] [polyhedral_lattice Λ]
variables [profinitely_filtered_pseudo_normed_group_with_Tinv r' M]

instance : profinitely_filtered_pseudo_normed_group Λ :=
sorry

instance : profinitely_filtered_pseudo_normed_group_with_Tinv r' (Λ →+ M) :=
sorry

I pushed these to polyhedral_lattice/pseudo_normed_group.lean

view this post on Zulip Johan Commelin (Feb 05 2021 at 12:26):

The first one is hopefully not too hard... it will need to use that bounded + discrete => compact.

view this post on Zulip Johan Commelin (Feb 05 2021 at 12:26):

The second one will require more work.

view this post on Zulip Damiano Testa (Feb 05 2021 at 14:52):

I had some time, so I tried to get into this, but it is hard work!

I made lean fill in some of the blanks, though:

instance : profinitely_filtered_pseudo_normed_group Λ :=
{ to_add_comm_group := by apply_instance,
  filtration := pseudo_normed_group.filtration Λ,
  filtration_mono := pseudo_normed_group.filtration_mono,
  zero_mem_filtration := pseudo_normed_group.zero_mem_filtration,
  neg_mem_filtration := pseudo_normed_group.neg_mem_filtration,
  add_mem_filtration := pseudo_normed_group.add_mem_filtration,
  topology := λ _, uniform_space.to_topological_space,
  t2 := by apply_instance,
  td := _,
  compact := _,
  continuous_add' := _,
  continuous_neg' := _,
  embedding_cast_le := _,
}

Since I am not sure on which branch to push, I post them here.

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:07):

@Damiano Testa Do you know about .. notation in structure definitions? It means that you can remove all the fields that come from pseudo_normed_group and replace them by

.. (show pseudo_normed_group \Lambda, by apply_instance)

view this post on Zulip Damiano Testa (Feb 05 2021 at 15:10):

Ah, I did not know about this! Thanks for the pointer!

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:12):

We should refactor the definition of profinitely_filtered_pseudo_normed_group to weaken embedding_cast_le to continuous_cast_le. Because as Peter pointed out, that implies embedding since the map is injective between CompHaus spaces.

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:13):

Otherwise, I guess it will be helpful to first show that the topology is discrete.

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:14):

And then we need to show that filtration \Lambda c is a finite set. Together, those two will give compact (this is already somewhere in the repo).

view this post on Zulip Johan Commelin (Feb 05 2021 at 17:14):

And once we have the discreteness, all the continuity proof obligations will be obvious.

view this post on Zulip Johan Commelin (Feb 10 2021 at 08:16):

I'm taking a shot at writing the statement of 9.5. I believe all ingredients are now in place for a sorry-free statement.

view this post on Zulip Johan Commelin (Feb 10 2021 at 08:31):

Tada:

/-- Theorem 9.5 in [Analytic] -/
theorem thm95 [BD.suitable c']
  (r r' : 0) [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r'  1)] :
   m : ,
   (k K : 0) [fact (1  k)],
   (Λ : Type) [normed_group Λ],  [polyhedral_lattice Λ],
   c₀ : 0,
   (S : Type) [fintype S],
   (V : NormedGroup) [normed_with_aut r V],
    (BD.system c' r V r' (Hom Λ (Mbar r' S))).is_bdd_exact_for_bdd_degree_above_idx k K m c₀ :=
sorry

view this post on Zulip Johan Commelin (Feb 10 2021 at 08:44):

I need to do some other stuff now, but if someone wants to proof first_target by reducing it to thm95, that should be "straightforward".
It basically boils down to showing that additive group homs from Z\Z to MM are isomorphic to MM. Now add a bit of topology, a T1T^{-1}, and some functoriality, and there you have the proof.


Last updated: May 09 2021 at 15:11 UTC