## Stream: new members

### Topic: subtype map

#### 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?

#### Rob Lewis (Oct 31 2019 at 14:25):

subtype.val?

#### 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'

#### 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?

#### Chris Hughes (Oct 31 2019 at 14:43):

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

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

#### Chris Hughes (Oct 31 2019 at 14:45):

You just want discrete.lift subtype.val

#### Chris Hughes (Oct 31 2019 at 14:46):

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

#### Rob Lewis (Oct 31 2019 at 14:46):

You just want discrete.lift subtype.val`

Maybe with some type annotations.

#### Calle Sönne (Oct 31 2019 at 14:48):

Great! Thank you :)

Last updated: May 08 2021 at 04:14 UTC