Zulip Chat Archive

Stream: new members

Topic: subtype map


view this post on Zulip Calle Sönne (Oct 31 2019 at 14:24):

Is there some theorem/lemma that can give me a map from a subtype into the corresponding type?

view this post on Zulip Rob Lewis (Oct 31 2019 at 14:25):

subtype.val?

view this post on Zulip Calle Sönne (Oct 31 2019 at 14:26):

Thanks! I must have been searching for the wrong thing then.. thought its name would be something like 'lift' or 'map'

view this post on Zulip Calle Sönne (Oct 31 2019 at 14:40):

Despite its simplicity I am having problems using subtype.val
I have the following code (the only important thing is the last line in tactic mode):

open_locale classical
lemma finite_prod_of_binary_prod [has_binary_products.{v} C] :  (J : Type v) [fintype J], limits.has_limits_of_shape (discrete J) C
| J fin := if h : nonempty J then
begin
let x := classical.choice h,
let J' := {a // a  x}, resetI,
have card_lt : fintype.card J' < fintype.card J, refine fintype.card_subtype_lt J _, exact x, simp,
have lim_J' : limits.has_limits_of_shape (discrete J') C, refine finite_prod_of_binary_prod J',
refine ⟨_⟩, intro,
let F' := discrete.lift (subtype.val J'),

end
else _
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, @fintype.card x.1 x.2)]}

I get the following error:

type mismatch at application
  J'.val
term
  J'
has type
  Type v : Type (max 1 (v+1))
but is expected to have type
  subtype ?m_3 : Type (max ? ?)
state:
C : Type u,
𝒞 : category C,
_inst_1 : limits.has_binary_products C,
finite_prod_of_binary_prod : Π (J : Type v) [_inst_2 : fintype J], limits.has_limits_of_shape (discrete J) C,
J : Type v,
fin : fintype J,
h : nonempty J,
x : J := classical.choice h,
J' : Type v := {a // a  x},
card_lt : fintype.card J' < fintype.card J,
lim_J' : limits.has_limits_of_shape (discrete J') C,
F : discrete J  C
 limits.has_limit F

How do I supply the fact that J' is a subtype of J to subtype.val? Shouldnt this be inferred?

view this post on Zulip Chris Hughes (Oct 31 2019 at 14:43):

You can't apply subtype.val to J' only to an element of J'

view this post on Zulip Rob Lewis (Oct 31 2019 at 14:44):

I'm not sure what the type of discrete.lift is, but note that subtype.val is a function from J' to J, not a function that can be applied to J' itself.

view this post on Zulip Chris Hughes (Oct 31 2019 at 14:45):

You just want discrete.lift subtype.val

view this post on Zulip Chris Hughes (Oct 31 2019 at 14:46):

Or probably discrete.lift (subtype.val : J' -> J)

view this post on Zulip Rob Lewis (Oct 31 2019 at 14:46):

You just want discrete.lift subtype.val

Maybe with some type annotations.

view this post on Zulip Calle Sönne (Oct 31 2019 at 14:48):

Great! Thank you :)


Last updated: May 08 2021 at 04:14 UTC