subtype map

Stream: new members

[Calle Sönne]

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

[Rob Lewis]

subtype.val?

[Calle Sönne]

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

[Calle Sönne]

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]

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

[Rob Lewis]

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]

You just want discrete.lift subtype.val

[Chris Hughes]

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

[Rob Lewis]

You just want discrete.lift subtype.val

Maybe with some type annotations.

[Calle Sönne]

Great! Thank you :)