feat(order/*): introduces complemented lattices (#5747)

Defines `is_complemented` on bounded lattices
Proves facts about complemented modular lattices
Provides two instances of `is_complemented` on submodule lattices



Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

Author: awainverse

src/linear_algebra/basis.lean

@@ -482,6 +482,9 @@ lemma submodule.exists_is_compl (p : submodule K V) : ∃ q : submodule K V, is_
 let ⟨f, hf⟩ := p.subtype.exists_left_inverse_of_injective p.ker_subtype in
 ⟨f.ker, linear_map.is_compl_of_proj $ linear_map.ext_iff.1 hf⟩
 
+instance vector_space.submodule.is_complemented : is_complemented (submodule K V) :=
+⟨submodule.exists_is_compl⟩
+
 lemma linear_map.exists_right_inverse_of_surjective (f : V →ₗ[K] V')
   (hf_surj : f.range = ⊤) : ∃g:V' →ₗ V, f.comp g = linear_map.id :=
 begin

src/order/atoms.lean

@@ -40,6 +40,9 @@ which are lattices with only two elements, and related ideas.
    of `is_atom` and `is_coatom`.
   * `is_simple_lattice_iff_is_atom_top` and `is_simple_lattice_iff_is_coatom_bot` express the
   connection between atoms, coatoms, and simple lattices
+  * `is_compl.is_atom_iff_is_coatom` and `is_compl.is_coatom_if_is_atom`: In a modular
+  bounded lattice, a complement of an atom is a coatom and vice versa.
+  * ``is_atomic_iff_is_coatomic`: A modular complemented lattice is atomic iff it is coatomic.
 
 -/
 
@@ -456,4 +459,26 @@ lemma is_coatom_iff_is_atom : is_coatom a ↔ is_atom b := hc.symm.is_atom_iff_i
 
 end is_compl
 
+variables [is_complemented α]
+
+lemma is_coatomic_of_is_atomic_of_is_complemented_of_is_modular [is_atomic α] : is_coatomic α :=
+⟨λ x, begin
+  rcases exists_is_compl x with ⟨y, xy⟩,
+  apply (eq_bot_or_exists_atom_le y).imp _ _,
+  { rintro rfl,
+    exact eq_top_of_is_compl_bot xy },
+  { rintro ⟨a, ha, ay⟩,
+    rcases exists_is_compl (xy.symm.Iic_order_iso_Ici ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩,
+    refine ⟨↑(⟨b, xb⟩ : set.Ici x), is_coatom.of_is_coatom_coe_Ici _, xb⟩,
+    rw [← hb.is_atom_iff_is_coatom, order_iso.is_atom_iff],
+    apply ha.Iic }
+end⟩
+
+lemma is_atomic_of_is_coatomic_of_is_complemented_of_is_modular [is_coatomic α] : is_atomic α :=
+is_coatomic_dual_iff_is_atomic.1 is_coatomic_of_is_atomic_of_is_complemented_of_is_modular
+
+theorem is_atomic_iff_is_coatomic : is_atomic α ↔ is_coatomic α :=
+⟨λ h, @is_coatomic_of_is_atomic_of_is_complemented_of_is_modular _ _ _ _ h,
+  λ h, @is_atomic_of_is_coatomic_of_is_complemented_of_is_modular _ _ _ _ h⟩
+
 end is_modular_lattice

src/order/boolean_algebra.lean

@@ -119,6 +119,13 @@ by rw [sdiff_eq, sdiff_eq]; from inf_le_inf h₁ (compl_le_compl h₂)
 @[simp] lemma sdiff_idem_right : x \ y \ y = x \ y :=
 by rw [sdiff_eq, sdiff_eq, inf_assoc, inf_idem]
 
+namespace boolean_algebra
+
+@[priority 100]
+instance : is_complemented α := ⟨λ x, ⟨xᶜ, is_compl_compl⟩⟩
+
+end boolean_algebra
+
 end boolean_algebra
 
 instance boolean_algebra_Prop : boolean_algebra Prop :=

src/order/bounded_lattice.lean

@@ -1089,6 +1089,39 @@ is_compl.of_eq bot_inf_eq sup_top_eq
 lemma is_compl_top_bot [bounded_lattice α] : is_compl (⊤ : α) ⊥ :=
 is_compl.of_eq inf_bot_eq top_sup_eq
 
+section
+variables [bounded_lattice α] {x : α}
+
+lemma eq_top_of_is_compl_bot (h : is_compl x ⊥) : x = ⊤ :=
+sup_bot_eq.symm.trans h.sup_eq_top
+
+lemma eq_top_of_bot_is_compl (h : is_compl ⊥ x) : x = ⊤ :=
+eq_top_of_is_compl_bot h.symm
+
+lemma eq_bot_of_is_compl_top (h : is_compl x ⊤) : x = ⊥ :=
+eq_top_of_is_compl_bot h.to_order_dual
+
+lemma eq_bot_of_top_is_compl (h : is_compl ⊤ x) : x = ⊥ :=
+eq_top_of_bot_is_compl h.to_order_dual
+
+end
+
+/-- A complemented bounded lattice is one where every element has a
+  (not necessarily unique) complement. -/
+class is_complemented (α) [bounded_lattice α] : Prop :=
+(exists_is_compl : ∀ (a : α), ∃ (b : α), is_compl a b)
+
+export is_complemented (exists_is_compl)
+
+namespace is_complemented
+variables [bounded_lattice α] [is_complemented α]
+
+instance : is_complemented (order_dual α) :=
+⟨λ a, ⟨classical.some (@exists_is_compl α _ _ a),
+  (classical.some_spec (@exists_is_compl α _ _ a)).to_order_dual⟩⟩
+
+end is_complemented
+
 end is_compl
 
 section nontrivial

src/order/modular_lattice.lean

@@ -107,4 +107,31 @@ instance is_modular_lattice_Iic : is_modular_lattice (set.Iic a) :=
 instance is_modular_lattice_Ici : is_modular_lattice (set.Ici a) :=
 ⟨λ x y z xz, (sup_inf_le_assoc_of_le (y : α) xz : (↑x ⊔ ↑y) ⊓ ↑z ≤ ↑x ⊔ ↑y ⊓ ↑z)⟩
 
+section is_complemented
+variables [is_complemented α]
+
+instance is_complemented_Iic : is_complemented (set.Iic a) :=
+⟨λ ⟨x, hx⟩, ⟨⟨(classical.some (exists_is_compl x)) ⊓ a, set.mem_Iic.2 inf_le_right⟩, begin
+    split,
+    { change x ⊓ (classical.some _ ⊓ a) ≤ ⊥, -- improve lattice subtype API
+      rw ← inf_assoc,
+      exact le_trans inf_le_left (classical.some_spec (exists_is_compl x)).1 },
+    { change a ≤ x ⊔ (classical.some _ ⊓ a), -- improve lattice subtype API
+      rw [← sup_inf_assoc_of_le _ (set.mem_Iic.1 hx),
+          top_le_iff.1 (classical.some_spec (exists_is_compl x)).2, top_inf_eq] }
+  end⟩⟩
+
+instance is_complemented_Ici : is_complemented (set.Ici a) :=
+⟨λ ⟨x, hx⟩, ⟨⟨(classical.some (exists_is_compl x)) ⊔ a, set.mem_Ici.2 le_sup_right⟩, begin
+    split,
+    { change x ⊓ (classical.some _ ⊔ a) ≤ a, -- improve lattice subtype API
+      rw [← inf_sup_assoc_of_le _ (set.mem_Ici.1 hx),
+          le_bot_iff.1 (classical.some_spec (exists_is_compl x)).1, bot_sup_eq] },
+    { change ⊤ ≤ x ⊔ (classical.some _ ⊔ a), -- improve lattice subtype API
+      rw ← sup_assoc,
+      exact le_trans (classical.some_spec (exists_is_compl x)).2 le_sup_left }
+  end⟩⟩
+
+end is_complemented
+
 end is_modular_lattice

src/representation_theory/maschke.lean

@@ -136,6 +136,8 @@ end
 end linear_map
 end
 
+namespace monoid_algebra
+
 -- Now we work over a `[field k]`, and replace the assumption `[invertible (fintype.card G : k)]`
 -- with `¬(ring_char k ∣ fintype.card G)`.
 variables {k : Type u} [field k] {G : Type u} [fintype G] [group G]
@@ -144,7 +146,7 @@ variables [is_scalar_tower k (monoid_algebra k G) V]
 variables {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W]
 variables [is_scalar_tower k (monoid_algebra k G) W]
 
-lemma monoid_algebra.exists_left_inverse_of_injective
+lemma exists_left_inverse_of_injective
   (not_dvd : ¬(ring_char k ∣ fintype.card G)) (f : V →ₗ[monoid_algebra k G] W) (hf : f.ker = ⊥) :
   ∃ (g : W →ₗ[monoid_algebra k G] V), g.comp f = linear_map.id :=
 begin
@@ -161,8 +163,16 @@ begin
   exact congr_fun this v
 end
 
-lemma monoid_algebra.submodule.exists_is_compl
+namespace submodule
+
+lemma exists_is_compl
   (not_dvd : ¬(ring_char k ∣ fintype.card G)) (p : submodule (monoid_algebra k G) V) :
   ∃ q : submodule (monoid_algebra k G) V, is_compl p q :=
 let ⟨f, hf⟩ := monoid_algebra.exists_left_inverse_of_injective not_dvd p.subtype p.ker_subtype in
 ⟨f.ker, linear_map.is_compl_of_proj $ linear_map.ext_iff.1 hf⟩
+
+theorem is_complemented (not_dvd : ¬(ring_char k ∣ fintype.card G)) :
+  is_complemented (submodule (monoid_algebra k G) V) := ⟨exists_is_compl not_dvd⟩
+
+end submodule
+end monoid_algebra