## Stream: condensed mathematics

### Topic: theorem 9.5 (statement)

#### 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

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

#### Johan Commelin (Feb 05 2021 at 12:26):

The second one will require more work.

#### 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 Λ :=
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,
topology := λ _, uniform_space.to_topological_space,
t2 := by apply_instance,
td := _,
compact := _,
continuous_neg' := _,
embedding_cast_le := _,
}


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

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


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

#### Johan Commelin (Feb 05 2021 at 17:13):

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

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

#### Johan Commelin (Feb 05 2021 at 17:14):

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

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

#### Johan Commelin (Feb 10 2021 at 08:31):

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

Last updated: May 09 2021 at 15:11 UTC