type synonym

Stream: new members

[Kalle Kytölä]

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ä]

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ä]

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ä]

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ä]

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]

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]

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]

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

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ä]

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

[Kevin Buzzard]

Study mine and then forget it, apparently :-)

[Eric Wieser]

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