<commit_before>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>

# Preorder homomorphisms

Bundled monotone functions, `x ≤ y → f x ≤ f y`.
-/
import logic.function.iterate
import order.basic
import order.bounded_lattice
import order.complete_lattice
import tactic.monotonicity

/-! # Category of preorders -/

/-- Bundled monotone (aka, increasing) function -/
structure preorder_hom (α β : Type*) [preorder α] [preorder β] :=
(to_fun   : α → β)
(monotone' : monotone to_fun)

infixr ` →ₘ `:25 := preorder_hom

namespace preorder_hom
variables {α : Type*} {β : Type*} {γ : Type*} [preorder α] [preorder β] [preorder γ]

instance : has_coe_to_fun (preorder_hom α β) :=
{ F := λ f, α → β,
  coe := preorder_hom.to_fun }

initialize_simps_projections preorder_hom (to_fun → coe)

@[mono]
lemma monotone (f : α →ₘ β) : monotone f :=
preorder_hom.monotone' f

@[simp] lemma to_fun_eq_coe {f : α →ₘ β} : f.to_fun = f := rfl
@[simp] lemma coe_fun_mk {f : α → β} (hf : _root_.monotone f) : (mk f hf : α → β) = f := rfl

@[ext] -- See library note [partially-applied ext lemmas]
lemma ext (f g : preorder_hom α β) (h : (f : α → β) = g) : f = g :=
by { cases f, cases g, congr, exact h }

/-- The identity function as bundled monotone function. -/
@[simps {fully_applied := ff}]
def id : preorder_hom α α :=
⟨id, monotone_id⟩

instance : inhabited (preorder_hom α α) := ⟨id⟩

/-- The composition of two bundled monotone functions. -/
@[simps {fully_applied := ff}]
def comp (g : preorder_hom β γ) (f : preorder_hom α β) : preorder_hom α γ :=
⟨g ∘ f, g.monotone.comp f.monotone⟩

@[simp] lemma comp_id (f : preorder_hom α β) : f.comp id = f :=
by { ext, refl }

@[simp] lemma id_comp (f : preorder_hom α β) : id.comp f = f :=
by { ext, refl }

/-- `subtype.val` as a bundled monotone function.  -/
@[simps {fully_applied := ff}]
def subtype.val (p : α → Prop) : subtype p →ₘ α :=
⟨subtype.val, λ x y h, h⟩

/-- The preorder structure of `α →ₘ β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
instance : preorder (α →ₘ β) :=
preorder.lift preorder_hom.to_fun

instance {β : Type*} [partial_order β] : partial_order (α →ₘ β) :=
partial_order.lift preorder_hom.to_fun $ by rintro ⟨⟩ ⟨⟩ h; congr; exact h

@[simps]
instance {β : Type*} [semilattice_sup β] : has_sup (α →ₘ β) :=
{ sup := λ f g, ⟨λ a, f a ⊔ g a, λ x y h, sup_le_sup (f.monotone h) (g.monotone h)⟩ }

instance {β : Type*} [semilattice_sup β] : semilattice_sup (α →ₘ β) :=
{ sup := has_sup.sup,
  le_sup_left := λ a b x, le_sup_left,
  le_sup_right := λ a b x, le_sup_right,
  sup_le := λ a b c h₀ h₁ x, sup_le (h₀ x) (h₁ x),
  .. (_ : partial_order (α →ₘ β)) }

@[simps]
instance {β : Type*} [semilattice_inf β] : has_inf (α →ₘ β) :=
{ inf := λ f g, ⟨λ a, f a ⊓ g a, λ x y h, inf_le_inf (f.monotone h) (g.monotone h)⟩ }

instance {β : Type*} [semilattice_inf β] : semilattice_inf (α →ₘ β) :=
{ inf := (⊓),
  inf_le_left := λ a b x, inf_le_left,
  inf_le_right := λ a b x, inf_le_right,
  le_inf := λ a b c h₀ h₁ x, le_inf (h₀ x) (h₁ x),
  .. (_ : partial_order (α →ₘ β)) }
<commit_msg>feat(order/preorder_hom): preorder_hom_eq_id (#8135)<commit_after>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>

# Preorder homomorphisms

Bundled monotone functions, `x ≤ y → f x ≤ f y`.
-/
import logic.function.iterate
import order.basic
import order.bounded_lattice
import order.complete_lattice
import tactic.monotonicity

/-! # Category of preorders -/

/-- Bundled monotone (aka, increasing) function -/
structure preorder_hom (α β : Type*) [preorder α] [preorder β] :=
(to_fun   : α → β)
(monotone' : monotone to_fun)

infixr ` →ₘ `:25 := preorder_hom

namespace preorder_hom
variables {α : Type*} {β : Type*} {γ : Type*} [preorder α] [preorder β] [preorder γ]

instance : has_coe_to_fun (preorder_hom α β) :=
{ F := λ f, α → β,
  coe := preorder_hom.to_fun }

initialize_simps_projections preorder_hom (to_fun → coe)

@[mono]
lemma monotone (f : α →ₘ β) : monotone f :=
preorder_hom.monotone' f

@[simp] lemma to_fun_eq_coe {f : α →ₘ β} : f.to_fun = f := rfl
@[simp] lemma coe_fun_mk {f : α → β} (hf : _root_.monotone f) : (mk f hf : α → β) = f := rfl

@[ext] -- See library note [partially-applied ext lemmas]
lemma ext (f g : preorder_hom α β) (h : (f : α → β) = g) : f = g :=
by { cases f, cases g, congr, exact h }

/-- The identity function as bundled monotone function. -/
@[simps {fully_applied := ff}]
def id : preorder_hom α α :=
⟨id, monotone_id⟩

instance : inhabited (preorder_hom α α) := ⟨id⟩

/-- The composition of two bundled monotone functions. -/
@[simps {fully_applied := ff}]
def comp (g : preorder_hom β γ) (f : preorder_hom α β) : preorder_hom α γ :=
⟨g ∘ f, g.monotone.comp f.monotone⟩

@[simp] lemma comp_id (f : preorder_hom α β) : f.comp id = f :=
by { ext, refl }

@[simp] lemma id_comp (f : preorder_hom α β) : id.comp f = f :=
by { ext, refl }

/-- `subtype.val` as a bundled monotone function.  -/
@[simps {fully_applied := ff}]
def subtype.val (p : α → Prop) : subtype p →ₘ α :=
⟨subtype.val, λ x y h, h⟩

-- TODO[gh-6025]: make this a global instance once safe to do so
/-- There is a unique monotone map from a subsingleton to itself. -/
local attribute [instance]
def unique [subsingleton α] : unique (α →ₘ α) :=
{ default := preorder_hom.id, uniq := λ a, ext _ _ (subsingleton.elim _ _) }

lemma preorder_hom_eq_id [subsingleton α] (g : α →ₘ α) : g = preorder_hom.id :=
subsingleton.elim _ _

/-- The preorder structure of `α →ₘ β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
instance : preorder (α →ₘ β) :=
preorder.lift preorder_hom.to_fun

instance {β : Type*} [partial_order β] : partial_order (α →ₘ β) :=
partial_order.lift preorder_hom.to_fun $ by rintro ⟨⟩ ⟨⟩ h; congr; exact h

@[simps]
instance {β : Type*} [semilattice_sup β] : has_sup (α →ₘ β) :=
{ sup := λ f g, ⟨λ a, f a ⊔ g a, λ x y h, sup_le_sup (f.monotone h) (g.monotone h)⟩ }

instance {β : Type*} [semilattice_sup β] : semilattice_sup (α →ₘ β) :=
{ sup := has_sup.sup,
  le_sup_left := λ a b x, le_sup_left,
  le_sup_right := λ a b x, le_sup_right,
  sup_le := λ a b c h₀ h₁ x, sup_le (h₀ x) (h₁ x),
  .. (_ : partial_order (α →ₘ β)) }

@[simps]
instance {β : Type*} [semilattice_inf β] : has_inf (α →ₘ β) :=
{ inf := λ f g, ⟨λ a, f a ⊓ g a, λ x y h, inf_le_inf (f.monotone h) (g.monotone h)⟩ }

instance {β : Type*} [semilattice_inf β] : semilattice_inf (α →ₘ β) :=
{ inf := (⊓),
  inf_le_left := λ a b x, inf_le_left,
  inf_le_right := λ a b x, inf_le_right,
  le_inf := λ a b c h₀ h₁ x, le_inf (h₀ x) (h₁ x),
  .. (_ : partial_order (α →ₘ β)) }

{'fraction_non_alphanumeric': 0.15325956937799043, 'fraction_numerical': 0.0035885167464114833, 'mean_word_length': 3.4623082054703134, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7121184', 'n_tokens_mistral': 3066, 'n_tokens_neox': 2819, 'n_words': 981}