le notation

Stream: new members

[Calle Sönne]

I have defined a preorder on a bunch of sets and I want to use the ≤ notation, but lean interprets this as the subset relation. Is there anyway I can temporarily "prioritize" the ≤ notation to use this new preorder?

[Johan Commelin]

So the "bunch of sets" is actually "all sets"?

[Calle Sönne]

Johan Commelin said:

So the "bunch of sets" is actually "all sets"?

Oh no, its a certain set of sets

[Johan Commelin]

If you defined bunch_of_sets := _ then Lean shouldn't be able to infer any subset relation whatsoever on it.

[Calle Sönne]

Hmm, this is my definition:

def profinite_skeleton (X : Profinite) :=
{ I : set (set (X.to_Top.α)) | (I.finite) ∧ (∀ U ∈ I, is_open U ∧ U.nonempty) ∧
  (⋃₀ I = univ) ∧ (∀ U V ∈ I, (U ∩ V : set X.to_Top.α).nonempty → (U = V) )}

[Calle Sönne]

So its actually of type set (set (set (X.to_Top.α)))

[Calle Sönne]

When I turned it into a category I had to be very specific to use the right le:

instance profinite_limit_category : small_category (profinite_skeleton X) :=
@preorder.small_category _ (@partial_order.to_preorder _ profinite_skeleton.partial_order)

(I had to learn this the hard way :joy: )

[Johan Commelin]

Well, you can make that a little bit easier by first declaring

instance profinite_limit_category : preorder (profinite_skeleton X) :=
@partial_order.to_preorder _ profinite_skeleton.partial_order

[Johan Commelin]

huh, wait

[Johan Commelin]

Do you already have

instance profinite_limit_category : partial_order (profinite_skeleton X) := _

[Johan Commelin]

The code suggests you do

[Calle Sönne]

yeah

[Johan Commelin]

So how come it doesn't infer that instance?

[Calle Sönne]

Because it uses the wrong one

[Johan Commelin]

Which instance does it find instead when you ask for has_le?

[Johan Commelin]

def foo : has_le (profinite_skeleton X) := by apply_instance

#print foo

[Johan Commelin]

what does that return?

[Calle Sönne]

def Profinite.foo : Π {X : Profinite}, has_le ↥(X.profinite_skeleton) :=
λ {X : Profinite}, preorder.to_has_le ↥(X.profinite_skeleton)

[Calle Sönne]

Johan Commelin said:

Well, you can make that a little bit easier by first declaring

instance profinite_limit_category : preorder (profinite_skeleton X) :=
@partial_order.to_preorder _ profinite_skeleton.partial_order

Oh so my problem is since I dont have this, lean infers another preorder?

[Johan Commelin]

No, you should scratch that first advice

[Johan Commelin]

Could you please print foo with set_option.pp_all true, or maybe pp.implicit if the former yields 5gb of mess.

[Calle Sönne]

def Profinite.foo : Π {X : Profinite}, has_le ↥(X.profinite_skeleton) :=
λ {X : Profinite},
  @preorder.to_has_le ↥(X.profinite_skeleton)
    (@subtype.preorder (set (set (@bundled.α topological_space X.to_Top)))
       (@partial_order.to_preorder (set (set (@bundled.α topological_space X.to_Top)))
          (@order_bot.to_partial_order (set (set (@bundled.α topological_space X.to_Top)))
             (@bounded_lattice.to_order_bot (set (set (@bundled.α topological_space X.to_Top)))
                (@complete_lattice.to_bounded_lattice (set (set (@bundled.α topological_space X.to_Top)))
                   (@set.lattice_set (set (@bundled.α topological_space X.to_Top)))))))
       (λ (x : set (set (@bundled.α topological_space X.to_Top))), x ∈ X.profinite_skeleton))

[Calle Sönne]

So its the topological space that ruins everything?

[Johan Commelin]

Aah! I see. It's the ↥ in has_le ↥(X.profinite_skeleton)

[Johan Commelin]

You define profinite_skeleton as a set, instead of as a new type.

[Johan Commelin]

I'm not sure if you actually want to treat it as a (sub)set, or as a type.

[Johan Commelin]

If you want a type, then change the | into // in the definition of profinite_skeleton.

[Johan Commelin]

That should solve these issues with instances.

[Johan Commelin]

Of course you loose the ability to write x \in profinite_skeleton X, so you have to decide if that's important

[Johan Commelin]

lunch time :running: :bread:

[Calle Sönne]

Thanks!