## Stream: new members

### Topic: Protected inheritance

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

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


#### Patrick Massot (Jul 03 2020 at 22:25):

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

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

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


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


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


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

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

#### Nicolò Cavalleri (Jul 03 2020 at 22:52):

Sure I saw the correction ;)

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