Zulip Chat Archive

Stream: new members

Topic: Protected inheritance


view this post on Zulip Nicolò Cavalleri (Jul 03 2020 at 22:22):

I do not understand how I access the fields of an inherited structure such as, in this example

structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)

structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)

#check bar.c
#check bar.a
#check foo.a

bar.a

view this post on Zulip Patrick Massot (Jul 03 2020 at 22:24):

structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)

structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)

#check bar.c
#check (bar.to_foo _).a
#check foo.a

set_option old_structure_cmd true

structure foo' (α : Type*) (β : Type*) :=
(a : α)
(b : β)

structure bar' (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)

#check bar'.c
#check bar'.a
#check foo'.a

view this post on Zulip Patrick Massot (Jul 03 2020 at 22:25):

But I need to go to bed, so I'll let other elaborate.

view this post on Zulip Nicolò Cavalleri (Jul 03 2020 at 22:26):

Patrick Massot said:

But I need to go to bed, so I'll let other elaborate.

Sure haha good night!

view this post on Zulip Mario Carneiro (Jul 03 2020 at 22:27):

structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)

structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)

variables (α β γ : Type) (x : foo α β) (y : bar α β γ)
#check y.c
#check y.a -- y.to_foo.a : α
#check x.a

view this post on Zulip Nicolò Cavalleri (Jul 03 2020 at 22:32):

Mario Carneiro said:

structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)

structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)

variables (α β γ : Type) (x : foo α β) (y : bar α β γ)
#check y.c
#check y.a -- y.to_foo.a : α
#check x.a

I am not sure I understand why your example works but in any case I still cannot make the following example work:

import topology.algebra.group

structure topological_group_morphism
(G : Type*) [topological_space G] [group G] [topological_group G]
(G' : Type*) [topological_space G'] [group G'] [topological_group G'] extends monoid_hom G G' :=
  (continuous_to_fun : continuous to_fun)

instance {G : Type*} [topological_space G] [group G] [topological_group G]
{G' : Type*} [topological_space G'] [group G'] [topological_group G'] :
has_coe_to_fun (topological_group_morphism G G') := ⟨_, (topological_group_morphism.to_monoid_hom _).to_fun

view this post on Zulip Jalex Stark (Jul 03 2020 at 22:48):

I think this works

import topology.algebra.group

structure topological_group_morphism
(G : Type*) [topological_space G] [group G] [topological_group G]
(G' : Type*) [topological_space G'] [group G'] [topological_group G'] extends monoid_hom G G' :=
  (continuous_to_fun : continuous to_fun)

instance {G : Type*} [topological_space G] [group G] [topological_group G]
{G' : Type*} [topological_space G'] [group G'] [topological_group G'] :
has_coe_to_fun (topological_group_morphism G G') :=
⟨_, λ a, a.to_fun

view this post on Zulip Nicolò Cavalleri (Jul 03 2020 at 22:50):

Jalex Stark said:

I think this works

import topology.algebra.group

structure topological_group_morphism
(G : Type*) [topological_space G] [group G] [topological_group G]
(G' : Type*) [topological_space G'] [group G'] [topological_group G'] extends monoid_hom G G' :=
  (continuous_to_fun : continuous to_fun)

instance {G : Type*} [topological_space G] [group G] [topological_group G]
{G' : Type*} [topological_space G'] [group G'] [topological_group G'] :
has_coe_to_fun (topological_group_morphism G G') :=
{F := _, G  G', coe := λ a, a.to_fun}

Ok thanks this makes some sense! I'll try to understand the details tomorrow!

view this post on Zulip Jalex Stark (Jul 03 2020 at 22:51):

sorry, the version you quoted has a typo that makes it not work. The current version compiles on my end, though, and seems very similar to what you had written

view this post on Zulip Nicolò Cavalleri (Jul 03 2020 at 22:52):

Sure I saw the correction ;)

view this post on Zulip Nicolò Cavalleri (Jul 03 2020 at 22:55):

Jalex Stark said:

sorry, the version you quoted has a typo that makes it not work. The current version compiles on my end, though, and seems very similar to what you had written

Thanks a lot!


Last updated: May 13 2021 at 17:42 UTC