Commit 2025-01-20 11:09 3bf4857a

View on Github →

chore(Order): split GaloisConnection into Defs.lean and Basic.lean (#20798) The main reason for this PR is noticing that NNRat brings in a lot of order theory: Mathlib.Data.NNRat.Defs.pdf. We don't actually need to know what a boolean algebra is, or even a complete lattice, to define NNRat.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Floor/Div.lean

Modified Mathlib/CategoryTheory/Category/GaloisConnection.lean

Modified Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/Data/Setoid/Basic.lean

Modified Mathlib/Order/Closure.lean

Modified Mathlib/Order/Cofinal.lean

Renamed Mathlib/Order/GaloisConnection.lean to Mathlib/Order/GaloisConnection/Basic.lean

deleted def GaloisCoinsertion.dual

deleted theorem GaloisCoinsertion.l_injective

deleted theorem GaloisCoinsertion.l_le_l_iff

deleted def GaloisCoinsertion.monotoneIntro

deleted def GaloisCoinsertion.ofDual

deleted theorem GaloisCoinsertion.strictMono_l

deleted theorem GaloisCoinsertion.u_bot

deleted theorem GaloisCoinsertion.u_l_eq

deleted theorem GaloisCoinsertion.u_l_leftInverse

deleted theorem GaloisCoinsertion.u_surjective

deleted structure GaloisCoinsertion

deleted theorem GaloisConnection.exists_eq_l

deleted theorem GaloisConnection.exists_eq_u

deleted theorem GaloisConnection.l_bot

deleted theorem GaloisConnection.l_comm_iff_u_comm

deleted theorem GaloisConnection.l_comm_of_u_comm

deleted theorem GaloisConnection.l_eq

deleted theorem GaloisConnection.l_eq_bot

deleted theorem GaloisConnection.l_le

deleted theorem GaloisConnection.l_u_bot

deleted theorem GaloisConnection.l_u_l_eq_l'

deleted theorem GaloisConnection.l_u_l_eq_l

deleted theorem GaloisConnection.l_u_le

deleted theorem GaloisConnection.l_u_le_trans

deleted theorem GaloisConnection.l_unique

deleted theorem GaloisConnection.le_iff_le

deleted theorem GaloisConnection.le_u

deleted theorem GaloisConnection.le_u_l

deleted theorem GaloisConnection.le_u_l_trans

deleted def GaloisConnection.liftOrderBot

deleted def GaloisConnection.liftOrderTop

deleted theorem GaloisConnection.lt_iff_lt

deleted theorem GaloisConnection.monotone_intro

deleted theorem GaloisConnection.monotone_l

deleted theorem GaloisConnection.monotone_u

deleted def GaloisConnection.toGaloisCoinsertion

deleted def GaloisConnection.toGaloisInsertion

deleted theorem GaloisConnection.u_comm_of_l_comm

deleted theorem GaloisConnection.u_eq

deleted theorem GaloisConnection.u_eq_top

deleted theorem GaloisConnection.u_l_top

deleted theorem GaloisConnection.u_l_u_eq_u'

deleted theorem GaloisConnection.u_l_u_eq_u

deleted theorem GaloisConnection.u_top

deleted theorem GaloisConnection.u_unique

deleted def GaloisConnection

deleted def GaloisInsertion.dual

deleted theorem GaloisInsertion.l_surjective

deleted theorem GaloisInsertion.l_top

deleted theorem GaloisInsertion.l_u_eq

deleted theorem GaloisInsertion.leftInverse_l_u

deleted def GaloisInsertion.monotoneIntro

deleted def GaloisInsertion.ofDual

deleted theorem GaloisInsertion.strictMono_u

deleted theorem GaloisInsertion.u_injective

deleted theorem GaloisInsertion.u_le_u_iff

deleted structure GaloisInsertion

deleted theorem OrderIso.to_galoisConnection

Created Mathlib/Order/GaloisConnection/Defs.lean

added def GaloisCoinsertion.dual

added theorem GaloisCoinsertion.l_injective

added theorem GaloisCoinsertion.l_le_l_iff

added def GaloisCoinsertion.monotoneIntro

added def GaloisCoinsertion.ofDual

added theorem GaloisCoinsertion.strictMono_l

added theorem GaloisCoinsertion.u_bot

added theorem GaloisCoinsertion.u_l_eq

added theorem GaloisCoinsertion.u_l_leftInverse

added theorem GaloisCoinsertion.u_surjective

added structure GaloisCoinsertion

added theorem GaloisConnection.exists_eq_l

added theorem GaloisConnection.exists_eq_u

added theorem GaloisConnection.l_bot

added theorem GaloisConnection.l_comm_iff_u_comm

added theorem GaloisConnection.l_comm_of_u_comm

added theorem GaloisConnection.l_eq

added theorem GaloisConnection.l_eq_bot

added theorem GaloisConnection.l_le

added theorem GaloisConnection.l_u_bot

added theorem GaloisConnection.l_u_l_eq_l'

added theorem GaloisConnection.l_u_l_eq_l

added theorem GaloisConnection.l_u_le

added theorem GaloisConnection.l_u_le_trans

added theorem GaloisConnection.l_unique

added theorem GaloisConnection.le_iff_le

added theorem GaloisConnection.le_u

added theorem GaloisConnection.le_u_l

added theorem GaloisConnection.le_u_l_trans

added def GaloisConnection.liftOrderBot

added def GaloisConnection.liftOrderTop

added theorem GaloisConnection.lt_iff_lt

added theorem GaloisConnection.monotone_intro

added theorem GaloisConnection.monotone_l

added theorem GaloisConnection.monotone_u

added def GaloisConnection.toGaloisCoinsertion

added def GaloisConnection.toGaloisInsertion

added theorem GaloisConnection.u_comm_of_l_comm

added theorem GaloisConnection.u_eq

added theorem GaloisConnection.u_eq_top

added theorem GaloisConnection.u_l_top

added theorem GaloisConnection.u_l_u_eq_u'

added theorem GaloisConnection.u_l_u_eq_u

added theorem GaloisConnection.u_top

added theorem GaloisConnection.u_unique

added def GaloisConnection

added def GaloisInsertion.dual

added theorem GaloisInsertion.l_surjective

added theorem GaloisInsertion.l_top

added theorem GaloisInsertion.l_u_eq

added theorem GaloisInsertion.leftInverse_l_u

added def GaloisInsertion.monotoneIntro

added def GaloisInsertion.ofDual

added theorem GaloisInsertion.strictMono_u

added theorem GaloisInsertion.u_injective

added theorem GaloisInsertion.u_le_u_iff

added structure GaloisInsertion

added theorem OrderIso.to_galoisConnection

Modified Mathlib/Order/Heyting/Regular.lean

Modified Mathlib/Order/Hom/Order.lean

Modified Mathlib/Order/ModularLattice.lean

Modified Mathlib/Order/Rel/GaloisConnection.lean