Quotient of linear order is linear order

Stream: Is there code for X?

[Violeta Hernández]

Suppose LinearOrder α and Setoid α, such that every equivalence class (preimage of mk) is docs#Set.OrdConnected. Then one can define a LinearOrder (Quotient α) in a semi-obvious way.

[Violeta Hernández]

Do we have anything like this in Mathlib?

[Yan Yablonovskiy 🇺🇦]

Violeta Hernández said:

Suppose LinearOrder α and Setoid α, such that every equivalence class (preimage of mk) is docs#Set.OrdConnected. Then one can define a LinearOrder (Quotient α) in a semi-obvious way.

Would you say this has some relation to #28278 ?

[Violeta Hernández]

I don't think so, no

[Violeta Hernández]

After loogling around for a bit, I don't think we have this.

[Violeta Hernández]

How should I implement it? It's hard to prove results about the linear order without making an instance, but I can't make an instance without wrapping the "every equivalence class is OrdConnected" hypothesis in a typeclass. Is it acceptable to make a new typeclass just for this?

[Violeta Hernández]

Should I use Quotient, or should I write this down in some other way?

[Weiyi Wang]

Using Quotient directly has the problem that if one wants to apply this to existing type (like your original example IsLocalRing.ResidueField), one will need to pierce defeq to use the underlying Quotient type

[Violeta Hernández]

Yes, but I think that's just the existing design

[Violeta Hernández]

QuotLike never made it into Mathlib

[Aaron Liu]

Violeta Hernández said:

QuotLike never made it into Mathlib

Don't give up, we can still do it

[Violeta Hernández]

#16210, #16421, #16428, #17127

[Violeta Hernández]

@Yuyang Zhao What would be needed to push these PRs through?

[Violeta Hernández]

Regarding my first point, I don't need to make a new typeclass, because for some reason OrdConnected is already a class:

