Protected inheritance

Stream: new members

[Nicolò Cavalleri]

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]

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]

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

[Nicolò Cavalleri]

Patrick Massot said:

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

Sure haha good night!

[Mario Carneiro]

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]

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]

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]

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]

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]

Sure I saw the correction ;)

[Nicolò Cavalleri]

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!