feat(order/flag): Order isomorphisms act on flags

src/order/chain.lean

@@ -57,6 +57,8 @@ lemma set.subsingleton.is_chain (hs : s.subsingleton) : is_chain r s := hs.pairw
 
 lemma is_chain.mono : s ⊆ t → is_chain r t → is_chain r s := set.pairwise.mono
 
+lemma is_chain_singleton (r : α → α → Prop) (a : α) : is_chain r {a} := pairwise_singleton _ _
+
 lemma is_chain.mono_rel {r' : α → α → Prop} (h : is_chain r s)
   (h_imp : ∀ x y, r x y → r' x y) : is_chain r' s :=
 h.mono' $ λ x y, or.imp (h_imp x y) (h_imp y x)
@@ -71,6 +73,9 @@ lemma is_chain.insert (hs : is_chain r s) (ha : ∀ b ∈ s, a ≠ b → a ≺ b
   is_chain r (insert a s) :=
 hs.insert_of_symmetric (λ _ _, or.symm) ha
 
+lemma is_chain_pair (r : α → α → Prop) {a b : α} (h : r a b) : is_chain r {a, b} :=
+(is_chain_singleton _ _).insert $ λ _ hb _, or.inl $ (eq_of_mem_singleton hb).symm.rec_on ‹_›
+
 lemma is_chain_univ_iff : is_chain r (univ : set α) ↔ is_trichotomous α r :=
 begin
   refine ⟨λ h, ⟨λ a b , _⟩, λ h, @is_chain_of_trichotomous _ _ h univ⟩,
@@ -123,6 +128,15 @@ lemma is_max_chain.bot_mem [has_le α] [order_bot α] (h : is_max_chain (≤) s)
 lemma is_max_chain.top_mem [has_le α] [order_top α] (h : is_max_chain (≤) s) : ⊤ ∈ s :=
 (h.2 (h.1.insert $ λ a _ _, or.inr le_top) $ subset_insert _ _).symm ▸ mem_insert _ _
 
+lemma is_max_chain.image {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {c : set α}
+  (hc : is_max_chain r c) :
+  is_max_chain s (f '' c) :=
+⟨hc.is_chain.image _ _ _ $ λ _ _, f.map_rel_iff.2, λ t ht hf,
+  (f.to_equiv.eq_preimage_iff_image_eq _ _).1 begin
+    rw preimage_equiv_eq_image_symm,
+    exact hc.2 (ht.image _ _ _ $ λ _ _, f.symm.map_rel_iff.2) ((f.to_equiv.subset_image' _ _).2 hf),
+  end⟩
+
 open_locale classical
 
 /-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `succ_chain s`
@@ -260,7 +274,7 @@ structure flag (α : Type*) [has_le α] :=
 
 namespace flag
 section has_le
-variables [has_le α] {s t : flag α} {a : α}
+variables [has_le α] {s t : flag α} {c : set α} {a : α}
 
 instance : set_like (flag α) α :=
 { coe := carrier,
@@ -277,19 +291,39 @@ protected lemma max_chain (s : flag α) : is_max_chain (≤) (s : set α) := ⟨
 lemma top_mem [order_top α] (s : flag α) : (⊤ : α) ∈ s := s.max_chain.top_mem
 lemma bot_mem [order_bot α] (s : flag α) : (⊥ : α) ∈ s := s.max_chain.bot_mem
 
+/-- Reinterpret a maximal chain as a flag. -/
+protected def _root_.is_max_chain.flag (hc : is_max_chain (≤) c) : flag α := ⟨c, hc.is_chain, hc.2⟩
+
+@[simp, norm_cast] lemma _root_.is_max_chain.coe_flag (hc : is_max_chain (≤) c) : ↑hc.flag = c :=
+rfl
+
 end has_le
 
 section preorder
-variables [preorder α] {a b : α}
+variables [preorder α] [preorder β] {s : flag α} {a b : α}
 
 protected lemma le_or_le (s : flag α) (ha : a ∈ s) (hb : b ∈ s) : a ≤ b ∨ b ≤ a :=
 s.chain_le.total ha hb
 
+lemma mem_iff_forall_le_or_ge : a ∈ s ↔ ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a :=
+⟨λ ha b, s.le_or_le ha, λ hb, of_not_not $ λ ha, set.ne_insert_of_not_mem _ ‹_› $ s.max_chain.2
+  (s.chain_le.insert $ λ c hc _, hb hc) $ set.subset_insert _ _⟩
+
 instance [order_top α] (s : flag α) : order_top s := subtype.order_top s.top_mem
 instance [order_bot α] (s : flag α) : order_bot s := subtype.order_bot s.bot_mem
 instance [bounded_order α] (s : flag α) : bounded_order s :=
 subtype.bounded_order s.bot_mem s.top_mem
 
+/-- Flags are preserved under order isomorphisms. -/
+def map (e : α ≃o β) : flag α ≃ flag β :=
+{ to_fun := λ s, (s.max_chain.image e).flag,
+  inv_fun := λ s, (s.max_chain.image e.symm).flag,
+  left_inv := λ s, ext $ e.symm_image_image s,
+  right_inv := λ s, ext $ e.image_symm_image s }
+
+@[simp, norm_cast] lemma coe_map (e : α ≃o β) (s : flag α) : ↑(map e s) = e '' s := rfl
+@[simp] lemma symm_map (e : α ≃o β) : (map e).symm = map e.symm := rfl
+
 end preorder
 
 section partial_order

src/order/flag.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.set.pointwise.smul
+import order.chain
+import order.grade
+import order.rel_iso.group
+
+/-!
+# Additional constructions about flags
+
+This file defines the action of order isomorphisms on flags and grades the elements of a flag.
+
+## TODO
+
+The file structure doesn't seem optimal. Maybe all the `flag` material could move here, or to a
+subfolder?
+-/
+
+open_locale pointwise
+
+variables {𝕆 α : Type*}
+
+namespace flag
+
+/-!
+### Action on flags
+
+Order isomorphisms act on flags.
+-/
+
+section preorder
+variables [preorder α]
+
+instance : has_smul (α ≃o α) (flag α) := ⟨λ e, map e⟩
+
+@[simp, norm_cast] lemma coe_smul (e : α ≃o α) (s : flag α) : (↑(e • s) : set α) = e • s := rfl
+
+instance : mul_action (α ≃o α) (flag α) := set_like.coe_injective.mul_action _ coe_smul
+
+end preorder
+
+/-!
+### Grading a flag
+
+A flag inherits the grading of its ambient order.
+-/
+
+section partial_order
+variables [partial_order α] {s : flag α}
+
+@[simp] lemma coe_covby_coe {a b : s} : (a : α) ⋖ b ↔ a ⋖ b :=
+begin
+  refine and_congr_right' ⟨λ h c hac, h hac, λ h c hac hcb,
+    @h ⟨c, mem_iff_forall_le_or_ge.2 $ λ d hd, _⟩ hac hcb⟩,
+  classical,
+  obtain hda | had := le_or_lt (⟨d, hd⟩ : s) a,
+  { exact or.inr ((subtype.coe_le_coe.2 hda).trans hac.le) },
+  obtain hbd | hdb := le_or_lt b ⟨d, hd⟩,
+  { exact or.inl (hcb.le.trans hbd) },
+  { cases h had hdb }
+end
+
+@[simp] lemma is_max_coe {a : s} : is_max (a : α) ↔ is_max a :=
+⟨λ h b hab, h hab, λ h b hab, @h ⟨b, mem_iff_forall_le_or_ge.2 $ λ c hc,
+  by { classical, exact or.inr (hab.trans' $ h.is_top ⟨c, hc⟩) }⟩ hab⟩
+
+@[simp] lemma is_min_coe {a : s} : is_min (a : α) ↔ is_min a :=
+⟨λ h b hba, h hba, λ h b hba, @h ⟨b, mem_iff_forall_le_or_ge.2 $ λ c hc,
+  by { classical, exact or.inl (hba.trans $ h.is_bot ⟨c, hc⟩) }⟩ hba⟩
+
+variables [preorder 𝕆]
+
+instance [grade_order 𝕆 α] (s : flag α) : grade_order 𝕆 s :=
+grade_order.lift_right coe (subtype.strict_mono_coe _) $ λ _ _, coe_covby_coe.2
+
+instance [grade_min_order 𝕆 α] (s : flag α) : grade_min_order 𝕆 s :=
+grade_min_order.lift_right coe (subtype.strict_mono_coe _) (λ _ _, coe_covby_coe.2) $
+  λ _, is_min_coe.2
+
+instance [grade_max_order 𝕆 α] (s : flag α) : grade_max_order 𝕆 s :=
+grade_max_order.lift_right coe (subtype.strict_mono_coe _) (λ _ _, coe_covby_coe.2) $
+  λ _, is_max_coe.2
+
+instance [grade_bounded_order 𝕆 α] (s : flag α) : grade_bounded_order 𝕆 s :=
+grade_bounded_order.lift_right coe (subtype.strict_mono_coe _) (λ _ _, coe_covby_coe.2)
+  (λ _, is_min_coe.2) (λ _, is_max_coe.2)
+
+@[simp, norm_cast] lemma grade_coe [grade_order 𝕆 α] (a : s) : grade 𝕆 (a : α) = grade 𝕆 a := rfl
+
+end partial_order
+end flag

src/order/rel_iso/group.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import algebra.group.defs
+import group_theory.group_action.defs
 import order.rel_iso.basic
 
 /-!
@@ -37,4 +37,14 @@ lemma mul_apply (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x
 
 @[simp] lemma apply_inv_self (e : r ≃r r) (x) : e (e⁻¹ x) = x := e.apply_symm_apply x
 
+/-- The tautological action by `r ≃r r` on `α`. -/
+instance apply_mul_action : mul_action (r ≃r r) α :=
+{ smul := coe_fn,
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] lemma smul_def (f : r ≃r r) (a : α) : f • a = f a := rfl
+
+instance apply_has_faithful_smul : has_faithful_smul (r ≃r r) α := ⟨rel_iso.ext⟩
+
 end rel_iso

src/order/zorn.lean

@@ -202,3 +202,21 @@ begin
   { exact (hcs₀ hsz).right (h hysy) hzsz hyz },
   { exact (hcs₀ hsy).right hysy (h hzsz) hyz }
 end
+
+/-! ### Flags -/
+
+namespace flag
+variables [preorder α] {s : flag α} {a b : α}
+
+lemma _root_.is_chain.exists_subset_flag (hc : is_chain (≤) c) : ∃ s : flag α, c ⊆ s :=
+let ⟨s, hs, hcs⟩ := hc.exists_max_chain in ⟨hs.flag, hcs⟩
+
+lemma exists_mem (a : α) : ∃ s : flag α, a ∈ s :=
+let ⟨s, hs⟩ := set.subsingleton_singleton.is_chain.exists_subset_flag in ⟨s, hs rfl⟩
+
+lemma exists_mem_mem (hab : a ≤ b) : ∃ s : flag α, a ∈ s ∧ b ∈ s :=
+by simpa [set.insert_subset] using (is_chain_pair _ hab).exists_subset_flag
+
+instance : nonempty (flag α) := ⟨max_chain_spec.flag⟩
+
+end flag