Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat (order/modular_lattice): modular_lattice as extension of lattice #7539

Closed
wants to merge 1 commit into from
Closed

feat (order/modular_lattice): modular_lattice as extension of lattice #7539

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
21 changes: 21 additions & 0 deletions src/order/modular_lattice.lean
View file
Open in desktop
Expand Up @@ -36,6 +36,9 @@ variable {α : Type*}
class is_modular_lattice α [lattice α] : Prop :=
(sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z))

class modular_lattice α extends lattice α :=
(modular_law: ∀ (x u v : α ), (x ≤ u) → u ⊓ (v ⊔ x) = (u ⊓ v) ⊔ x )
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this class is a good idea - it means you need a new class to talk about modular bounded lattices, modular complete lattices, ...

What was the reason you added it?


section is_modular_lattice
variables [lattice α] [is_modular_lattice α ]

Expand Down Expand Up @@ -78,6 +81,24 @@ def inf_Icc_order_iso_Icc_sup (a b : α) : set.Icc (a ⊓ b) a ≃o set.Icc b (a
end }
end is_modular_lattice

namespace modular_lattice

theorem diamond_isomorphism
[modular_lattice α] {u v w x y : α} :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of a new class, the existing one should work fine

Suggested change
[modular_lattice α] {u v w x y : α} :
[lattice α] [is_modular_lattice α] {u v w x y : α} :

(x ≤ u) → (x ≥ v) → (x ≥ u ⊓ v) → (x ≤ u ⊔ v) → u ⊓ (v ⊔ x) = x ∧ (x ⊓ u) ⊔ v = x :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mathlib almost never uses ≥:

Suggested change
(x ≤ u) → (x ≥ v) → (x ≥ u ⊓ v) → (x ≤ u ⊔ v) → u ⊓ (v ⊔ x) = x ∧ (x ⊓ u) ⊔ v = x :=
(x ≤ u) → (v ≤ x) → (u ⊓ v ≤ x) → (x ≤ u ⊔ v) → u ⊓ (v ⊔ x) = x ∧ (x ⊓ u) ⊔ v = x :=

begin
intros h1 h2 h3 h4,
split,
{ rw modular_lattice.modular_law,
exact sup_eq_right.mpr h3,
exact h1 },
Comment on lines +92 to +94
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This half of the proof only uses h1 and h3, while the other branch only uses h2 and h4. This suggests to me that this should be two different lemmas not a single lemma.

{ rw ← modular_lattice.modular_law,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
{ rw ← modular_lattice.modular_law,
{ rw ← inf_sup_assoc_of_le,

Or similar, with the changes I suggest above

exact inf_eq_left.mpr h4,
exact h2 }
end

end modular_lattice

namespace is_compl
variables [bounded_lattice α] [is_modular_lattice α]

Expand Down