bundled subgroups

Stream: new members

[Jason KY.]

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]

If you extend then it's probably now called something like subgroup.to_submonoid.carrier

[Kevin Buzzard]

Try #print prefix subgroup directly after the definition

[Jason KY.]

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.]

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]

You have subgroup.to_submonoid and submonoid.carrier so now it's just a jigsaw puzzle

[Kevin Buzzard]

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

[Jason KY.]

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

[Jason KY.]

Thanks!

[Kevin Buzzard]

Do you understand dot notation?

[Kevin Buzzard]

I should say first that my choice of G for the variable was very poor :-/

[Kevin Buzzard]

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

[Jason KY.]

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

[Kevin Buzzard]

So H is a subgroup of G, so it has type subgroup <something>

[Kevin Buzzard]

and that means that if you ever write subgroup.blah H you might have been able to type H.blah

[Jason KY.]

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

[Kevin Buzzard]

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.