theorem 9.5 (statement)

Stream: condensed mathematics

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

The second one will require more work.

[Damiano Testa]

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.

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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$ to $M$ are isomorphic to $M$. Now add a bit of topology, a $T^{-1}$, and some functoriality, and there you have the proof.