abbrev LinearlyOrderedQuotient : Prop :=
  ∀ x, OrdConnected (Quotient.mk s ⁻¹' {x})

[Weiyi Wang]

What if we don't mention Quotient at all? The API can look like LinearOrder.descend [LinearOrder a] (f : a -> b) (h : Function.Surjective f) (hconnected : ∀ x y z, f x = f y -> z \in Set.Icc x y \to f x = f z) : LinearOrder b
(Not sure if I put the correct hypothesis)

[Violeta Hernández]

This makes sense. But I still have the problem of "how do I give any API if I don't have an instance"?

[Violeta Hernández]

e.g. if I wanted to prove some result of the form x ≤ y → ... for this linear order, I couldn't, since I don't have a LE instance, unless I painstakingly wrote (LinearOrder.descend f _ _).toPartialOrder.toPreorder.toLE.le x y every single time

[Aaron Liu]

take advantage of the defeqs

[Violeta Hernández]

wdym?

[Aaron Liu]

what kind of results are you wanting to prove

[Violeta Hernández]

here's a simple one:

theorem le_congr_left (hx : x₁ ≈ x₂) (hy : ¬ x₁ ≈ y) : x₁ ≤ y ↔ x₂ ≤ y := sorry

[Violeta Hernández]

of course there's analogous results le_congr_right, and lt_congr_left, and lt_congr_right

[Violeta Hernández]

and of course, once the LinearOrder is constructed, the fact that mk is monotone is another important fact

[Aaron Liu]

tricky

[Violeta Hernández]

Weiyi Wang said:

What if we don't mention Quotient at all? The API can look like LinearOrder.descend [LinearOrder a] (f : a -> b) (h : Function.Surjective f) (hconnected : ∀ x y z, f x = f y -> z \in Set.Icc x y \to f x = f z) : LinearOrder b
(Not sure if I put the correct hypothesis)

An unfortunate consequence of not using Quotient is that we don't get Quotient.lift, and as a result, we don't get a decidable linear order

[Aaron Liu]

oh no

[Eric Wieser]

I think a special case for Quotient is reasonable here

[Eric Wieser]

Violeta Hernández said:

unless I painstakingly wrote (LinearOrder.descend f _ _).toPartialOrder.toPreorder.toLE.le x y every single time

letI := LinearOrder.descend f _ _; x <= y

[Violeta Hernández]

Just to be completely explicit, my design proposal is the following:

import Mathlib.Order.Interval.Set.OrdConnected

open Set

variable {α : Type*} {s : Setoid α} [LinearOrder α]

variable (s) in
abbrev LinearlyOrderedQuotient : Prop :=
  ∀ x, OrdConnected (Quotient.mk s ⁻¹' {x})

instance Quotient.linearOrder [LinearlyOrderedQuotient s] : LinearOrder (Quotient s) :=
  sorry

Does this seem reasonable?

[Weiyi Wang]

If we do the LinearOrder.descend way, I think what you can do is

def LinearOrder.descendLE (.....) : b -> b -> Prop := ...
--define some good API
theorem LinearOrder.descendLE_apply_apply (...) : LinearOrder.descendLE  (f a) (f b) \iff ...
...
abbrev LinearOrder.descend(...) : LinearOrder b where
  le := LinearOrder.descendLE
  ...

And then on the use site, you use LinearOrder.descendLE_apply_apply and freinds to rewrite it.

I think this is how LinearOrder.lift' is supposed to be used, except that its definition is pretty simple so it doesn't need to be separately defined

[Weiyi Wang]

It also has a note at https://github.com/leanprover-community/mathlib4/blob/540f08201fa427d86387cfabf20e7090e1db965e/Mathlib/Algebra/HierarchyDesign.lean#L188-L203

[Violeta Hernández]

This doesn't really gain us much if I use Quotient, because in either case I need to use the hypothesis that equivalence classes are order connected to define the ordering computably

[Eric Wieser]

Weiyi Wang said:

I think this is how LinearOrder.lift' is supposed to be used,

Generally speaking I would claim that docs#LinearOrder.lift' is not supported to be used (at least, not in any definitions)

[Eric Wieser]

Elsewhere instead of using [SomeTypeclass (s : Setoid X)] we use class SomeSetoid extends Setoid, eg docs#Con, docs#RingCon

[Violeta Hernández]

I think my design questions are two:

• is it fine to make this ad-hoc LinearOrderedQuotient abbrev?
• is it fine to register this as a LinearOrder (Quotient s) instance? (i.e. is it safe to assume this won't cause diamonds?)

[Eric Wieser]

Does this overlap with #26836 ?

[Violeta Hernández]

Eric Wieser said:

Elsewhere instead of using [SomeTypeclass (s : Setoid X)] we use class SomeSetoid extends Setoid, eg docs#Con, docs#RingCon

What about making a LinearOrderedSetoid typeclass then, with the assumption that all preimages are order connected, and building a LinearOrder from that assumption?

[Eric Wieser]

Is LatticeCon equivalent?

[Aaron Liu]

no

[Aaron Liu]

in fact, on a linear order LatticeCon is trivial (satisfied by all setoids)

[Aaron Liu]

this follows pretty easily from docs#min_cases and docs#max_cases

[Aaron Liu]

actually I should probably check

[Aaron Liu]

I think that might be not true

[Eric Wieser]

Maybe I should ask a different question; does a c : LinearOrderedCon on a lattice permit a Lattice (Quotient c) instance?

[Violeta Hernández]

Does r w x → r y z → r w z? I don't think that's true

[Aaron Liu]

it's not true

[Aaron Liu]

sorry for lying everyone

[Aaron Liu]

the condition for it to be true seems to be that the equivalence classes are docs#OrdConnected which is what @Eric Wieser said

[Violeta Hernández]

Yes, I think that if the equivalence classes in a linear order are OrdConnected then you do in fact have a LatticeCon

[Aaron Liu]

and the converse too of course

[Violeta Hernández]

The converse too?

[Violeta Hernández]

That's surprising to hear

[Violeta Hernández]

Eric Wieser said:

Maybe I should ask a different question; does a c : LinearOrderedCon on a lattice permit a Lattice (Quotient c) instance?

Isn't the LatticeCon condition precisely what you need for this?

[Eric Wieser]

Sure, really I'm just asking if one of these definitions suffices for both use cases, and Aaron tricked me into thinking I had it the wrong way around

[Eric Wieser]

If they're equivalent then LatticeCon is the right definition and yours can be a helper constructor

[Aaron Liu]

if you're not OrdConnected then there's x < y < z with r x z but ¬r y z so we have that r x z and r y y but ¬r (max x y) (max z y)

[Aaron Liu]

I hope that's not a lie

[Violeta Hernández]

That seems correct

[Aaron Liu]

Eric Wieser said:

Sure, really I'm just asking if one of these definitions suffices for both use cases, and Aaron tricked me into thinking I had it the wrong way around

you believed me

[Violeta Hernández]

Just asked on the LatticeCon PR to see if there was any progress

[Violeta Hernández]

hopefully the author is still around and willing to continue it

[Eric Wieser]

Actually that's also the wrong definition

[Violeta Hernández]

what do you mean :sob:

[Eric Wieser]

We want OrderCon with r w x -> r y z -> w ≤ y <-> x ≤ z or similar

[Eric Wieser]

You can make the iff an implication as r w x -> x ≤ y -> r y z -> w ≤ z, but I'm not sure if that's actually more convenient

[Eric Wieser]

Crucially that's exactly the property needed to lift LE

[Eric Wieser]

I guess you could require something similar for LT, though maybe that's only relevant for very useless generality

[Violeta Hernández]

Don't lattices have an inherent notion of ≤ though?

[Eric Wieser]

Sure, but my OrderCon works on partial orders that aren't lattices

[Violeta Hernández]

I see

[Eric Wieser]

Then you can prove things like "order congruences preserve lattice operations"

[Violeta Hernández]

So, what would my "setoid where equivalence classes are order connected" translate into? Just OrderCon on a LinearOrder? Or would you also need LatticeCon?

[Eric Wieser]

The former

[Violeta Hernández]

Are all of these true?

• An OrderCon on a Preorder defines a Preorder instance on the quotient
• the same for partial orders
• the same for linear orders

[Violeta Hernández]

...no, I think there's something wrong

[Violeta Hernández]

Eric Wieser said:

We want OrderCon with r w x -> r y z -> w ≤ y <-> x ≤ z or similar

The trivial relation does not satisfy this, but it does satisfy that all equivalence classes are order connected (the only equivalence class is univ)

[Violeta Hernández]

that's also why I said the linear order on the quotient was "semi-obvious"

[Aaron Liu]

why can't we just use Relation.ReflTransGen fun x y => x ≤ y ∨ r x y ∨ r y x

[Violeta Hernández]

it requires some subtlety because of this

[Aaron Liu]

as the LE relation I mean

[Aaron Liu]

I guess it's already refl so only the trans gen

[Aaron Liu]

and you also don't need r y x since it's symmetric

[Violeta Hernández]

Aaron Liu said:

why can't we just use Relation.ReflTransGen fun x y => x ≤ y ∨ r x y ∨ r y x

r x y ∨ x ≤ y should be enough

[Aaron Liu]

so what I really mean is Relation.TransGen fun x y => x ≤ y ∨ r x y

[Violeta Hernández]

Why do you need the TransGen?

[Aaron Liu]

obviously so you get transitivity

[Aaron Liu]

I think this is also the quotient object in the category of preorders

[Violeta Hernández]

if the equivalence classes are OrdConnected you already have transitivity

[Aaron Liu]

Violeta Hernández said:

if the equivalence classes are OrdConnected you already have transitivity

and if they're not then you need a docs#Relation.TransGen

[Violeta Hernández]

Ah, I get your point

[Aaron Liu]

you get for example that this quotient order is the specialization preorder of the quotient topology of the specialization topology (docs#Topology.upperSet) of the original order

[Aaron Liu]

probably

[Violeta Hernández]

Aaron Liu said:

I think this is also the quotient object in the category of preorders

What does this mean in English

[Violeta Hernández]

What's the relevant universal property?

[Aaron Liu]

uhhm

[Aaron Liu]

the quotient map is monotone and respects the equivalence classes, and also, any monotone map which also respects the equivalence classes lifts to a monotone map out of the quotient order making the triangle commute

[Aaron Liu]

or "descends" if you draw your diagrams right side up

[Aaron Liu]

wait I thought you were learning category theory?

[Violeta Hernández]

Yes I didn't say I was any good at it just yet

[Violeta Hernández]

Haven't seen quotient objects yet

[Aaron Liu]

I still have no idea what a quotient object is supposed to be

[Aaron Liu]

this is just what felt right

[Violeta Hernández]

So, new proposal

[Aaron Liu]

basically I copied it from https://xenaproject.wordpress.com/2025/02/09/what-is-a-quotient/

[Violeta Hernández]

What about making a Preorder α → Preorder (Quotient s) instance with this definition?

[Aaron Liu]

this sounds like a thing that can be done

[Violeta Hernández]

Or if it's unacceptable to be making instances this generic, perhaps we make a type alias doing something similar?

[Aaron Liu]

we have lots of other quotient instances what's wrong with this one

[Violeta Hernández]

Well I fear it might clash with something else

[Aaron Liu]

clash with what

[Violeta Hernández]

e.g. we already define an order instance on surreals, and that's also a quotient

[Weiyi Wang]

It can clash with quotient defined with docs#Antisymmetrization (?)

[Violeta Hernández]

both of these should be equivalent to what we want to define, mind you

[Violeta Hernández]

but they have way better def-eqs

[Violeta Hernández]

e.g. in the antisymmetrization case, TransGen fun x y ↦ r x y ∨ x ≤ y reduces to just x ≤ y

[Aaron Liu]

ok so the "map" of a Preorder α by a function f : α → β is the Preorder β where x ≤ y ↔ ∀ s : Set β, IsUpperSet (f ⁻¹' s) → x ∈ s → y ∈ s

[Aaron Liu]

and the quotient order is the map of the order along the quotient map

[Aaron Liu]

and this map is a left adjoint

[Aaron Liu]

to the comap of an order which for a Preorder β and f : α → β is the Preorder α where x ≤ y ↔ f x ≤ f y

[Aaron Liu]

and the order on preorders is the one induced from the ordering on relations where we identify a preorder with its LE relation

[Aaron Liu]

did I get that right

[Violeta Hernández]

it feels correct?

[Aaron Liu]

I copied over all the stuff from topological spaces which I know very well

[Violeta Hernández]

so yet again the question is "how do we make API out of this"

[Aaron Liu]

same as all the other quotient apis I guess

[Aaron Liu]

until that quotientlike thing lands

[Aaron Liu]

It'd be great if this map has a better characterization

[Aaron Liu]

right now I have to do this thing with sets

[Violeta Hernández]

is the transgen thing you said incorrect?

[Violeta Hernández]

Aaron Liu said:

so what I really mean is Relation.TransGen fun x y => x ≤ y ∨ r x y

Something funny about this definition is that it gives a preorder with no further assumptions on ≤

[Violeta Hernández]

is that... intended?

[Violeta Hernández]

Aaron Liu said:

the quotient map is monotone and respects the equivalence classes, and also, any monotone map which also respects the equivalence classes lifts to a monotone map out of the quotient order making the triangle commute

Is this the correct way to write this in Lean?

theorem lift_monotone {α β : Type*} [Preorder α] {s : Setoid α} [Preorder β]
    (f : α → β) (hf : Monotone f) (H : ∀ x₁ x₂, x₁ ≈ x₂ → f x₁ = f x₂) :
    Monotone (Quotient.lift f H) := by
  sorry

[Violeta Hernández]

because I can prove this is true using the transgen definition

[Violeta Hernández]

Though it's also worth pointing out that in general this quotient doesn't preserve the partial order or linear order properties

[Violeta Hernández]

...are we sure this is a useful definition?

[Violeta Hernández]

Because if the idea is just "give some undecidable ≤ relation that happens to coincide with what I want in the linear order with order connected equivalence classes case" we could have just gone with LinearOrder.lift' Quotient.out

[Violeta Hernández]

Well after asking around for a bit I think this is the correct quotient, categorically speaking

[Violeta Hernández]

I guess what I really need to do is prove that under these stronger conditions on the equivalence classes, the ≤ relation can be nicely rewritten

[Violeta Hernández]

Just opened #29735 doing this

[Eric Wieser]

I don't think we care about the preorder case; if we're taking a Quotient under a transitive relation I think it's reasonable to require any relation we lift to also be transitive

[Eric Wieser]

I think the typeclass should be the conditions necessary to make mk x ≤ mk y defeq to x ≤ y

[Aaron Liu]

Eric Wieser said:

I think the typeclass should be the conditions necessary to make mk x ≤ mk y defeq to x ≤ y

Well that doesn't with fur the case we do care about, linear orders with convex equivalence classes

[Aaron Liu]

Violeta Hernández said:

...are we sure this is a useful definition?

I'm sure this is the natural definition

[Aaron Liu]

Violeta Hernández said:

Aaron Liu said:

the quotient map is monotone and respects the equivalence classes, and also, any monotone map which also respects the equivalence classes lifts to a monotone map out of the quotient order making the triangle commute

Is this the correct way to write this in Lean?

theorem lift_monotone {α β : Type*} [Preorder α] {s : Setoid α} [Preorder β]
    (f : α → β) (hf : Monotone f) (H : ∀ x₁ x₂, x₁ ≈ x₂ → f x₁ = f x₂) :
    Monotone (Quotient.lift f H) := by
  sorry

yes that looks good but don't forget to prove the quotient mk map is monotone too

[Aaron Liu]

Violeta Hernández said:

because I can prove this is true using the transgen definition

yes that sounds correct

[Aaron Liu]

Violeta Hernández said:

Because if the idea is just "give some undecidable ≤ relation that happens to coincide with what I want in the linear order with order connected equivalence classes case" we could have just gone with LinearOrder.lift' Quotient.out

but that doesn't satisfy that amazing quotient property (the quotient mk map isn't monotone)

[Aaron Liu]

Violeta Hernández said:

...are we sure this is a useful definition?

it's the correct definition, I'm sure someone will find it useful eventually

[Aaron Liu]

Violeta Hernández said:

Aaron Liu said:

so what I really mean is Relation.TransGen fun x y => x ≤ y ∨ r x y

Something funny about this definition is that it gives a preorder with no further assumptions on ≤

yeah this actually gives the quotient order on the preorder generated by the LE relation, since the preorders are a reflective subcategory of the relations

[Aaron Liu]

Violeta Hernández said:

is the transgen thing you said incorrect?

it's equivalent it's an explicit formula but apparently people don't like formulas and defining it with the map lets you map along functions which aren't Quotient.mk

[Kenny Lau]

Aaron Liu said:

Eric Wieser said:

I think the typeclass should be the conditions necessary to make mk x ≤ mk y defeq to x ≤ y

Well that doesn't with fur the case we do care about, linear orders with convex equivalence classes

how does that not work?

[Aaron Liu]

If x and y are different but in the same equivalence class then mk x = mk but clearly x < y or y < x

[Kenny Lau]

oh, right...

[Eric Wieser]

Why does that impact le? Isn't that only about lt?

[Kenny Lau]

@Eric Wieser let's say you make [0,1] into one point, then mk 0 = mk 1, which also means mk 1 <= mk 0, but 1 <= 0 is false

[Kenny Lau]

< also has the same problem, 0 < 1 is true, but mk 0 < mk 1 is false

[Aaron Liu]

There's another definition, which is "the finest preorder meaning the quotient map monotone"

[Aaron Liu]

There's a lot of ways to make the same thing

[Yaël Dillies]

Btw, once you've defined those mapping instances, you can use them to golf the ones on docs#Antisymmetrization

[Violeta Hernández]

Yaël Dillies said:

Btw, once you've defined those mapping instances, you can use them to golf the ones on docs#Antisymmetrization

I don't think I can, because Antisymmetrization is defined in terms of an unbundled relation rather than a preordered type

[Weiyi Wang]

I remember Antisymmetrization is somewhat inconsistent in API, where the basic definition uses unbundled, but a lot of lemmas require bundled

[Yaël Dillies]

You definitely can. Look at the partial order instance

[Violeta Hernández]

There's also the separate problem that we'd get much worse def-eqs using the new "preorder on quotients" instance

[Violeta Hernández]

in the special case of the antisymmetrization, ≤ directly lifts to the quotient

[Violeta Hernández]

Well, independently of any future golfs and improvements, I'd like to know if the design I used in #29735 makes sense, i.e.

• should we have such a general instance Preorder (Quotient s)?
• is the weird typeclass assumption ∀ x, OrdConnected (mk ⁻¹' {x}) ok to have?

I'd like to make use of the LinearOrder typeclass on a subsequent PR, so I think these are important questions to answer before any further review

[Weiyi Wang]

Would this surprise users by giving them unexpected order on Quotient? Should it be a scoped instance?

[Aaron Liu]

do you have another better order on Quotient

[Violeta Hernández]

for specific Quotients such as the antisymmetrization, we do

[Aaron Liu]

well docs#Antisymmetrization is a def not an abbrev so we can override it with our own implementation

[Weiyi Wang]

Aaron Liu said:

do you have another better order on Quotient

for example, if one defines Rat as a Quotient of integer pairs, they don't want the order from the product order

[Violeta Hernández]

I think it makes sense to make this a scoped instance, just in case

[Violeta Hernández]

what would the scope be? Quotient?

[Aaron Liu]

well if one defines Rat as a Quotient of integer pairs they also don't want the topology from the product topology

[Aaron Liu]

but topology is an instance

[Weiyi Wang]

Right, so I don't have strong opinion on this. Just mention it in case someone thinks it is a problem

[Violeta Hernández]

Aaron Liu said:

but topology is an instance

Is there a TopologicalSpace (Quotient s) instance in Mathlib?

[Aaron Liu]

@loogle |- TopologicalSpace (Quotient _)

[loogle]

:search: instTopologicalSpaceQuotient, DiscreteQuotient.instTopologicalSpaceQuotient

[Aaron Liu]

looks like there's actually two

[Yakov Pechersky]

What order does this induce on ZMod n for positive n, if it was implemented via a quotient?

[Kenny Lau]

probably the order where everything is <= everything

[Aaron Liu]

Yakov Pechersky said:

What order does this induce on ZMod n for positive n, if it was implemented via a quotient?

the trivial order whose docs#Antisymmetrization is a singleton

[Yakov Pechersky]

Then I don't think a trivial order is worth setting on types globally

[Aaron Liu]

There's not really any other choice

[Aaron Liu]

and it's not always a trivial order

[Aaron Liu]

Just we want the quotient map to be monotone and the trivial order is the only one that does that for ZMod

[Kenny Lau]

Aaron Liu said:

There's not really any other choice

just don't make it an instance

[Aaron Liu]

why not an instance again?

[Aaron Liu]

what will it be bad for?

[Aaron Liu]

we already have the instances for docs#Prod docs#Sum docs#Subtype

[Aaron Liu]

what's the argument for why this is bad as an instance

[Kenny Lau]

I just don't think (yet) that it's canonical enough, the one one Prod is already a problem, the fact that you need Lex as a type synonym shows that it's not canonical

[Aaron Liu]

was the universal property not enough

[Aaron Liu]

how about this

[Aaron Liu]

it lets you glue together hasse diagrams

[Aaron Liu]

for example if I have Σ _ : Nat, Fin 2 and I quotient it by the relation generated by ⟨n, 1⟩ ≈ ⟨n + 1, 0⟩ then the resulting order is order-isomorphic to Nat

[Kenny Lau]

i don't know enough to comment

[Yakov Pechersky]

I think it would be surprising if the order on ZMod suddenly changed from the order one gets from Fin or Int, which is the one from Nat, to one that has terms indistinguishable by the order.

[Kenny Lau]

but ZMod is not (implemented as) a quotient

[Aaron Liu]

well it will not, since ZMod isn't defined in terms of Quotient

[Weiyi Wang]

Is it correct to say that a global instance will only impact direct use of Quotient and those defined with abbrev ... = Quotient..., but will not impact those with def ... = Quotient...?

[Kenny Lau]

correct

[Weiyi Wang]

Yeah, then I think I am fine with it, as I don't expect mathlib to have many abbrevs. We might want to check them individually to ensure none of them accidentally gets a weird order, if there is any

[Aaron Liu]

well if we aren't using it for the order who cares

[Aaron Liu]

and if we are using it for the order it probably shouldn't be abbrev

[Violeta Hernández]

I have no problem with making the instance scoped. There's a bit of def-eq finangling I need to do to get to use it in my application no matter what.

[Aaron Liu]

a bit curious what is the application

[Violeta Hernández]

It's something I was discussing on another thread

[Violeta Hernández]

Generalizing the standard part function from hyperreals to a non-archimedean field

[Violeta Hernández]

That requires me to give a linear order instance on the residue field of the subring of finite elements (i.e. non-negative archimedean class)

[Violeta Hernández]

It all comes back to the surreal numbers lol

[Aaron Liu]

oh I remember now

[Aaron Liu]

Violeta Hernández said:

I have no problem with making the instance scoped. There's a bit of def-eq finangling I need to do to get to use it in my application no matter what.

do you care about the defeqs?

[Violeta Hernández]

Aaron Liu said:

Violeta Hernández said:

I have no problem with making the instance scoped. There's a bit of def-eq finangling I need to do to get to use it in my application no matter what.

do you care about the defeqs?

I really just need a linear order instance that's equivalent to x ≤ y or mk x = mk y in my specific case

[Violeta Hernández]

by def-eq finangling I mean "I had to write the instances explicitly"
image.png

[Aaron Liu]

uhm sure

[Violeta Hernández]

Am I correct in saying docs#LinearOrderedField.inducedOrderRingHom_toFun is a bad simp lemma? You lose the RingHom structure for no reason

[Weiyi Wang]

That seams to be a common pattern for a lot of @[simps]-generated lemma. Whenever a bundled function is applied to an element, it is simped to the bare function

[Violeta Hernández]

Well, the difference here is that this embedding has no interesting inner structure

[Weiyi Wang]

Yeah that sounds like a good argument

[Violeta Hernández]

you're just turning some essentially arbitrary order ring hom into an essentially arbitrary add monoid hom

[Violeta Hernández]

i.e. you're losing structure and gaining nothing

[Violeta Hernández]

In fact, I'm not sure why we have both the add-hom and order-ring-hom version when both take in the same hypotheses

[Violeta Hernández]

if you can use the former, you can use the latter

[Weiyi Wang]

Would you support it if I replace the entire Mathlib.Algebra.Order.CompleteField with #27566 (after replacing \R with ConditionallyCompleteLinearOrderedField in my code)?
Then you get a AddMonoidHom and a RingHom that actually require different things

[Violeta Hernández]

Yes, I think that would be a good change.

[Violeta Hernández]

Well, I haven't taken a look at your PR, but the idea of having different hypotheses for both of these maps makes sense to me

[Weiyi Wang]

Yeah, addMonoidHom is docs#Archimedean.embedReal, which downgrades the domain to an AddCommGroup

[Yuyang Zhao]

Violeta Hernández said:

Yuyang Zhao What would be needed to push these PRs through?

Still waiting for the discussion here, but nobody has participated in a long time.

[Eric Paul]

Just saw this and wanted to say that I would love to have this quotient of linear orders in mathlib as it's used in things I want to formalize. I don't know if it's helpful, but I normally see an equivalence relation such that all classes are OrdConnected called a convex equivalence relation and the resulting quotient called a condensation.

[Violeta Hernández]

@Eric Paul my PR exists here: #29735