Zulip Chat Archive

Stream: new members

Topic: type synonym


Kalle KytΓΆlΓ€ (Jul 24 2021 at 20:41):

I understand that when one wants to place two different structures of the same kind on the same type, and there is already one instance of the structure as a type class, then one (recommended?) way is to form a type synonym. Apparently one should be able to "copy" other relevant instances to the type synonym by @derive, but replace the instance that one wants to get rid of by something else. This sounds fine and well, but I had some issues with the syntax...

(Btw, sorry, I might have technicalities wrong above. Please point out mistakes you notice and I will correct to make this as generally useful to new members as possible.)

Kalle KytΓΆlΓ€ (Jul 24 2021 at 20:41):

Here is an example, in which I would like to introduce the weak topology on a normed space E --- instead of the default topology instance on E, which is the norm topology. My attempt below is to create a type synonym weak E (in fact weak π•œ E since I struggled with implicit arguments) which is just E, but will instead be equipped with the weak topology. I would also like weak E to inherit the same old add_comm_group and module π•œ from E (it is only the topology I want to get rid of).

Kalle KytΓΆlΓ€ (Jul 24 2021 at 20:41):

This is an approximate #mwe (the two questions are pretty much right at the start, the rest is included for context). As a summary, my two questions are:

  • How to derive a module π•œ structure on weak π•œ E?
  • How to get rid of using @to_weak with lots of _s?
    • (The other direction, to_ordinary, seems to work just fine without the @!)
import tactic
import analysis.normed_space.dual

@[derive add_comm_group] -- Q : `@[derive [add_comm_group, module π•œ]]` fails. How to state?
def weak (π•œ : Type*) [nondiscrete_normed_field π•œ]
  (E : Type*) [normed_group E] [normed_space π•œ E] : Type* := E

/-- The canonical map `E β†’ weak π•œ E`. -/
def to_weak {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] : E β†’ weak π•œ E := id

/-- The canonical map `weak π•œ E β†’ E`. -/
def to_ordinary {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] : weak π•œ E β†’ E := id

lemma to_weak_injective {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] :
  function.injective (to_weak : E β†’ weak π•œ E) := Ξ» _ _, id

lemma to_ordinary_injective {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] :
  function.injective (to_ordinary : weak π•œ E β†’ E) := Ξ» _ _, id

@[simp] lemma to_weak_to_ordinary {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : weak π•œ E) :
  to_weak (to_ordinary x) = x := rfl

@[simp] lemma to_ordinary_to_weak {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : E) :
  to_ordinary (@to_weak π•œ _ _ _ _ x) = x := rfl
  -- Q : Without the `@`-notation and lots of `_`s, the statement doesn't parse. How to fix?

@[simp] lemma to_weak_inj_iff {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x y : E) :
  to_weak x = @to_weak π•œ _ _ _ _ y ↔ x = y := iff.rfl

@[simp] lemma to_ordinary_inj_iff {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x y : weak π•œ E) :
  to_ordinary x = to_ordinary y ↔ x = y := iff.rfl

attribute [irreducible] weak

/-- The type-level equivalence between `E` and `weak π•œ E`. -/
def equiv_to_weak {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] : E ≃ weak π•œ E :=
{ to_fun := to_weak,
  inv_fun := to_ordinary,
  left_inv := to_ordinary_to_weak,
  right_inv := to_weak_to_ordinary, }

@[simp]
lemma equiv_to_weak_apply {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : E):
  equiv_to_weak x = @to_weak π•œ _ _ _ _ x := rfl

@[simp]
lemma equiv_to_weak_symm_apply {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : weak π•œ E) :
  equiv_to_weak.symm x = to_ordinary x := rfl

lemma unop_eq_iff_eq_op {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : E) (y : weak π•œ E) :
  to_weak x = y ↔ x = to_ordinary y := equiv_to_weak.apply_eq_iff_eq_symm_apply

lemma op_eq_iff_eq_unop {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : weak π•œ E) (y : E) :
  to_ordinary x = y ↔ x = to_weak y := equiv_to_weak.symm.apply_eq_iff_eq_symm_apply

instance {π•œ : Type*} [nondiscrete_normed_field π•œ]
  {E : Type*} [normed_group E] [normed_space π•œ E] (x : weak π•œ E) (y : E)
  [inhabited E] : inhabited (weak π•œ E) := ⟨to_weak (default _)⟩

