Zulip Chat Archive

Stream: new members

Topic: Opposite order `nonempty_sections_of_fintype_inverse_system`

Junyan Xu (Sep 03 2022 at 23:18):

@Rémi Bottinelli It's easier to derive the desired result from docs#nonempty_sections_of_fintype_cofiltered_system by mimicking the proof of src#nonempty_sections_of_fintype_inverse_system:

import topology.category.Top.limits

universes u v

variables {J : Type u} [preorder J] [is_directed J ge] (F : J  Type v)

theorem nonempty_sections_of_fintype_inverse_system'
 [fin : Π (j : J), fintype (F.obj j)] [nempty :  (j : J), nonempty (F.obj j)] : F.sections.nonempty :=
  casesI is_empty_or_nonempty J,
  { exact is_empty_elim, is_empty_elim⟩, },
  { exact nonempty_sections_of_fintype_cofiltered_system _, },

Junyan Xu (Sep 03 2022 at 23:22):

I think the error you get is due to the category structure you get from
Joppreo : preorder Jᵒᵖ ⟿ category Jᵒᵖ is different from
preorder J ⟿ category J ⟿ category Jᵒᵖ,
which is known as a diamond.
(normally you would get the opposite preorder using docs#order_dual Jᵒᵈ instead of Jᵒᵖ, but then you won't be able to use category_theory.op_op.)

Last updated: Dec 20 2023 at 11:08 UTC