Type expected error

Stream: maths

[Ashvni Narayanan]

I am trying to define dir_sys as the following : a collection of finite sets (X_i)_{i ∈ ℕ} such that for j ≤ i, there exists a surjective map π_{ij} such that for k ≤ j ≤ i, π_{ij} ∘ π_{jk} = π_{ik}. I get stuck here:

import ring_theory.int.basic
import set_theory.zfc

structure dir_sys :=
( α : Type* )
(h : ℕ → finset α )
(sys : ∀ i j : ℕ, j ≤ i → ∃ f : (h i).1 → (h j).1, function.surjective f )

The error I get is :

type expected at
  (h i).val
term has type
  quot setoid.r

I don't understand the error. Does Lean want me to specify the type of (h i).val? Any help is appreciated, thank you!

[Eric Wieser]

Adding an explicit ↥ might help

[Eric Wieser]

↥(h i).1 → ↥(h j).1 or similar

[Eric Wieser]

Why the .1 which turns your finset into a multiset?

[Ashvni Narayanan]

Eric Wieser said:

Adding an explicit ↥ might help

I get the following error :

type expected at
  ↥(h i)
term has type
  has_coe_to_sort.S (finset α)

[Ashvni Narayanan]

Eric Wieser said:

Why the .1 which turns your finset into a multiset?

I was just experimenting..

[Kevin Buzzard]

My instinct is that we might already have some far more general kind of directed systems in mathlib already. I think that the functions themselves should be part of the data, not just some assumption that they exist. Might it be easier to work with types rather than finsets, which are terms?

[Eric Wieser]

We have docs#direct_limit which seems to have some things in common with what you're after

[Eric Wieser]

This works:

import data.finset.basic

structure dir_sys :=
( α : Type* )
(h : ℕ → finset α )
(sys : ∀ i j : ℕ, j ≤ i → ∃ f : (h i : set α) → (h j : set α), function.surjective f )

[Eric Wieser]

finset has no coercion to sort

[Eric Wieser]

Only coercion to set, which then has a coercion to sort