# Zulip Chat Archive

## Stream: new members

### Topic: bundled subgroups

#### Jason KY. (Apr 07 2020 at 15:03):

I'm trying to create a coercion and I'm not sure why one of my definition is working and the other is not

import group_theory.subgroup variables {G : Type*} [group G] structure subgroup (G : Type*) [group G] extends submonoid G := (inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier) instance has_coe : has_coe (subgroup G) (set G) := { coe := subgroup.carrier } -- unknown identifier 'subgroup.carrier' structure subgroup' (G : Type*) [group G] := (carrier : set G) (one_mem' : (1 : G) ∈ carrier) (mul_mem' {x y} : x ∈ carrier → y ∈ carrier → x * y ∈ carrier) (inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier) instance has_coe' : has_coe (subgroup' G) (set G) := { coe := subgroup'.carrier }

As you can see, LEAN is not recognizing that my first subgroup has a carrrier in my first coercion. Why might this be the case?

#### Kevin Buzzard (Apr 07 2020 at 15:18):

If you `extend`

then it's probably now called something like `subgroup.to_submonoid.carrier`

#### Kevin Buzzard (Apr 07 2020 at 15:18):

Try `#print prefix subgroup`

directly after the definition

#### Jason KY. (Apr 07 2020 at 15:21):

Kevin Buzzard said:

Try

`#print prefix subgroup`

directly after the definition

This is what I get

subgroup : Π (G : Type u_2) [_inst_2 : group G], Type u_2 subgroup.cases_on : Π {G : Type u_2} [_inst_2 : group G] {C : subgroup G → Sort l} (n : subgroup G), (Π (_to_submonoid : submonoid G) (inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier), C {to_submonoid := _to_submonoid, inv_mem' := inv_mem'}) → C n subgroup.has_sizeof_inst : Π (G : Type u_2) [_inst_2 : group G], has_sizeof (subgroup G) subgroup.inv_mem' : ∀ {G : Type u_2} [_inst_2 : group G] (c : subgroup G) {x : G}, x ∈ c.to_submonoid.carrier → x⁻¹ ∈ c.to_submonoid.carrier subgroup.mk : Π {G : Type u_2} [_inst_2 : group G] (_to_submonoid : submonoid G), (∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier) → subgroup G subgroup.mk.inj : ∀ {G : Type u_2} {_inst_2 : group G} {_to_submonoid : submonoid G} {inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier} {_to_submonoid_1 : submonoid G} {inv_mem'_1 : ∀ {x : G}, x ∈ _to_submonoid_1.carrier → x⁻¹ ∈ _to_submonoid_1.carrier}, {to_submonoid := _to_submonoid, inv_mem' := inv_mem'} = {to_submonoid := _to_submonoid_1, inv_mem' := inv_mem'_1} → _to_submonoid = _to_submonoid_1 subgroup.mk.inj_arrow : Π {G : Type u_2} {_inst_2 : group G} {_to_submonoid : submonoid G} {inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier} {_to_submonoid_1 : submonoid G} {inv_mem'_1 : ∀ {x : G}, x ∈ _to_submonoid_1.carrier → x⁻¹ ∈ _to_submonoid_1.carrier}, {to_submonoid := _to_submonoid, inv_mem' := inv_mem'} = {to_submonoid := _to_submonoid_1, inv_mem' := inv_mem'_1} → Π ⦃P : Sort l⦄, (_to_submonoid = _to_submonoid_1 → P) → P subgroup.mk.inj_eq : ∀ {G : Type u_2} {_inst_2 : group G} {_to_submonoid : submonoid G} {inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier} {_to_submonoid_1 : submonoid G} {inv_mem'_1 : ∀ {x : G}, x ∈ _to_submonoid_1.carrier → x⁻¹ ∈ _to_submonoid_1.carrier}, {to_submonoid := _to_submonoid, inv_mem' := inv_mem'} = {to_submonoid := _to_submonoid_1, inv_mem' := inv_mem'_1} = (_to_submonoid = _to_submonoid_1) subgroup.mk.sizeof_spec : ∀ (G : Type u_2) [_inst_2 : group G] (_to_submonoid : submonoid G) (inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier), subgroup.sizeof G {to_submonoid := _to_submonoid, inv_mem' := inv_mem'} = 1 + sizeof _to_submonoid subgroup.no_confusion : Π {G : Type u_2} {_inst_2 : group G} {P : Sort l} {v1 v2 : subgroup G}, v1 = v2 → subgroup.no_confusion_type P v1 v2 subgroup.no_confusion_type : Π {G : Type u_2} {_inst_2 : group G}, Sort l → subgroup G → subgroup G → Sort l subgroup.rec : Π {G : Type u_2} [_inst_2 : group G] {C : subgroup G → Sort l}, (Π (_to_submonoid : submonoid G) (inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier), C {to_submonoid := _to_submonoid, inv_mem' := inv_mem'}) → Π (n : subgroup G), C n subgroup.rec_on : Π {G : Type u_2} [_inst_2 : group G] {C : subgroup G → Sort l} (n : subgroup G), (Π (_to_submonoid : submonoid G) (inv_mem' : ∀ {x : G}, x ∈ _to_submonoid.carrier → x⁻¹ ∈ _to_submonoid.carrier), C {to_submonoid := _to_submonoid, inv_mem' := inv_mem'}) → C n subgroup.sizeof : Π (G : Type u_2) [_inst_2 : group G], subgroup G → ℕ subgroup.to_submonoid : Π {G : Type u_2} [_inst_2 : group G], subgroup G → submonoid G

#### Jason KY. (Apr 07 2020 at 15:24):

Kevin Buzzard said:

If you

`extend`

then it's probably now called something like`subgroup.to_submonoid.carrier`

I thought this was it also but apparently not :/

invalid field notation, type is not of the form (C ...) where C is a constant subgroup.to_submonoid has type subgroup ?m_1 → submonoid ?m_1

I also tried this `(subgroup G).to_submonoid.carrier`

but then I get

invalid field notation, type is not of the form (C ...) where C is a constant ⁇ has type ?m_1

#### Kevin Buzzard (Apr 07 2020 at 15:33):

You have `subgroup.to_submonoid`

and `submonoid.carrier`

so now it's just a jigsaw puzzle

#### Kevin Buzzard (Apr 07 2020 at 15:36):

instance : has_coe (subgroup G) (set G) := { coe := λ G, _ }

#### Jason KY. (Apr 07 2020 at 15:46):

This works!

`instance has_coe'' : has_coe (subgroup G) (set G) := { coe := λ G, (subgroup.to_submonoid G).carrier }`

#### Jason KY. (Apr 07 2020 at 15:46):

Thanks!

#### Kevin Buzzard (Apr 07 2020 at 15:46):

Do you understand dot notation?

#### Kevin Buzzard (Apr 07 2020 at 15:47):

I should say first that my choice of `G`

for the variable was very poor :-/

#### Kevin Buzzard (Apr 07 2020 at 15:47):

instance : has_coe (subgroup G) (set G) := { coe := λ H, (subgroup.to_submonoid H).carrier }

#### Jason KY. (Apr 07 2020 at 15:47):

I would say I understand it but I feel that whenever I say that I don't really understand it

#### Kevin Buzzard (Apr 07 2020 at 15:48):

So `H`

is a subgroup of `G`

, so it has type `subgroup <something>`

#### Kevin Buzzard (Apr 07 2020 at 15:48):

and that means that if you ever write `subgroup.blah H`

you might have been able to type `H.blah`

#### Jason KY. (Apr 07 2020 at 15:49):

Right, like `instance : has_coe (subgroup G) (set G) := { coe := λ K, K.to_submonoid.carrier }`

#### Kevin Buzzard (Apr 07 2020 at 15:50):

I guess it's because we use dot notation twice here (the other dot is the same as `submonoid.carrier (K.to_submonoid)`

because `K.to_submonoid`

has type `submonoid <something>`

) that you can't get away with `subgroup.to_submonoid.carrier`

.

Last updated: May 08 2021 at 18:17 UTC