## Stream: general

### Topic: Knaster-Tarski

#### Kenny Lau (Mar 29 2018 at 04:43):

https://github.com/kckennylau/Lean/blob/master/Knaster-Tarski.lean
@Mario Carneiro por favor diz que nao fazias isso

#### Kenny Lau (Mar 29 2018 at 04:44):

pooh favoh jeez ki now fazeeaish eesoo

#### Kenny Lau (Mar 29 2018 at 04:44):

(that's how I pronounce it)

#### Kenny Lau (Mar 29 2018 at 04:52):

@Kevin Buzzard if you're interested

#### Kenny Lau (Mar 29 2018 at 04:52):

it's related to the link I pm'ed you

#### Mario Carneiro (Mar 29 2018 at 04:54):

Actually I'm a bit surprised it's not there

bom!

#### Mario Carneiro (Mar 29 2018 at 04:55):

I'm certain there's something like it somewhere, but maybe it's not stated on complete lattices

#### Kenny Lau (Mar 29 2018 at 04:55):

I thought it's a theorem of complete lattices

#### Mario Carneiro (Mar 29 2018 at 04:55):

There is a lfp function in ordinal with a similar proof attached

nice

#### Kenny Lau (Mar 29 2018 at 04:56):

that's the theorem about normal ordinal functions right

#### Kenny Lau (Mar 29 2018 at 04:56):

does it have a name?

#### Kenny Lau (Mar 29 2018 at 04:56):

maybe you can prove your lfp using this :D

#### Kenny Lau (Mar 29 2018 at 04:56):

nvm it isn't a complete lattice

#### Mario Carneiro (Mar 29 2018 at 04:56):

is_normal.nfp_fp is what I was thinking of

#### Mario Carneiro (Mar 29 2018 at 04:57):

Dunno, it's not a complete lattice

interesting

#### Mario Carneiro (Mar 29 2018 at 04:57):

Maybe that means there's a hidden abstraction?

well to be fair

#### Mario Carneiro (Mar 29 2018 at 04:57):

like a sup-continuous monotone function

#### Kenny Lau (Mar 29 2018 at 04:57):

your set is well-ordered

hmm

#### Kenny Lau (Mar 29 2018 at 04:58):

but my function isn't sup-continuous

#### Mario Carneiro (Mar 29 2018 at 04:59):

Are you sure? Seems like it follows from the assumptions

#### Mario Carneiro (Mar 29 2018 at 05:00):

Anyway, I think this is why it isn't abstracted :)

look at my aux 3

#### Mario Carneiro (Mar 29 2018 at 05:03):

Why do next and previous take an unused proof argument?

#### Mario Carneiro (Mar 29 2018 at 05:05):

Wouldn't it be nicer to state aux3 for subsets of fixed_points f rather than sets in the subtype?

#### Mario Carneiro (Mar 29 2018 at 05:05):

Then you could skip the subtype.val '' part

#### Kenny Lau (Mar 29 2018 at 05:07):

then how can I use it

#### Kenny Lau (Mar 29 2018 at 05:07):

Why do next and previous take an unused proof argument?

fixed

#### Mario Carneiro (Mar 29 2018 at 05:07):

For the big ol complete_lattice proof, I don't think that's the claim you want. Rather, fixed_points f is a complete sublattice of the powerset

sublattice?

#### Mario Carneiro (Mar 29 2018 at 05:08):

and then you have that construction generally for all sublattices

#### Kenny Lau (Mar 29 2018 at 05:08):

I'm not aware of the existence of sublattices in Lean?

#### Mario Carneiro (Mar 29 2018 at 05:09):

I don't think they exist

#### Mario Carneiro (Mar 29 2018 at 05:09):

But you could just skip the complete_lattice construction and just prove that the sup of fixed points is a fixed point

#### Kenny Lau (Mar 29 2018 at 05:10):

Wouldn't it be nicer to state aux3 for subsets of fixed_points f rather than sets in the subtype?

nope, unprovable

#### Kenny Lau (Mar 29 2018 at 05:11):

wait, misinterpreted

#### Kenny Lau (Mar 29 2018 at 05:11):

But you could just skip the complete_lattice construction and just prove that the sup of fixed points is a fixed point

they aren't

#### Mario Carneiro (Mar 29 2018 at 05:11):

oh, I see, you need that next thing in the middle

#### Mario Carneiro (Mar 29 2018 at 05:12):

Hm, it's something like a retract from set A to fixed_points f

#### Mario Carneiro (Mar 29 2018 at 05:12):

It still strikes me as a generic construction

#### Kenny Lau (Mar 29 2018 at 05:14):

https://github.com/kckennylau/Lean/blob/master/Knaster-Tarski.lean

#### Kenny Lau (Mar 29 2018 at 05:15):

Wouldn't it be nicer to state aux3 for subsets of fixed_points f rather than sets in the subtype?

done. compare aux3 and aux4. aux4 has not been changed. which one is better?

#### Mario Carneiro (Mar 29 2018 at 05:18):

Sup (f '' A) is also expressible as an indexed sup, ⨆ x ∈ A, f x

oh

#### Kenny Lau (Mar 29 2018 at 05:42):

@Mario Carneiro so what is the verdict?

#### Mario Carneiro (Mar 29 2018 at 05:43):

I prefer aux3 since it is more likely to be used as a lemma

and in general?

#### Kenny Lau (Mar 29 2018 at 05:43):

do you find ways of abstracting Knaster-Tarski?

#### Mario Carneiro (Mar 29 2018 at 05:44):

Not anything obvious

#### Kenny Lau (Mar 29 2018 at 05:44):

and is it worth pushing?

#### Mario Carneiro (Mar 29 2018 at 05:44):

I wonder if it works in conditionally complete lattices

yes, PR it

#### Kenny Lau (Mar 29 2018 at 05:44):

what is cc lattices?

#### Mario Carneiro (Mar 29 2018 at 05:45):

@Johannes Hölzl should also weigh in, he's more involved in complete lattice theory than me

#### Mario Carneiro (Mar 29 2018 at 05:45):

real numbers, basically

#### Mario Carneiro (Mar 29 2018 at 05:45):

sup of nonempty bounded sets

#### Kenny Lau (Mar 29 2018 at 05:45):

bot uses top, top uses bot

?

#### Kenny Lau (Mar 29 2018 at 05:45):

I think they can do without each other then

#### Kenny Lau (Mar 29 2018 at 05:46):

the least fixed point is from the top element of the original lattice

#### Kenny Lau (Mar 29 2018 at 05:46):

f(x)=x+1 has no fixed points

sounds legit

#### Kenny Lau (Mar 29 2018 at 05:47):

[0,infty) is downward complete right

#### Kenny Lau (Mar 29 2018 at 05:48):

same example applies

#### Kenny Lau (Mar 29 2018 at 05:52):

[0,1] is complete right

yes

hmm

#### Kenny Lau (Mar 29 2018 at 05:53):

you don’t even need continuity

#### Mario Carneiro (Mar 29 2018 at 05:53):

wait, doesn't that imply banach's fp theorem in 1D?

:open_mouth:

#### Kenny Lau (Mar 29 2018 at 05:54):

maths is beautiful

#### Kenny Lau (Mar 29 2018 at 06:13):

https://github.com/leanprover/mathlib/pull/88

#### Johannes Hölzl (Mar 29 2018 at 06:59):

There is already order/fixed_points.lean in mathlib. It contains lattice.lfp and lattice.gfp to compute the least and greatest fixed point of a function. For conditionally complete lattices: we could add a subtype instance for intervals on conditionally complete lattices. Then $[0, 1] : \mathbb{R}$ would be a complete lattice.

fair enough

#### Johannes Hölzl (Mar 29 2018 at 07:06):

Your next and previous function can be represented using the gfp and lfp: e.g. gfp (λz, x ⊔ f z) = Sup {z | z ≤ x ⊔ f z}. Then you can use the lfp and gfp properties.

#### Kenny Lau (Mar 29 2018 at 07:07):

so you're just going to close my PR?

#### Johannes Hölzl (Mar 29 2018 at 07:08):

No, I don't want to close it. I would like to see the fixed point lattice in order/fixed_points.lean. And using the constants and proofs we already have.

oh ok

#### Kenny Lau (Mar 29 2018 at 07:08):

are you going to edit it or am I going to edit it?

#### Johannes Hölzl (Mar 29 2018 at 07:10):

Of course, if you want you can edit it! I have a couple more changes: rename aux1..4 to something useful and replace is_ord_hom by the assumption monotone f, also going from type class to just assumption.

#### Kenny Lau (Mar 29 2018 at 08:43):

how would you rename aux1..4? @Johannes Hölzl

#### Johannes Hölzl (Mar 29 2018 at 08:48):

something like sup_le_f_sup_of_fixed_points?

#### Kenny Lau (Mar 29 2018 at 08:48):

ach fur gottesliebe

#### Kenny Lau (Mar 29 2018 at 08:49):

that's 10 times as long

#### Kevin Buzzard (Mar 29 2018 at 08:49):

and more descriptive too ;-)

#### Kenny Lau (Mar 29 2018 at 08:50):

do you use f in names?

#### Kevin Buzzard (Mar 29 2018 at 08:50):

Wait -- aren't you and I editing some schemes files with function names like structure_sheaf_of_rings_on_affine_scheme ?

#### Kenny Lau (Mar 29 2018 at 08:50):

my mind replaces f with apply in names

#### Kenny Lau (Mar 29 2018 at 08:50):

yes, and it's always you who type it :P

#### Kevin Buzzard (Mar 29 2018 at 08:51):

definition structure_sheaf_of_rings_on_affine_scheme (R : Type*) [comm_ring R] : is_sheaf_of_rings (structure_presheaf_of_rings_on_affine_scheme R) :=... :-)

#### Kevin Buzzard (Mar 29 2018 at 08:51):

well Mario told me I couldn't use tag00EJ...

#### Kenny Lau (Mar 29 2018 at 08:51):

I never typed it :P

#### Kevin Buzzard (Mar 29 2018 at 08:51):

Perhaps tag00EJ is as bad as aux1 right? ;-)

#### Kenny Lau (Mar 29 2018 at 08:52):

right

Last updated: May 13 2021 at 00:41 UTC