instance weak.topology (π•œ : Type*) [nondiscrete_normed_field π•œ]
  (E : Type*) [normed_group E] [normed_space π•œ E] : topological_space (weak π•œ E) :=
topological_space.induced
  (Ξ» (x : (weak π•œ E)), (Ξ» (x' : normed_space.dual π•œ E), x' (to_ordinary x))) Pi.topological_space

lemma weak.test_continuous' (π•œ : Type*) [nondiscrete_normed_field π•œ]
  (E : Type*) [normed_group E] [normed_space π•œ E] :
  continuous (Ξ» (x : (weak π•œ E)), (Ξ» (x' : normed_space.dual π•œ E), x' (to_ordinary x))) :=
@continuous_induced_dom (weak π•œ E) (Ξ  (x' : normed_space.dual π•œ E), π•œ)
  (Ξ» (x : (weak π•œ E)), (Ξ» (x' : normed_space.dual π•œ E), x' (to_ordinary x))) Pi.topological_space

lemma weak.test_continuous (π•œ : Type*) [nondiscrete_normed_field π•œ]
  (E : Type*) [normed_group E] [normed_space π•œ E] (x' : normed_space.dual π•œ E) :
  continuous (Ξ» (x : weak π•œ E), (x' (to_ordinary x))) :=
(continuous_pi_iff.mp (weak.test_continuous' π•œ E)) x'

theorem to_weak_continuous (π•œ : Type*) [nondiscrete_normed_field π•œ]
  (E : Type*) [normed_group E] [normed_space π•œ E] :
  continuous (@to_weak π•œ _ E _ _) :=
begin
  apply continuous_induced_rng,
  apply continuous_pi_iff.mpr,
  intros x',
  exact continuous_linear_map.continuous x',
end

Kalle KytΓΆlΓ€ (Jul 24 2021 at 20:47):

Btw, the example is pretty much copy paste from docs#opposite, which was recommended as a good model of type synonyms in this conversation.

Kalle KytΓΆlΓ€ (Jul 24 2021 at 20:48):

And I do realize that it should be possible to clean up by introducing variables, but the struggle with arguments was a part of my question in any case.

Kevin Buzzard (Jul 24 2021 at 20:54):

Older viewers here will remember one answer to the first question -- the thing we used to do before @derive was a thing:

instance (π•œ : Type*) [nondiscrete_normed_field π•œ] (E : Type*) [normed_group E] [normed_space π•œ E] :
  module π•œ (weak π•œ E) := by { dunfold weak, apply_instance }

Sebastien Gouezel (Jul 24 2021 at 20:54):

I think variables does solve your problem:

import tactic
import analysis.normed_space.dual

variables (π•œ : Type*) [nondiscrete_normed_field π•œ]

@[derive [add_comm_group, module π•œ]]
def weak (E : Type*) [normed_group E] [normed_space π•œ E] : Type* := E

works fine for me. Otherwise, you can derive it by hand, as in the file formal_multilinear_series:

section module
/- `derive` is not able to find the module structure, probably because Lean is confused by the
dependent types. We register it explicitly. -/
local attribute [reducible] formal_multilinear_series

instance : module π•œ (formal_multilinear_series π•œ E F) :=
begin
  letI : βˆ€ n, module π•œ (continuous_multilinear_map π•œ (Ξ» (i : fin n), E) F) :=
    Ξ» n, by apply_instance,
  apply_instance
end

Sebastien Gouezel (Jul 24 2021 at 20:55):

@Kevin Buzzard , I think dunfold is bad as it introduces an id somewhere. Opening a section and using local attribute [reducible] avoids this.

Kevin Buzzard (Jul 24 2021 at 20:56):

so those of us paying attention at the time clearly have an understanding of why the old method was removed and derive was introduced :-)

Kalle KytΓΆlΓ€ (Jul 24 2021 at 20:57):

Thank you Kevin and Sebastien for super fast replies! I'll study them. :smile:

Kevin Buzzard (Jul 24 2021 at 20:57):

Study mine and then forget it, apparently :-)

Eric Wieser (Jul 24 2021 at 22:45):

If you use dunfold weak, show_term { apply_instance } then you can also replace the entire tactic with the result it prints out to avoid the id problem


Last updated: Dec 20 2023 at 11:08 UTC