# Zulip Chat Archive

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

s:

```
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 Λ :=
{ 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 (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)
```

#### Damiano Testa (Feb 05 2021 at 15:10):

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

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

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