## 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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.727146327495575, "perplexity": 7519.694971029457}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-21/segments/1620243991943.36/warc/CC-MAIN-20210513173321-20210513203321-00157.warc.gz"}