Skip to content

Commit

Permalink
feat(data/sum/interval): The lexicographic sum of two locally finite …
Browse files Browse the repository at this point in the history
…orders is locally finite (#11352)

This proves `locally_finite_order (α ⊕ₗ β)` where `α` and `β` are locally finite themselves.
  • Loading branch information
YaelDillies committed Aug 2, 2023
1 parent 3ba1516 commit 48a058d
Show file tree
Hide file tree
Showing 2 changed files with 185 additions and 5 deletions.
2 changes: 2 additions & 0 deletions src/data/finset/sum.lean
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@ multiset.mem_disj_sum
@[simp] lemma inl_mem_disj_sum : inl a ∈ s.disj_sum t ↔ a ∈ s := inl_mem_disj_sum
@[simp] lemma inr_mem_disj_sum : inr b ∈ s.disj_sum t ↔ b ∈ t := inr_mem_disj_sum

@[simp] lemma disj_sum_eq_empty : s.disj_sum t = ∅ ↔ s = ∅ ∧ t = ∅ := by simp [ext_iff]

lemma disj_sum_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁.disj_sum t₁ ⊆ s₂.disj_sum t₂ :=
val_le_iff.1 $ disj_sum_mono (val_le_iff.2 hs) (val_le_iff.2 ht)

Expand Down
188 changes: 183 additions & 5 deletions src/data/sum/interval.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import data.finset.sum
import data.sum.order
import order.locally_finite

Expand All @@ -12,11 +13,8 @@ import order.locally_finite
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
This file provides the `locally_finite_order` instance for the disjoint sum of two orders.
## TODO
Do the same for the lexicographic sum of orders.
This file provides the `locally_finite_order` instance for the disjoint sum and linear sum of two
orders and calculates the cardinality of their finite intervals.
-/

open function sum
Expand Down Expand Up @@ -99,6 +97,106 @@ lemma sum_lift₂_mono (h₁ : ∀ a b, f₁ a b ⊆ g₁ a b) (h₂ : ∀ a b,
| (inr a) (inr b) := map_subset_map.2 (h₂ _ _)

end sum_lift₂

section sum_lex_lift
variables (f₁ f₁' : α₁ → β₁ → finset γ₁) (f₂ f₂' : α₂ → β₂ → finset γ₂)
(g₁ g₁' : α₁ → β₂ → finset γ₁) (g₂ g₂' : α₁ → β₂ → finset γ₂)

/-- Lifts maps `α₁ → β₁ → finset γ₁`, `α₂ → β₂ → finset γ₂`, `α₁ → β₂ → finset γ₁`,
`α₂ → β₂ → finset γ₂` to a map `α₁ ⊕ α₂ → β₁ ⊕ β₂ → finset (γ₁ ⊕ γ₂)`. Could be generalized to
alternative monads if we can make sure to keep computability and universe polymorphism. -/
def sum_lex_lift : Π (a : α₁ ⊕ α₂) (b : β₁ ⊕ β₂), finset (γ₁ ⊕ γ₂)
| (inl a) (inl b) := (f₁ a b).map embedding.inl
| (inl a) (inr b) := (g₁ a b).disj_sum (g₂ a b)
| (inr a) (inl b) := ∅
| (inr a) (inr b) := (f₂ a b).map ⟨_, inr_injective⟩

@[simp] lemma sum_lex_lift_inl_inl (a : α₁) (b : β₁) :
sum_lex_lift f₁ f₂ g₁ g₂ (inl a) (inl b) = (f₁ a b).map embedding.inl := rfl

@[simp] lemma sum_lex_lift_inl_inr (a : α₁) (b : β₂) :
sum_lex_lift f₁ f₂ g₁ g₂ (inl a) (inr b) = (g₁ a b).disj_sum (g₂ a b) := rfl

@[simp] lemma sum_lex_lift_inr_inl (a : α₂) (b : β₁) :
sum_lex_lift f₁ f₂ g₁ g₂ (inr a) (inl b) = ∅ := rfl

@[simp] lemma sum_lex_lift_inr_inr (a : α₂) (b : β₂) :
sum_lex_lift f₁ f₂ g₁ g₂ (inr a) (inr b) = (f₂ a b).map ⟨_, inr_injective⟩ := rfl

variables {f₁ g₁ f₂ g₂ f₁' g₁' f₂' g₂'} {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c : γ₁ ⊕ γ₂}

lemma mem_sum_lex_lift :
c ∈ sum_lex_lift f₁ f₂ g₁ g₂ a b ↔
(∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
(∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
(∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂ :=
begin
split,
{ cases a; cases b,
{ rw [sum_lex_lift, mem_map],
rintro ⟨c, hc, rfl⟩,
exact or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩ },
{ refine λ h, (mem_disj_sum.1 h).elim _ _,
{ rintro ⟨c, hc, rfl⟩,
refine or.inr (or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩) },
{ rintro ⟨c, hc, rfl⟩,
refine or.inr (or.inr $ or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩) } },
{ refine λ h, (not_mem_empty _ h).elim },
{ rw [sum_lex_lift, mem_map],
rintro ⟨c, hc, rfl⟩,
exact or.inr (or.inr $ or.inr $ ⟨a, b, c, rfl, rfl, rfl, hc⟩) } },
{ rintro (⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩ |
⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩),
{ exact mem_map_of_mem _ hc },
{ exact inl_mem_disj_sum.2 hc },
{ exact inr_mem_disj_sum.2 hc },
{ exact mem_map_of_mem _ hc } }
end

lemma inl_mem_sum_lex_lift {c₁ : γ₁} :
inl c₁ ∈ sum_lex_lift f₁ f₂ g₁ g₂ a b ↔
(∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂ :=
by simp [mem_sum_lex_lift]

lemma inr_mem_sum_lex_lift {c₂ : γ₂} :
inr c₂ ∈ sum_lex_lift f₁ f₂ g₁ g₂ a b ↔
(∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂ :=
by simp [mem_sum_lex_lift]

lemma sum_lex_lift_mono (hf₁ : ∀ a b, f₁ a b ⊆ f₁' a b) (hf₂ : ∀ a b, f₂ a b ⊆ f₂' a b)
(hg₁ : ∀ a b, g₁ a b ⊆ g₁' a b) (hg₂ : ∀ a b, g₂ a b ⊆ g₂' a b) (a : α₁ ⊕ α₂) (b : β₁ ⊕ β₂) :
sum_lex_lift f₁ f₂ g₁ g₂ a b ⊆ sum_lex_lift f₁' f₂' g₁' g₂' a b :=
begin
cases a; cases b,
exacts [map_subset_map.2 (hf₁ _ _), disj_sum_mono (hg₁ _ _) (hg₂ _ _), subset.rfl,
map_subset_map.2 (hf₂ _ _)],
end

lemma sum_lex_lift_eq_empty :
(sum_lex_lift f₁ f₂ g₁ g₂ a b) = ∅ ↔ (∀ a₁ b₁, a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
(∀ a₁ b₂, a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
∀ a₂ b₂, a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅ :=
begin
refine ⟨λ h, ⟨_, _, _⟩, λ h, _⟩,
any_goals { rintro a b rfl rfl, exact map_eq_empty.1 h },
{ rintro a b rfl rfl, exact disj_sum_eq_empty.1 h },
cases a; cases b,
{ exact map_eq_empty.2 (h.1 _ _ rfl rfl) },
{ simp [h.2.1 _ _ rfl rfl] },
{ refl },
{ exact map_eq_empty.2 (h.2.2 _ _ rfl rfl) }
end

lemma sum_lex_lift_nonempty :
(sum_lex_lift f₁ f₂ g₁ g₂ a b).nonempty ↔ (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).nonempty)
∨ (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).nonempty ∨ (g₂ a₁ b₂).nonempty))
∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).nonempty :=
by simp [nonempty_iff_ne_empty, sum_lex_lift_eq_empty, not_and_distrib]

end sum_lex_lift
end finset

open finset function
Expand Down Expand Up @@ -141,4 +239,84 @@ lemma Ioc_inr_inr : Ioc (inr b₁ : α ⊕ β) (inr b₂) = (Ioc b₁ b₂).map
lemma Ioo_inr_inr : Ioo (inr b₁ : α ⊕ β) (inr b₂) = (Ioo b₁ b₂).map embedding.inr := rfl

end disjoint

/-! ### Lexicographical sum of orders -/

namespace lex
variables [preorder α] [preorder β] [order_top α] [order_bot β] [locally_finite_order α]
[locally_finite_order β]

/-- Throwaway tactic. -/
private meta def simp_lex : tactic unit :=
`[refine to_lex.surjective.forall₃.2 _, rintro (a | a) (b | b) (c | c); simp only
[sum_lex_lift_inl_inl, sum_lex_lift_inl_inr, sum_lex_lift_inr_inl, sum_lex_lift_inr_inr,
inl_le_inl_iff, inl_le_inr, not_inr_le_inl, inr_le_inr_iff, inl_lt_inl_iff, inl_lt_inr,
not_inr_lt_inl, inr_lt_inr_iff, mem_Icc, mem_Ico, mem_Ioc, mem_Ioo, mem_Ici, mem_Ioi, mem_Iic,
mem_Iio, equiv.coe_to_embedding, to_lex_inj, exists_false, and_false, false_and, map_empty,
not_mem_empty, true_and, inl_mem_disj_sum, inr_mem_disj_sum, and_true, of_lex_to_lex, mem_map,
embedding.coe_fn_mk, exists_prop, exists_eq_right, embedding.inl_apply]]

instance locally_finite_order : locally_finite_order (α ⊕ₗ β) :=
{ finset_Icc := λ a b,
(sum_lex_lift Icc Icc (λ a _, Ici a) (λ _, Iic) (of_lex a) (of_lex b)).map to_lex.to_embedding,
finset_Ico := λ a b,
(sum_lex_lift Ico Ico (λ a _, Ici a) (λ _, Iio) (of_lex a) (of_lex b)).map to_lex.to_embedding,
finset_Ioc := λ a b,
(sum_lex_lift Ioc Ioc (λ a _, Ioi a) (λ _, Iic) (of_lex a) (of_lex b)).map to_lex.to_embedding,
finset_Ioo := λ a b,
(sum_lex_lift Ioo Ioo (λ a _, Ioi a) (λ _, Iio) (of_lex a) (of_lex b)).map to_lex.to_embedding,
finset_mem_Icc := by simp_lex,
finset_mem_Ico := by simp_lex,
finset_mem_Ioc := by simp_lex,
finset_mem_Ioo := by simp_lex }

variables (a a₁ a₂ : α) (b b₁ b₂ : β)

lemma Icc_inl_inl :
Icc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Icc a₁ a₂).map (embedding.inl.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

lemma Ico_inl_inl :
Ico (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ico a₁ a₂).map (embedding.inl.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

lemma Ioc_inl_inl :
Ioc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ioc a₁ a₂).map (embedding.inl.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

lemma Ioo_inl_inl :
Ioo (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ioo a₁ a₂).map (embedding.inl.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

@[simp] lemma Icc_inl_inr :
Icc (inlₗ a) (inrₗ b) = ((Ici a).disj_sum (Iic b)).map to_lex.to_embedding := rfl
@[simp] lemma Ico_inl_inr :
Ico (inlₗ a) (inrₗ b) = ((Ici a).disj_sum (Iio b)).map to_lex.to_embedding := rfl
@[simp] lemma Ioc_inl_inr :
Ioc (inlₗ a) (inrₗ b) = ((Ioi a).disj_sum (Iic b)).map to_lex.to_embedding := rfl
@[simp] lemma Ioo_inl_inr :
Ioo (inlₗ a) (inrₗ b) = ((Ioi a).disj_sum (Iio b)).map to_lex.to_embedding := rfl

@[simp] lemma Icc_inr_inl : Icc (inrₗ b) (inlₗ a) = ∅ := rfl
@[simp] lemma Ico_inr_inl : Ico (inrₗ b) (inlₗ a) = ∅ := rfl
@[simp] lemma Ioc_inr_inl : Ioc (inrₗ b) (inlₗ a) = ∅ := rfl
@[simp] lemma Ioo_inr_inl : Ioo (inrₗ b) (inlₗ a) = ∅ := rfl

lemma Icc_inr_inr :
Icc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Icc b₁ b₂).map (embedding.inr.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

lemma Ico_inr_inr :
Ico (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ico b₁ b₂).map (embedding.inr.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

lemma Ioc_inr_inr :
Ioc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioc b₁ b₂).map (embedding.inr.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

lemma Ioo_inr_inr :
Ioo (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioo b₁ b₂).map (embedding.inr.trans to_lex.to_embedding) :=
by { rw ←finset.map_map, refl }

end lex
end sum

0 comments on commit 48a058d

Please sign in to comment.