text:
import control.traversable.instances

open set

structure filter (α : Type*) :=
(sets                   : set (set α))
(univ_sets              : set.univ ∈ sets)
(sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets)
(inter_sets {x y}       : x ∈ sets → y ∈ sets → x ∩ y ∈ sets)

structure is_filter {α : Type*} (sets : set (set α)):=
(univ_sets              : set.univ ∈ sets)
(sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets)
(inter_sets {x y}       : x ∈ sets → y ∈ sets → x ∩ y ∈ sets)

def principal {α : Type*} (s : set α) : filter α :=
{ sets             := {t | s ⊆ t},
  univ_sets        := subset_univ s,
  sets_of_superset := λ x y hx, subset.trans hx,
  inter_sets       := λ x y, subset_inter }

instance {α : Type*}: has_mem (set α) (filter α) := ⟨λ U F, U ∈ F.sets⟩

variables {α : Type} {f g : filter α} {s t : set α}

lemma filter_eq : ∀ {f g : filter α}, f.sets = g.sets → f = g
| ⟨a, _, _, _⟩ ⟨._, _, _, _⟩ rfl := rfl

instance : partial_order (filter α) :=
{ le            := λ f g, ∀ ⦃U : set α⦄, U ∈ g → U ∈ f,
  le_antisymm   := λ a b h₁ h₂, filter_eq $ subset.antisymm h₂ h₁,
  le_refl       := λ a, subset.rfl,
  le_trans      := λ a b c h₁ h₂, subset.trans h₂ h₁ }

theorem le_def {f g : filter α} : f ≤ g ↔ ∀ x ∈ g, x ∈ f := iff.rfl

author: mmasdeu

repo: topologygame

save_path: github-repos/lean/mmasdeu-topologygame


text:
/-
Copyright (c) 2022 Violeta Hernández Palacios. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Violeta Hernández Palacios

! This file was ported from Lean 3 source module set_theory.ordinal.topology
! leanprover-community/mathlib commit 23aa88e32dcc9d2a24cca7bc23268567ed4cd7d6
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.SetTheory.Ordinal.Arithmetic
import Mathbin.Topology.Order.Basic

/-!
### Topology of ordinals

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

We prove some miscellaneous results involving the order topology of ordinals.

### Main results

* `ordinal.is_closed_iff_sup` / `ordinal.is_closed_iff_bsup`: A set of ordinals is closed iff it's
  closed under suprema.
* `ordinal.is_normal_iff_strict_mono_and_continuous`: A characterization of normal ordinal
  functions.
* `ordinal.enum_ord_is_normal_iff_is_closed`: The function enumerating the ordinals of a set is
  normal iff the set is closed.
-/

noncomputable section

universe u v

open Cardinal Order

namespace Ordinal

variable {s : Set Ordinal.{u}} {a : Ordinal.{u}}

instance : TopologicalSpace Ordinal.{u} :=
  Preorder.topology Ordinal.{u}

instance : OrderTopology Ordinal.{u} :=
  ⟨rfl⟩

#print Ordinal.isOpen_singleton_iff /-
theorem isOpen_singleton_iff : IsOpen ({a} : Set Ordinal) ↔ ¬IsLimit a :=
  by
  refine' ⟨fun h ha => _, fun ha => _⟩
  · obtain ⟨b, c, hbc, hbc'⟩ :=
      (mem_nhds_iff_exists_Ioo_subset' ⟨0, Ordinal.pos_iff_ne_zero.2 ha.1⟩ ⟨_, lt_succ a⟩).1
        (h.mem_nhds rfl)
    have hba := ha.2 b hbc.1
    exact hba.ne (hbc' ⟨lt_succ b, hba.trans hbc.2⟩)
  · rcases zero_or_succ_or_limit a with (rfl | ⟨b, hb⟩ | ha')
    · convert isOpen_gt' (1 : Ordinal)
      ext
      exact ordinal.lt_one_iff_zero.symm
    · convert@isOpen_Ioo _ _ _ _ b (a + 1)
      ext c
      refine' ⟨fun hc => _, _⟩
      · rw [Set.mem_singleton_iff.1 hc]
        refine' ⟨_, lt_succ a⟩
        rw [hb]
        exact lt_succ b
      · rintro ⟨hc, hc'⟩
        apply le_antisymm (le_of_lt_succ hc')
        rw [hb]
        exact succ_le_of_lt hc
    · exact (ha ha').elim
#align ordinal.is_open_singleton_iff Ordinal.isOpen_singleton_iff
-/

/- warning: ordinal.is_open_iff -> Ordinal.isOpen_iff is a dubious translation:
lean 3 declaration is
  forall {s : Set.{succ u1} Ordinal.{u1}}, Iff (IsOpen.{succ u1} Ordinal.{u1} Ordinal.topologicalSpace.{u1} s) (forall (o : Ordinal.{u1}), (Membership.Mem.{succ u1, succ u1} Ordinal.{u1} (Set.{succ u1} Ordinal.{u1}) (Set.hasMem.{succ u1} Ordinal.{u1}) o s) -> (Ordinal.IsLimit.{u1} o) -> (Exists.{succ (succ u1)} Ordinal.{u1} (fun (a : Ordinal.{u1}) => Exists.{0} (LT.lt.{succ u1} Ordinal.{u1} (Preorder.toLT.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1})) a o) (fun (H : LT.lt.{succ u1} Ordinal.{u1} (Preorder.toLT.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1})) a o) => HasSubset.Subset.{succ u1} (Set.{succ u1} Ordinal.{u1}) (Set.hasSubset.{succ u1} Ordinal.{u1}) (Set.Ioo.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1}) a o) s))))
but is expected to have type
  forall {s : Set.{succ u1} Ordinal.{u1}}, Iff (IsOpen.{succ u1} Ordinal.{u1} Ordinal.instTopologicalSpaceOrdinal.{u1} s) (forall (o : Ordinal.{u1}), (Membership.mem.{succ u1, succ u1} Ordinal.{u1} (Set.{succ u1} Ordinal.{u1}) (Set.instMembershipSet.{succ u1} Ordinal.{u1}) o s) -> (Ordinal.IsLimit.{u1} o) -> (Exists.{succ (succ u1)} Ordinal.{u1} (fun (a : Ordinal.{u1}) => And (LT.lt.{succ u1} Ordinal.{u1} (Preorder.toLT.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1})) a o) (HasSubset.Subset.{succ u1} (Set.{succ u1} Ordinal.{u1}) (Set.instHasSubsetSet.{succ u1} Ordinal.{u1}) (Set.Ioo.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1}) a o) s))))
Case conversion may be inaccurate. Consider using '#align ordinal.is_open_iff Ordinal.isOpen_iffₓ'. -/
theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsLimit o → ∃ a < o, Set.Ioo a o ⊆ s := by
  classical
    refine' ⟨_, fun h => _⟩
    · rw [isOpen_iff_generate_intervals]
      intro h o hos ho
      have ho₀ := Ordinal.pos_iff_ne_zero.2 ho.1
      induction' h with t ht t u ht hu ht' hu' t ht H
      · rcases ht with ⟨a, rfl | rfl⟩
        · exact ⟨a, hos, fun b hb => hb.1⟩
        · exact ⟨0, ho₀, fun b hb => hb.2.trans hos⟩
      · exact ⟨0, ho₀, fun b _ => Set.mem_univ b⟩
      · rcases ht' hos.1 with ⟨a, ha, ha'⟩
        rcases hu' hos.2 with ⟨b, hb, hb'⟩
        exact
          ⟨_, max_lt ha hb, fun c hc =>
            ⟨ha' ⟨(le_max_left a b).trans_lt hc.1, hc.2⟩,
              hb' ⟨(le_max_right a b).trans_lt hc.1, hc.2⟩⟩⟩
      · rcases hos with ⟨u, hu, hu'⟩
        rcases H u hu hu' with ⟨a, ha, ha'⟩
        exact ⟨a, ha, fun b hb => ⟨u, hu, ha' hb⟩⟩
    · let f : s → Set Ordinal := fun o =>
        if ho : is_limit o.val then Set.Ioo (Classical.choose (h o.val o.Prop ho)) (o + 1)
        else {o.val}
      have : ∀ a, IsOpen (f a) := fun a =>
        by
        change IsOpen (dite _ _ _)
        split_ifs
        · exact isOpen_Ioo
        · rwa [is_open_singleton_iff]
      convert isOpen_unionᵢ this
      ext o
      refine' ⟨fun ho => Set.mem_unionᵢ.2 ⟨⟨o, ho⟩, _⟩, _⟩
      · split_ifs with ho'
        · refine' ⟨_, lt_succ o⟩
          cases' Classical.choose_spec (h o ho ho') with H
          exact H
        · exact Set.mem_singleton o
      · rintro ⟨t, ⟨a, ht⟩, hoa⟩
        change dite _ _ _ = t at ht
        split_ifs  at ht with ha <;> subst ht
        · cases' Classical.choose_spec (h a.val a.prop ha) with H has
          rcases lt_or_eq_of_le (le_of_lt_succ hoa.2) with (hoa' | rfl)
          · exact has ⟨hoa.1, hoa'⟩
          · exact a.prop
        · convert a.prop
#align ordinal.is_open_iff Ordinal.isOpen_iff

#print Ordinal.mem_closure_iff_sup /-
theorem mem_closure_iff_sup :
    a ∈ closure s ↔
      ∃ (ι : Type u)(_ : Nonempty ι)(f : ι → Ordinal), (∀ i, f i ∈ s) ∧ sup.{u, u} f = a :=
  by
  refine' mem_closure_iff.trans ⟨fun h => _, _⟩
  · by_cases has : a ∈ s
    · exact ⟨PUnit, by infer_instance, fun _ => a, fun _ => has, sup_const a⟩
    · have H := fun b (hba : b < a) => h _ (@isOpen_Ioo _ _ _ _ b (a + 1)) ⟨hba, lt_succ a⟩
      let f : a.out.α → Ordinal := fun i =>
        Classical.choose (H (typein (· < ·) i) (typein_lt_self i))
      have hf : ∀ i, f i ∈ Set.Ioo (typein (· < ·) i) (a + 1) ∩ s := fun i =>
        Classical.choose_spec (H _ _)
      rcases eq_zero_or_pos a with (rfl | ha₀)
      · rcases h _ (is_open_singleton_iff.2 not_zero_is_limit) rfl with ⟨b, hb, hb'⟩
        rw [Set.mem_singleton_iff.1 hb] at *
        exact (has hb').elim
      refine'
        ⟨_, out_nonempty_iff_ne_zero.2 (Ordinal.pos_iff_ne_zero.1 ha₀), f, fun i => (hf i).2,
          le_antisymm (sup_le fun i => le_of_lt_succ (hf i).1.2) _⟩
      by_contra' h
      cases' H _ h with b hb
      rcases eq_or_lt_of_le (le_of_lt_succ hb.1.2) with (rfl | hba)
      · exact has hb.2
      · have : b < f (enum (· < ·) b (by rwa [type_lt])) :=
          by
          have := (hf (enum (· < ·) b (by rwa [type_lt]))).1.1
          rwa [typein_enum] at this
        have : b ≤ sup.{u, u} f := this.le.trans (le_sup f _)
        exact this.not_lt hb.1.1
  · rintro ⟨ι, ⟨i⟩, f, hf, rfl⟩ t ht hat
    cases' eq_zero_or_pos (sup.{u, u} f) with ha₀ ha₀
    · rw [ha₀] at hat
      use 0, hat
      convert hf i
      exact (sup_eq_zero_iff.1 ha₀ i).symm
    rcases(mem_nhds_iff_exists_Ioo_subset' ⟨0, ha₀⟩ ⟨_, lt_succ _⟩).1 (ht.mem_nhds hat) with
      ⟨b, c, ⟨hab, hac⟩, hbct⟩
    cases' lt_sup.1 hab with i hi
    exact ⟨_, hbct ⟨hi, (le_sup.{u, u} f i).trans_lt hac⟩, hf i⟩
#align ordinal.mem_closure_iff_sup Ordinal.mem_closure_iff_sup
-/

#print Ordinal.mem_closed_iff_sup /-
theorem mem_closed_iff_sup (hs : IsClosed s) :
    a ∈ s ↔ ∃ (ι : Type u)(hι : Nonempty ι)(f : ι → Ordinal), (∀ i, f i ∈ s) ∧ sup.{u, u} f = a :=
  by rw [← mem_closure_iff_sup, hs.closure_eq]
#align ordinal.mem_closed_iff_sup Ordinal.mem_closed_iff_sup
-/

#print Ordinal.mem_closure_iff_bsup /-
theorem mem_closure_iff_bsup :
    a ∈ closure s ↔
      ∃ (o : Ordinal)(ho : o ≠ 0)(f : ∀ a < o, Ordinal),
        (∀ i hi, f i hi ∈ s) ∧ bsup.{u, u} o f = a :=
  mem_closure_iff_sup.trans
    ⟨fun ⟨ι, ⟨i⟩, f, hf, ha⟩ =>
      ⟨_, fun h => (type_eq_zero_iff_isEmpty.1 h).elim i, bfamilyOfFamily f, fun i hi => hf _, by
        rwa [bsup_eq_sup]⟩,
      fun ⟨o, ho, f, hf, ha⟩ =>
      ⟨_, out_nonempty_iff_ne_zero.2 ho, familyOfBFamily o f, fun i => hf _ _, by
        rwa [sup_eq_bsup]⟩⟩
#align ordinal.mem_closure_iff_bsup Ordinal.mem_closure_iff_bsup
-/

#print Ordinal.mem_closed_iff_bsup /-
theorem mem_closed_iff_bsup (hs : IsClosed s) :
    a ∈ s ↔
      ∃ (o : Ordinal)(ho : o ≠ 0)(f : ∀ a < o, Ordinal),
        (∀ i hi, f i hi ∈ s) ∧ bsup.{u, u} o f = a :=
  by rw [← mem_closure_iff_bsup, hs.closure_eq]
#align ordinal.mem_closed_iff_bsup Ordinal.mem_closed_iff_bsup
-/

#print Ordinal.isClosed_iff_sup /-
theorem isClosed_iff_sup :
    IsClosed s ↔
      ∀ {ι : Type u} (hι : Nonempty ι) (f : ι → Ordinal), (∀ i, f i ∈ s) → sup.{u, u} f ∈ s :=
  by
  use fun hs ι hι f hf => (mem_closed_iff_sup hs).2 ⟨ι, hι, f, hf, rfl⟩
  rw [← closure_subset_iff_isClosed]
  intro h x hx
  rcases mem_closure_iff_sup.1 hx with ⟨ι, hι, f, hf, rfl⟩
  exact h hι f hf
#align ordinal.is_closed_iff_sup Ordinal.isClosed_iff_sup
-/

#print Ordinal.isClosed_iff_bsup /-
theorem isClosed_iff_bsup :
    IsClosed s ↔
      ∀ {o : Ordinal} (ho : o ≠ 0) (f : ∀ a < o, Ordinal),
        (∀ i hi, f i hi ∈ s) → bsup.{u, u} o f ∈ s :=
  by
  rw [is_closed_iff_sup]
  refine' ⟨fun H o ho f hf => H (out_nonempty_iff_ne_zero.2 ho) _ _, fun H ι hι f hf => _⟩
  · exact fun i => hf _ _
  · rw [← bsup_eq_sup]
    apply H (type_ne_zero_iff_nonempty.2 hι)
    exact fun i hi => hf _
#align ordinal.is_closed_iff_bsup Ordinal.isClosed_iff_bsup
-/

#print Ordinal.isLimit_of_mem_frontier /-
theorem isLimit_of_mem_frontier (ha : a ∈ frontier s) : IsLimit a :=
  by
  simp only [frontier_eq_closure_inter_closure, Set.mem_inter_iff, mem_closure_iff] at ha
  by_contra h
  rw [← is_open_singleton_iff] at h
  rcases ha.1 _ h rfl with ⟨b, hb, hb'⟩
  rcases ha.2 _ h rfl with ⟨c, hc, hc'⟩
  rw [Set.mem_singleton_iff] at *
  subst hb; subst hc
  exact hc' hb'
#align ordinal.is_limit_of_mem_frontier Ordinal.isLimit_of_mem_frontier
-/

#print Ordinal.isNormal_iff_strictMono_and_continuous /-
theorem isNormal_iff_strictMono_and_continuous (f : Ordinal.{u} → Ordinal.{u}) :
    IsNormal f ↔ StrictMono f ∧ Continuous f :=
  by
  refine' ⟨fun h => ⟨h.StrictMono, _⟩, _⟩
  · rw [continuous_def]
    intro s hs
    rw [is_open_iff] at *
    intro o ho ho'
    rcases hs _ ho (h.is_limit ho') with ⟨a, ha, has⟩
    rw [← IsNormal.bsup_eq.{u, u} h ho', lt_bsup] at ha
    rcases ha with ⟨b, hb, hab⟩
    exact
      ⟨b, hb, fun c hc =>
        Set.mem_preimage.2 (has ⟨hab.trans (h.strict_mono hc.1), h.strict_mono hc.2⟩)⟩
  · rw [is_normal_iff_strict_mono_limit]
    rintro ⟨h, h'⟩
    refine' ⟨h, fun o ho a h => _⟩
    suffices : o ∈ f ⁻¹' Set.Iic a
    exact Set.mem_preimage.1 this
    rw [mem_closed_iff_sup (IsClosed.preimage h' (@isClosed_Iic _ _ _ _ a))]
    exact
      ⟨_, out_nonempty_iff_ne_zero.2 ho.1, typein (· < ·), fun i => h _ (typein_lt_self i),
        sup_typein_limit ho.2⟩
#align ordinal.is_normal_iff_strict_mono_and_continuous Ordinal.isNormal_iff_strictMono_and_continuous
-/

/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (b «expr < » a) -/
#print Ordinal.enumOrd_isNormal_iff_isClosed /-
theorem enumOrd_isNormal_iff_isClosed (hs : s.Unbounded (· < ·)) :
    IsNormal (enumOrd s) ↔ IsClosed s :=
  by
  have Hs := enum_ord_strict_mono hs
  refine'
    ⟨fun h => is_closed_iff_sup.2 fun ι hι f hf => _, fun h =>
      (is_normal_iff_strict_mono_limit _).2 ⟨Hs, fun a ha o H => _⟩⟩
  · let g : ι → Ordinal.{u} := fun i => (enum_ord_order_iso hs).symm ⟨_, hf i⟩
    suffices enum_ord s (sup.{u, u} g) = sup.{u, u} f
      by
      rw [← this]
      exact enum_ord_mem hs _
    rw [@IsNormal.sup.{u, u, u} _ h ι g hι]
    congr
    ext
    change ((enum_ord_order_iso hs) _).val = f x
    rw [OrderIso.apply_symm_apply]
  · rw [is_closed_iff_bsup] at h
    suffices : enum_ord s a ≤ bsup.{u, u} a fun b (_ : b < a) => enum_ord s b
    exact this.trans (bsup_le H)
    cases'
      enum_ord_surjective hs _
        (h ha.1 (fun b hb => enum_ord s b) fun b hb => enum_ord_mem hs b) with
      b hb
    rw [← hb]
    apply Hs.monotone
    by_contra' hba
    apply (Hs (lt_succ b)).not_le
    rw [hb]
    exact le_bsup.{u, u} _ _ (ha.2 _ hba)
#align ordinal.enum_ord_is_normal_iff_is_closed Ordinal.enumOrd_isNormal_iff_isClosed
-/

end Ordinal

author: leanprover-community


text:
-- wWARNING : OLD INEFFICIENT CODE
#exit
-- this wsas written presumably in Oct 2017 by KB when he knew nothing

import analysis.real init.classical tactic.norm_num

namespace M1F

def floor_set (x : ℝ) : set ℝ := { y : ℝ | y ≤ x ∧ ∃ n : ℤ, y = ↑n }

lemma floor_set_nonempty (x : ℝ) : ∃ s : ℝ, s ∈ floor_set x :=
let ⟨m,Hm⟩ := exists_lt_nat (-x) in
⟨-m,begin
  split,
  { exact le_of_lt (neg_lt.1 Hm)},
  existsi (-(m:ℤ)),
  simp,
end⟩

lemma floor_set_bounded (x : ℝ) : ∃ B : ℝ, B ∈ upper_bounds (floor_set x) :=
⟨x,λ _ H,H.left⟩

theorem exists_real_floor (x : ℝ) : ∃ (n : ℤ), ↑n ≤ x ∧ x < n+1 :=
begin
let S :=floor_set x,
have H₁ := floor_set_nonempty x,
cases H₁ with z Hz,
have HB : x ∈ upper_bounds (floor_set x)
have H₂ := floor_set_bounded x,
cases H₂ with B HB,

have lub_exists := exists_supremum_real Hz HB,
cases lub_exists with m Hm,

have H1 : ∃ s : ℝ, s ∈ S := let ⟨m,Hm⟩ := exists_lt_nat (-x) in
⟨-m,begin
  split,
  { exact le_of_lt (neg_lt.1 Hm)},
  existsi (-(m:ℤ)),
  simp,
end⟩

end

theorem floor_real_exists : ∀ (x : ℝ), ∃ (n : ℤ), ↑n ≤ x ∧ x < n+1 :=
begin
intro x,
have H : ∃ (q : ℚ), x < ↑q ∧ ↑q < x + 1,
  exact @exists_rat_btwn x (x+1) (by simp [zero_lt_one]),
cases H with q Hq,
cases classical.em (x < rat.floor q) with Hb Hs,
  exact ⟨rat.floor q - 1,
  begin
  split,
    rw [int.cast_sub,int.cast_one],
    apply sub_left_le_of_le_add _,
    rw [add_comm],
    suffices H7 : (↑q:real) ≤ x+1,
      exact calc (↑(rat.floor q):ℝ) = (↑((rat.floor q):ℚ):ℝ) : by simp
      ... ≤ (↑q:ℝ) : rat.cast_le.mpr (rat.floor_le q)
      ... ≤ x+1 : H7,
    exact le_of_lt Hq.right,
  rwa [int.cast_sub,int.cast_one,sub_add_cancel],
  end
  ⟩,

  exact ⟨rat.floor q,
    begin
    split,
      have H : (x < ↑(rat.floor q)) ∨ (x ≥ ↑(rat.floor q)),
        exact lt_or_ge x ↑(rat.floor q),
      cases H with F T,
        exact false.elim (Hs F),
      exact T,

    clear Hs,
    have H1 : x < ↑q,
      { exact Hq.left },
    clear Hq,

      -- insanity starts here

    suffices H2 : q < ↑((rat.floor q)+(1:ℤ)),
      exact calc x < (q:ℝ) : H1
      ... < ((((rat.floor q + 1):ℤ):ℚ):ℝ) : rat.cast_lt.2 H2
      ... = (((rat.floor q + 1):ℤ):ℝ) : by simp
      ... = ((rat.floor q):ℝ)+((1:ℤ):ℝ) : int.cast_add _ _
      ... = ↑(rat.floor q) + 1 : by rw [int.cast_one],
    clear H1,
    exact rat.lt_succ_floor q,
  end⟩
end

lemma rational_half_not_an_integer : ¬ (∃ y : ℤ, 1/2 = (y:rat)) :=
begin
apply not_exists.2,
rw [one_div_eq_inv],
assume x:ℤ,
intro H,
have H6 : ((1:ℤ):ℚ)=((2:ℤ):ℚ)*x,
  exact calc
  ((1:ℤ):ℚ) = (1:ℚ) : by simp
  ... = (2:ℚ)* 2⁻¹ : eq.symm (mul_inv_cancel (by norm_num))
  ... = (2*x) : by rw[H],
clear H,
rw [←int.cast_mul,int.cast_inj] at H6,
have H : (1:ℤ) = 0,
exact calc (1:ℤ) = 1 % 2 : eq.symm (int.mod_eq_of_lt (by norm_num) (by norm_num))
... = (2*x) % 2 : eq.symm (by rw [←H6])
... = 0 : by simp,
revert H,
norm_num,
end

-- set_option pp.all true

lemma real_half_not_an_integer : ¬ (∃ y : ℤ, ((1/2):ℝ) = (y:ℝ)) :=
begin
assume H_real : (∃ y : ℤ, ((1/2):ℝ) = (y:ℝ)),
cases H_real with a Ha,
suffices H2 : ((1:ℤ):ℝ) = ((2:ℤ):ℝ)*((a:ℤ):ℝ),
  rw [←int.cast_mul,int.cast_inj] at H2,
  have H8 : (2*a) % 2 = 0,
    simp [@int.add_mul_mod_self 0],
  have H9 : (1:int) % 2 = 0,
    apply @eq.subst ℤ  (λ t, t%2 =0) _ _ (eq.symm H2) H8,
  have H10 : (1:int) % 2 ≠ 0,
    exact dec_trivial,
  contradiction,
have H20: (2:ℝ) ≠ 0, {norm_num},
have H1 : (↑a:ℝ) * 2 = 1,
  exact mul_eq_of_eq_div (a:ℝ) 1 H20 (eq.symm Ha),
have H2 : 1 = 2 * (↑a:ℝ),
  rw [mul_comm] at H1,
  exact eq.symm (H1),
have H3 : (1:ℝ) = ((1:ℤ):ℝ), by simp,
have H4 : (2:ℝ) = ((2:ℤ):ℝ), by simp,
rwa [←H3,←H4],
end

definition is_irrational (x : ℝ) := ¬ (∃ (q : ℚ), (q:ℝ) = x)

end M1F

author: kbuzzard

repo: xena

save_path: github-repos/lean/kbuzzard-xena


text:
lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
begin
intros h1 h2,
rwa [h1, h2],
end

author: chanha-park

repo: naturalNumberGame


text:
/-
This definition of UFD is quite clunky! I will instead use the one in the groups + rings notes in Thm 5.12
to avoid having to deal with factorisations.

structure factorisation (r : R) :=
(els : finset R)
(no_units : ∀ (t : R), t ∈ els → ¬is_unit t)
(irreducible : ∀ (t : R), t ∈ els → irreducible t)
(prod_r : finset.prod els (λ x, x) = r)

def facts_equiv {r : R} (a b : factorisation r) : Prop :=
  ∀(t : R), t ∈ a.els ↔ ∃ (c d: R), is_unit c ∧ d ∈ b.els ∧ c * d = t

def is_ufd  (R : Type) [comm_ring R] [is_integral_domain R] : Prop :=
  ∀(r : R), ¬(is_unit r) → ∃ (f : factorisation r), ∀ (g : factorisation r), facts_equiv f g

lemma irreducible_is_prime_ufd {b a p : R} (hint : is_integral_domain R) (hufd : @is_ufd R _ hint): irreducible p → (p \ (a*b)) →  p \ a ∨ p \ b:=
begin
  intro hirr,
  intro hdiv,
  by_cases ha :(is_unit a) ,
    rw is_unit_iff_exists_inv at ha,
    right,
    cases ha with ainv hainv,
    cases hdiv,
    use (hdiv_w * ainv),
    apply_fun (λ x, ainv * x) at hdiv_h,
    rw ←mul_assoc at hdiv_h, rw mul_comm at hainv,
    rw hainv at hdiv_h, rw one_mul at hdiv_h,
    rw ←mul_assoc, rw mul_comm, exact hdiv_h,
  by_cases hb : is_unit b,
    rw is_unit_iff_exists_inv at hb,
    left,
    cases hb with binv hbinv,
    cases hdiv,
    use (hdiv_w * binv),
    apply_fun (λ x, binv * x) at hdiv_h,
    rw mul_comm at hdiv_h,
    rw mul_assoc at hdiv_h,
    rw hbinv at hdiv_h,
    rw mul_one at hdiv_h, rw ← mul_assoc,
    rw mul_comm, exact hdiv_h,
    by_contra,
end

-/

author: sterguel

repo: formalising-mathematics


text:
/-
Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Bhavik Mehta
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.category_theory.opposites
import Mathlib.PostPort

universes u₂ v₂ u₁ v₁ u₃ v₃

namespace Mathlib

namespace category_theory.functor

/--
The functor sending `X : C` to the constant functor `J ⥤ C` sending everything to `X`.
-/
def const (J : Type u₁) [category J] {C : Type u₂} [category C] : C ⥤ J ⥤ C :=
  mk (fun (X : C) => mk (fun (j : J) => X) fun (j j' : J) (f : j ⟶ j') => 𝟙)
    fun (X Y : C) (f : X ⟶ Y) => nat_trans.mk fun (j : J) => f

namespace const

@[simp] theorem obj_obj {J : Type u₁} [category J] {C : Type u₂} [category C] (X : C) (j : J) : obj (obj (const J) X) j = X :=
  rfl

@[simp] theorem obj_map {J : Type u₁} [category J] {C : Type u₂} [category C] (X : C) {j : J} {j' : J} (f : j ⟶ j') : map (obj (const J) X) f = 𝟙 :=
  rfl

@[simp] theorem map_app {J : Type u₁} [category J] {C : Type u₂} [category C] {X : C} {Y : C} (f : X ⟶ Y) (j : J) : nat_trans.app (map (const J) f) j = f :=
  rfl

/--
The contant functor `Jᵒᵖ ⥤ Cᵒᵖ` sending everything to `op X`
is (naturally isomorphic to) the opposite of the constant functor `J ⥤ C` sending everything to `X`.
-/
def op_obj_op {J : Type u₁} [category J] {C : Type u₂} [category C] (X : C) : obj (const (Jᵒᵖ)) (opposite.op X) ≅ functor.op (obj (const J) X) :=
  iso.mk (nat_trans.mk fun (j : Jᵒᵖ) => 𝟙) (nat_trans.mk fun (j : Jᵒᵖ) => 𝟙)

@[simp] theorem op_obj_op_hom_app {J : Type u₁} [category J] {C : Type u₂} [category C] (X : C) (j : Jᵒᵖ) : nat_trans.app (iso.hom (op_obj_op X)) j = 𝟙 :=
  rfl

@[simp] theorem op_obj_op_inv_app {J : Type u₁} [category J] {C : Type u₂} [category C] (X : C) (j : Jᵒᵖ) : nat_trans.app (iso.inv (op_obj_op X)) j = 𝟙 :=
  rfl

/--
The contant functor `Jᵒᵖ ⥤ C` sending everything to `unop X`
is (naturally isomorphic to) the opposite of
the constant functor `J ⥤ Cᵒᵖ` sending everything to `X`.
-/
def op_obj_unop {J : Type u₁} [category J] {C : Type u₂} [category C] (X : Cᵒᵖ) : obj (const (Jᵒᵖ)) (opposite.unop X) ≅ functor.left_op (obj (const J) X) :=
  iso.mk (nat_trans.mk fun (j : Jᵒᵖ) => 𝟙) (nat_trans.mk fun (j : Jᵒᵖ) => 𝟙)

-- Lean needs some help with universes here.

@[simp] theorem op_obj_unop_hom_app {J : Type u₁} [category J] {C : Type u₂} [category C] (X : Cᵒᵖ) (j : Jᵒᵖ) : nat_trans.app (iso.hom (op_obj_unop X)) j = 𝟙 :=
  rfl

@[simp] theorem op_obj_unop_inv_app {J : Type u₁} [category J] {C : Type u₂} [category C] (X : Cᵒᵖ) (j : Jᵒᵖ) : nat_trans.app (iso.inv (op_obj_unop X)) j = 𝟙 :=
  rfl

@[simp] theorem unop_functor_op_obj_map {J : Type u₁} [category J] {C : Type u₂} [category C] (X : Cᵒᵖ) {j₁ : J} {j₂ : J} (f : j₁ ⟶ j₂) : map (opposite.unop (obj (functor.op (const J)) X)) f = 𝟙 :=
  rfl

end const

/-- These are actually equal, of course, but not definitionally equal
  (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is
  more convenient than an equality between functors (compare id_to_iso). -/
def const_comp (J : Type u₁) [category J] {C : Type u₂} [category C] {D : Type u₃} [category D] (X : C) (F : C ⥤ D) : obj (const J) X ⋙ F ≅ obj (const J) (obj F X) :=
  iso.mk (nat_trans.mk fun (_x : J) => 𝟙) (nat_trans.mk fun (_x : J) => 𝟙)

/-- If `J` is nonempty, then the constant functor over `J` is faithful. -/
protected instance const.category_theory.faithful (J : Type u₁) [category J] {C : Type u₂} [category C] [Nonempty J] : faithful (const J) :=
  faithful.mk

author: AurelienSaue


text:
-- Transitividad_de_la_igualdad.lean
-- Transitividad de la igualdad.
-- José A. Alonso Jiménez
-- Sevilla, 12 de agosto de 2020
-- ---------------------------------------------------------------------

-- En esta relación se muestra distintas pruebas de la transitividad de
-- la igualdad de los números reales: por reescritura, sustitución, con
-- lemas y automáticas.

-- ---------------------------------------------------------------------
-- Ejercicio. Realizar las siguientes acciones:
-- 1. Importar la teoría de los números reales.
-- 2. Declarar x, y y z como variables sobre los números reales.
-- ----------------------------------------------------------------------

import data.real.basic   -- 1
variables (x y z : ℝ)    -- 2

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que la igualdad en los reales es transitiva; es
-- decir, si x, y y z son números reales tales que x = y e y = z,
-- entonces x = z.
-- ----------------------------------------------------------------------

-- 1ª demostración (con reescritura)
-- =================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
begin
  rw h,
  exact h',
end

-- Prueba:
/-
  x y z : ℝ,
  h : x = y,
  h' : y = z
  ⊢ x = z
rw h,
  ⊢ y = z
exact h',
  no goals
-/

-- Comentarios:
-- + La táctica (rw h) cuando h es una igualdad sustituye en la
--   conclusión el término izquierdo de h por el derecho.
-- + La táctica (exact h) concluye la demostración si h es del tipo de
--   la conclusión.

-- 2ª demostración (con reescritura inversa)
-- =========================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
begin
  rw ← h',
  exact h,
end

-- Prueba:
/-
  x y z : ℝ,
  h : x = y,
  h' : y = z
  ⊢ x = z
rw ← h',
  ⊢ x = y
exact h,
  no goals
-/

-- Comentarios:
-- + La táctica (rw ← h) cuando h es una igualdad sustituye en la
--   conclusión el término derecho de h por el izquierdo

-- 3ª demostración (con reescritura en hipótesis)
-- ==============================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
begin
  rw h' at h,
  exact h,
end

-- Prueba:
/-
  x y z : ℝ,
  h : x = y,
  h' : y = z
  ⊢ x = z
rw h' at h,
  h : x = z
  ⊢ x = z
exact h,
  no goals
-/

-- Comentarios:
-- + La táctica (rw h1 at h2) cuando h1 es una igualdad sustituye en la
--   hipótesis h2 el término izquierdo de h1 por el derecho.

-- 4ª demostración (con reescritura inversa en hipótesis)
-- ======================================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
begin
  rw ← h at h',
  exact h',
end

-- Prueba:
/-
  x y z : ℝ,
  h : x = y,
  h' : y = z
  ⊢ x = z
rw ← h at h',
  h' : x = z
  ⊢ x = z
exact h',
  no goals
-/

-- Comentarios:
-- + La táctica (rw ← h1 at h2) cuando h1 es una igualdad sustituye en la
--   hipótesis h2 el término derecho de h1 por el izquierdo

-- 5ª demostración (con un lema)
-- =============================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
eq.trans h h'

-- Comentarios:
-- + Se ha usado el lema
--   + eq.trans : a = b → b = c → a = c
-- + El lema se puede encontrar con
--      by suggest

-- 6ª demostración (por sustitución)
-- =================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
h' ▸ h

-- Comentario:
-- + Si h es una igualdad entonces h ▸ h' es la expresión obtenida sustituyendo
--   en h' el término izquierdo de h por el derecho.

-- 7ª demostración (automática con linarith)
-- =========================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
by linarith

-- Comentarios:
-- + La táctica linarith demuestra la conclusión mediante aritmética
--   lineal.
-- + La sugerencia de usar linarith se puede obtener escrbiendo
--      by hint

-- 8ª demostración (automática con finish)
-- =======================================

example
  (h : x = y)
  (h' : y = z)
  : x = z :=
by finish

-- Comentario:
-- + La táctica finish demuestra la conclusión de forma automática.
-- + La sugerencia de usar finish se puede obtener escrbiendo
--      by hint

author: jaalonso


text:
import system_of_complexes.basic

universe variables u

noncomputable theory
open_locale nnreal
open category_theory opposite normed_group_hom system_of_complexes

variables (M M' N : system_of_complexes.{u}) (f : M ⟶ M') (g : M' ⟶ N)

/-- The normed snake lemma, weak version. See Proposition 9.10 from Analytic.pdf -/
--TODO Add the non weak version for complete system of complexes
lemma weak_normed_snake {k k' k'' K K' K'' : ℝ≥0}
  [hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')] [hk'' : fact (1 ≤ k'')]
  {m : ℕ} {c₀ : ℝ≥0}
  (hM : M.is_weak_bounded_exact k K (m+1) c₀)
  (hM' : M'.is_weak_bounded_exact k' K' (m+1) c₀)
  (hM'_adm : M'.admissible)
  (hf : ∀ c i, (f.apply : M c i ⟶ M' c i).norm_noninc)
  (Hf : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (x : M (k'' * c) i),
    ∥(res x : M c i)∥ ≤ K'' * ∥f x∥)
  (hg : ∀ c i, (g.apply : M' c i ⟶ N c i).ker = f.apply.range)
  (hgquot : system_of_complexes.is_quotient g) :
  N.is_weak_bounded_exact (k''*k*k') (K'*(K*K'' + 1)) m c₀ :=
begin
  introsI c hc i hi,
  let c₁ := k'' * (k * (k' * c)),
  suffices : ∀ n : N c₁ i, ∀ ε > 0,
    ∃ i₀ (hi₀ : i₀ = i - 1) (y : N c i₀),
      ∥res n - N.d _ _ y∥ ≤ K' * (K * K'' + 1) * ∥N.d i (i+1) n∥ + ε,
  { dsimp [c₁] at this,
    intros n₁ ε hε,
    haveI hc : fact (k'' * k * k' * c = c₁) :=
      { out := (mul_assoc _ _ _).trans ((mul_assoc _ _ _).trans rfl) },
    rcases this (res n₁) ε hε with ⟨i₀, hi₀, y, hy⟩,
    rw [res_res, d_res] at hy,
    refine ⟨i₀, _, hi₀, rfl, _⟩,
    refine ⟨y, hy.trans (add_le_add_right (mul_le_mul_of_nonneg_left _ _) ε)⟩,
    { apply (admissible_of_quotient hgquot hM'_adm).res_norm_noninc },
    { exact (nnreal.zero_le_coe : 0 ≤ K' * (K * K'' + 1)) } },
  intros n ε hε,
  let ε₁ := ε/(K' * (K * K'' + 2) + 1),

  have hε₁ : 0 < ε₁ :=
    div_pos hε (lt_of_lt_of_le zero_lt_one (nnreal.one_le_add'.out : 1 ≤ K' * (K * K'' + 2) + 1)),

  obtain ⟨m' : M' c₁ i, rfl : g m' = n⟩ := (hgquot _ _).surjective _,
  let m₁' := M'.d i (i+1) m',
  have hm₁' : g m₁' = N.d i (i+1) (g m') := (d_apply _ _ g m').symm,
  obtain ⟨m₁'' : M' c₁ (i+1),
          hgm₁'' : g m₁'' = N.d i (i+1) (g m'),
          hnorm_m₁'' : ∥m₁''∥ < ∥N.d i (i+1) (g m')∥ + ε₁⟩ :=
    (hgquot _ _).norm_lift hε₁ (N.d i (i+1) (g m')),
  obtain ⟨m₁, hm₁⟩ : ∃ m₁ : M c₁ (i+1), f m₁ + m₁'' = m₁',
  { have hrange : m₁' - m₁'' ∈ f.apply.range,
    { rw [← hg _ _, mem_ker  _ _, normed_group_hom.map_sub],
      change g m₁' - g m₁'' = 0,
      rw [hm₁', hgm₁'', sub_self] },
    obtain ⟨m₁, hm₁ : f m₁ = m₁' - m₁''⟩ := (mem_range _ _).1 hrange,
    exact ⟨m₁, by rw [hm₁, sub_add_cancel]⟩ },

  have him : i+2 ≤ m+2 := add_le_add_right hi _,
  have hm₂ : f (M.d (i+1) (i+2) m₁) = -M'.d (i+1) (i+2) m₁'',
  { rw [← d_apply, eq_sub_of_add_eq hm₁, normed_group_hom.map_sub, ← category_theory.comp_apply,
       d_comp_d, coe_zero, ← neg_inj, pi.zero_apply, zero_sub], },
  have hle : ∥res (M.d (i+1) (i+2) m₁)∥ ≤ K'' * ∥m₁''∥,
  { calc ∥res (M.d (i+1) (i+2) m₁)∥
        ≤ K'' * ∥f (M.d (i+1) (i+2) m₁)∥ : Hf _ _ him _
    ... = K'' * ∥M'.d (i+1) (i+2) m₁''∥ : by rw [hm₂, norm_neg]
    ... ≤ K'' * ∥m₁''∥ : (mul_le_mul_of_nonneg_left
                           (hM'_adm.d_norm_noninc _ _ _ _ m₁'') $ nnreal.coe_nonneg K'') },
  obtain ⟨i', j, hi', rfl, m₀, hm₀⟩ :=
    hM _ ⟨hc.out.trans $ le_mul_of_one_le_left' hk'.out⟩ _ (nat.succ_le_succ hi) (res m₁) ε₁ hε₁,
  rw [← nat.pred_eq_sub_one, i.pred_succ] at hi', subst i',
  replace hm₀ : ∥res m₁ - M.d i (i+1) m₀∥ ≤ K * K'' * ∥N.d i (i+1) (g m')∥ + K*K''*ε₁ + ε₁,
  { calc ∥res m₁ - M.d i (i+1) m₀∥  = ∥res (res m₁) - M.d i (i+1) m₀∥ : by rw res_res
    ... ≤ K * ∥M.d (i+1) (i+2) (res m₁)∥ + ε₁ : hm₀
    ... = K * ∥res (M.d (i+1) (i+2) m₁)∥ + ε₁ : by rw d_res
    ... ≤ K*(K'' * ∥m₁''∥) + ε₁ : add_le_add_right (mul_le_mul_of_nonneg_left hle nnreal.zero_le_coe) _
    ... ≤ K*(K'' * (∥N.d i (i+1) (g m')∥ + ε₁)) + ε₁ :  add_le_add_right (mul_le_mul_of_nonneg_left
                                        (mul_le_mul_of_nonneg_left hnorm_m₁''.le nnreal.zero_le_coe)
                                         nnreal.zero_le_coe) ε₁
    ... = K * K'' * ∥N.d i (i+1) (g m')∥ + K*K''*ε₁ + ε₁ : by ring },

  let mnew₁' := M'.d i (i+1) (res m' - f m₀),
  have hmnew' : mnew₁' = res m₁'' + f (res m₁ - M.d i (i+1) m₀),
  { calc mnew₁'
        = M'.d i (i+1) (res m' - f m₀) : rfl
    ... = res (M'.d i (i+1) m') - (f (M.d i (i+1) m₀)) : by rw [normed_group_hom.map_sub, d_res _, d_apply]
    ... = res (M'.d i (i+1) m') - (f (res m₁)) + (f (res m₁) - f (M.d i (i+1) m₀)) : by abel
    ... = res m₁'' + f ((res m₁) - (M.d i (i+1) m₀)) : by
                        { rw [← system_of_complexes.map_sub, ← res_apply,
                              ← normed_group_hom.map_sub, ← sub_eq_of_eq_add' hm₁.symm] } },
  have hnormle : ∥mnew₁'∥ ≤ (K*K'' + 1)*∥N.d i (i+1) (g m')∥ + (K*K'' + 2) * ε₁,
  { calc ∥mnew₁'∥
        = ∥res m₁'' + f (res m₁ - M.d i (i+1) m₀)∥ : by rw [hmnew']
    ... ≤ ∥res m₁''∥ + ∥f (res m₁ - M.d i (i+1) m₀)∥ : norm_add_le _ _
    ... ≤ ∥m₁''∥ + ∥f (res m₁ - M.d i (i+1) m₀)∥ : add_le_add_right
                                      (hM'_adm.res_norm_noninc _ _ _ _ m₁'') _
    ... ≤ ∥m₁''∥ + ∥res m₁ - M.d i (i+1) m₀∥ : add_le_add_left (hf _ _ _) _
    ... ≤ ∥N.d i (i+1) (g m')∥ + ε₁ + ∥res m₁ - M.d i (i+1) m₀∥ : add_le_add_right (le_of_lt hnorm_m₁'')  _
    ... ≤ ∥N.d i (i+1) (g m')∥ + ε₁ + (K * K'' * ∥N.d i (i+1) (g m')∥ + K * K'' * ε₁ + ε₁) : add_le_add_left hm₀ _
    ... = (K*K'' + 1)*∥d _ _ (i+1) (g m')∥ + (K*K'' + 2) * ε₁ : by ring },
  obtain ⟨i₀, _, hi₀, rfl, mnew₀, hmnew₀⟩ := hM' _ hc _ (hi.trans m.le_succ) (res m' - f m₀) _ hε₁,
  replace hmnew₀ : ∥res (res m' - f m₀) - d _ _ _ mnew₀∥ ≤
    K' * ((K * K'' + 1) * ∥N.d i (i+1) (g m')∥ + (K * K'' + 2) * ε₁) + ε₁ :=
    hmnew₀.trans (add_le_add_right (mul_le_mul_of_nonneg_left hnormle nnreal.zero_le_coe) ε₁),
  let nnew₀ : ↥(N c i₀) := g mnew₀,
  have hmnewlift : g (res (res m' - f m₀) - M'.d i₀ i mnew₀) = res (g m') - N.d i₀ i nnew₀,
  { suffices h : g (res m' - f m₀) = res (g m'),
    { rw [system_of_complexes.map_sub, ← res_apply, ← d_apply, h, res_res] },
    rw system_of_complexes.map_sub,
    have hker : f m₀ ∈ g.apply.ker,
    { rw [hg _ _, mem_range _ _],
      exact ⟨m₀, rfl⟩ },
    replace hker : g (f m₀) = 0, { rwa mem_ker at hker },
    rw [hker, sub_zero, ← res_apply] },
  refine ⟨i₀, hi₀, nnew₀, _⟩,
  rw ← hmnewlift,
  refine ((hgquot _ _).norm_le _).trans (hmnew₀.trans (le_of_eq _)),
  have hε₁_ε : (K' * (K * K'' + 2) + 1 : ℝ)*ε₁ = ε := mul_div_cancel' _
    (by { refine (lt_of_lt_of_le zero_lt_one _).ne',
          exact (nnreal.one_le_add'.out : 1 ≤ K' * (K * K'' + 2) + 1) }),
  rw ← hε₁_ε,
  ring,
end

author: bentoner

repo: debug

save_path: github-repos/lean/bentoner-debug


text:
-- inverse categories

import algebra.category data.nat
import algebra.category.constructions

import .fibrant .finite

import open nat

open nat.le functor
open category category.ops eq.ops

definition nat_cat_op [instance] : category ℕ :=
  ⦃ category,
    hom := λ a b, a ≥ b,
    comp := λ a b c, @nat.le_trans c b a,
    ID := nat.le_refl,
    assoc := λ a b c d h g f, eq.refl _,
    id_left := λ a b f, eq.refl _,
    id_right := λ a b f, eq.refl _ ⦄

definition ℕop := Mk nat_cat_op

lemma hom_ℕop_id {C : Category} {x : ℕop} {f : x ⟶ x} : f = id := rfl

-- ref:def:inverse-category
-- Definition 4.1
namespace invcat
  open sigma.ops iff
  definition id_reflect {C D: Category} (φ : C ⇒ D) :=
    Π ⦃x y : C⦄ (f : x ⟶ y), (Σ (q : φ x = φ y), q ▹ φ f = id) → Σ (p : x = y),  p ▹ f = id

  definition id_reflect' {C D: Category} :=
  Π (φ : C ⇒ D) ⦃x y : C⦄ (f : x ⟶ y), (Σ (q : φ x = φ y), q ▹ φ f = id) → Σ (p : x = y),  p ▹ f = id

  definition transport {A : Type} := @eq.rec_on A
  notation x ≡ y := eq x y

  definition id_reflect'' {C D: Category} :=
  Π (φ : C ⇒ D) {x y : C} (f : hom x y),
  (Σ (q : φ y ≡ φ x), transport q (φ f) ≡ id) → Σ (p : y ≡ x),
  @transport _ _ _ _ p f ≡ id

  -- definition if "refect identity" property specific to ℕop.
  -- Though this definition doesn't require for φ(f) to be an identity, we will show that
  -- id_reflect(C,ℕop) and id_reflect_ℕop(C) are logically equivalent
  definition id_reflect_ℕop {C : Category} (φ : C ⇒ ℕop) :=
    Π ⦃x y : C⦄ (f : x ⟶ y), φ x = φ y → (Σ (p : x = y), p ▹ f = id)

  definition id_reflect_ℕop' {C : Category} (φ : C ⇒ ℕop) :=
    Π {x y : C} (f : x ⟶ y),
    φ x ≡ φ y → (Σ (p : x ≡ y), transport p f ≡ id)

  -- have to pack functor with the property that it reflects identities,
  -- because functor itself is not a type class
  structure has_idreflect [class] (C D : Category) :=
    (φ : C ⇒ D)
    (reflecting_id : id_reflect φ)

  section id_reflect_ℕop_iff

  -- showing that id_reflect_ℕop φ ↔ id_reflect φ
  -- NOTE: (Danil) I couldn't find instance of iff for Type
  definition map_id_reflect_ℕop {C : Category} (φ : C ⇒ ℕop):
    id_reflect_ℕop φ → id_reflect φ :=
    begin
      intros id_r_ℕop x y f s, cases s with [q, Heq], cases id_r_ℕop f q with [p₁, p₂],
      existsi p₁, cases p₁, esimp at *, apply p₂
    end

  definition map_ℕop_id_reflect {C : Category} (φ : C ⇒ ℕop):
    id_reflect φ → id_reflect_ℕop φ :=
    begin intros id_r x y f q,
    -- here we use the fact that any morphism x ⟶ x in ℕop only can be an identity morphism
    have f_is_id : q ▹ morphism φ f = id, from rfl,
    cases id_r f ⟨q,f_is_id⟩ with [p₁, p₂], existsi p₁, cases p₁, esimp at *, apply p₂
    end

  end id_reflect_ℕop_iff

  structure invcat [class] (C : Category) :=
    (reflecting_id_ℕop : has_idreflect C ℕop)

end invcat

-- some facts about inverse categories
section invcat_facts
  open invcat function sigma.ops

  definition endomorphism_is_id {C : Category} [invC : invcat C] {c : C} (f : c ⟶ c) : f = id :=
  begin cases invC with H, cases H with [φ, id_r], apply (id_r f ⟨rfl,rfl⟩).2 end

  lemma idreflect_inj_hom {C : Category} {x y : C} [idr : has_idreflect C ℕop] (f : x ⟶ y) :
    (has_idreflect.φ C ℕop) x = (has_idreflect.φ C ℕop) y → x = y :=
    begin cases idr with [φ, idr_φ], esimp, intro  H, cases (idr_φ f ⟨H,rfl⟩), assumption end

  definition has_le_ℕop [instance] : has_le ℕop := nat_has_le
  definition has_lt_ℕop [instance] : has_lt ℕop := nat_has_lt

  definition strict_order_ℕop [instance] : strict_order ℕop :=
    strict_order.mk nat.lt begin intros, refine (@lt.irrefl ℕ _ a a_1) end
    begin intros a b c, apply nat.lt_trans end

  definition weak_order_ℕop [instance] : weak_order ℕop :=
    weak_order.mk nat.le (@le.refl ℕ _) (λ a b c, @nat.le_trans a b c) (λ a b, nat.le_antisymm)

  definition no_incoming_non_id_arrows {C : Category.{1 1}}
    (z : C) {φ : C ⇒ ℕop} {max_rank : ∀ y, φ y ≤ φ z} {reflecting_id : id_reflect φ}
    : ¬ ∃ y : C, ∃ (f : y ⟶ z), y ≠ z :=
    begin intro H, cases H with [y, s], cases s with [f, y_ne_z], unfold id_reflect at *,
      have H : φ y ≥ φ z, from φ f,
      cases reflecting_id f ⟨le.antisymm (max_rank y) H, rfl⟩ with [p, Heq],
      apply y_ne_z, assumption
    end
end invcat_facts

open invcat
open unit

definition triv_funct : Category_one ⇒ ℕop :=
  functor.mk (λ (x : unit), zero) (λ a b p, id) (λa, eq.refl _) (λa b c p q, eq.refl _)

definition triv_funct_id_reflect [instance] : has_idreflect Category_one ℕop :=
  has_idreflect.mk
    triv_funct
    begin
      intros x y f,
      cases x, cases y, intro p,
      existsi (eq.refl _),
      cases f, reflexivity
    end

definition triv_cat_inverse [instance] : invcat Category_one := invcat.mk _

structure subcat_obj (C : Category) (p : objects C → Prop) :=
  (obj : objects C)
  (prop : p obj)

open subcat_obj function
attribute subcat_obj.obj [coercion]

section subcategory
  variables {C : Category.{1 1}}
            {D : Category}

definition subcat [instance] (C : Category) (p : C → Prop) : category (subcat_obj C p) :=
  ⦃ category,
    hom := λ (a b : subcat_obj C p), obj a ⟶ obj b,
    comp := λ a b c, @comp _ _ _ _ _,
    ID := λ (a : subcat_obj C p), ID (obj a),
    assoc := λ a b c d h g f, assoc h g f,
    id_left := λ a b f, id_left f,
    id_right := λ a b f, id_right f ⦄

definition Subcat (C : Category) (p : C → Prop) : Category := Mk (subcat C p)

-- A subcategory of [C] with one object removed.
-- We also refer to this category as C'
definition C_without_z {C : Category.{1 1}}(z : C) : Category := Mk (subcat C (λ c, c ≠ z))

-- use apply tactic, as it allows to infer correct implicits
definition Functor_from_C' [reducible] (z : C) (X : C ⇒ D) : C_without_z z ⇒ D :=
 ⦃ functor,
   object := λ ob, X (obj ob),
   morphism := λ a b f, by apply X f,
   respect_id := λ a, by apply respect_id X (obj a),
   respect_comp := λ a b c g f, by apply @respect_comp _ _ X (obj a) (obj b) (obj c) _ _ ⦄

open eq.ops function
definition C_without_z_invcat [instance] (z : C) [invC : invcat C] : invcat (C_without_z z) :=
  begin
    unfold C_without_z, cases invC, cases reflecting_id_ℕop,
    refine invcat.mk (has_idreflect.mk _ _), apply Functor_from_C' z φ, intros x y f p,
    cases reflecting_id f p with [p1, p2],
    refine ⟨_,_⟩,
    { cases x, cases y, congruence, apply p1 },
    { cases x, cases y, esimp at *, induction p1 using eq.drec, esimp at *, apply p2}
  end

open equiv equiv.ops sigma sigma.ops

definition C_without_z_sigma_equiv {C : Category} (z : C) : C_without_z z ≃ Σ (c : C), c ≠ z :=
equiv.mk (λ c', ⟨obj c', prop c'⟩) (λc, mk c.1 c.2) begin intros, cases x, esimp, end begin intros, cases x, esimp end

definition C_without_z_is_obj_finite [instance] {n : ℕ} (z : C) [φ : objects C ≃ fin (nat.succ n)]
: objects (C_without_z z) ≃ fin n :=  (fincat.fincat_ob_remove_fin_equiv z) ∘ (C_without_z_sigma_equiv z)

end subcategory

author: annenkov

repo: two-level

save_path: github-repos/lean/annenkov-two-level


text:
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

Computational realization of filters (experimental).
-/
import order.filter.cofinite
open set filter

/-- A `cfilter α σ` is a realization of a filter (base) on `α`,
  represented by a type `σ` together with operations for the top element and
  the binary inf operation. -/
structure cfilter (α σ : Type*) [partial_order α] :=
(f : σ → α)
(pt : σ)
(inf : σ → σ → σ)
(inf_le_left : ∀ a b : σ, f (inf a b) ≤ f a)
(inf_le_right : ∀ a b : σ, f (inf a b) ≤ f b)

variables {α : Type*} {β : Type*} {σ : Type*} {τ : Type*}

namespace cfilter
section
variables [partial_order α] (F : cfilter α σ)

instance : has_coe_to_fun (cfilter α σ) (λ _, σ → α) := ⟨cfilter.f⟩

@[simp] theorem coe_mk (f pt inf h₁ h₂ a) : (@cfilter.mk α σ _ f pt inf h₁ h₂) a = f a := rfl

/-- Map a cfilter to an equivalent representation type. -/
def of_equiv (E : σ ≃ τ) : cfilter α σ → cfilter α τ
| ⟨f, p, g, h₁, h₂⟩ :=
  { f            := λ a, f (E.symm a),
    pt           := E p,
    inf          := λ a b, E (g (E.symm a) (E.symm b)),
    inf_le_left  := λ a b, by simpa using h₁ (E.symm a) (E.symm b),
    inf_le_right := λ a b, by simpa using h₂ (E.symm a) (E.symm b) }

@[simp] theorem of_equiv_val (E : σ ≃ τ) (F : cfilter α σ) (a : τ) :
  F.of_equiv E a = F (E.symm a) := by cases F; refl

end

/-- The filter represented by a `cfilter` is the collection of supersets of
  elements of the filter base. -/
def to_filter (F : cfilter (set α) σ) : filter α :=
{ sets             := {a | ∃ b, F b ⊆ a},
  univ_sets        := ⟨F.pt, subset_univ _⟩,
  sets_of_superset := λ x y ⟨b, h⟩ s, ⟨b, subset.trans h s⟩,
  inter_sets       := λ x y ⟨a, h₁⟩ ⟨b, h₂⟩, ⟨F.inf a b,
    subset_inter (subset.trans (F.inf_le_left _ _) h₁) (subset.trans (F.inf_le_right _ _) h₂)⟩ }

@[simp] theorem mem_to_filter_sets (F : cfilter (set α) σ) {a : set α} :
  a ∈ F.to_filter ↔ ∃ b, F b ⊆ a := iff.rfl

end cfilter

/-- A realizer for filter `f` is a cfilter which generates `f`. -/
structure filter.realizer (f : filter α) :=
(σ : Type*)
(F : cfilter (set α) σ)
(eq : F.to_filter = f)

protected def cfilter.to_realizer (F : cfilter (set α) σ) : F.to_filter.realizer := ⟨σ, F, rfl⟩

namespace filter.realizer

theorem mem_sets {f : filter α} (F : f.realizer) {a : set α} : a ∈ f ↔ ∃ b, F.F b ⊆ a :=
by cases F; subst f; simp

-- Used because it has better definitional equalities than the eq.rec proof
def of_eq {f g : filter α} (e : f = g) (F : f.realizer) : g.realizer :=
⟨F.σ, F.F, F.eq.trans e⟩

/-- A filter realizes itself. -/
def of_filter (f : filter α) : f.realizer := ⟨f.sets,
{ f            := subtype.val,
  pt           := ⟨univ, univ_mem⟩,
  inf          := λ ⟨x, h₁⟩ ⟨y, h₂⟩, ⟨_, inter_mem h₁ h₂⟩,
  inf_le_left  := λ ⟨x, h₁⟩ ⟨y, h₂⟩, inter_subset_left x y,
  inf_le_right := λ ⟨x, h₁⟩ ⟨y, h₂⟩, inter_subset_right x y },
filter_eq $ set.ext $ λ x, set_coe.exists.trans exists_mem_subset_iff⟩

/-- Transfer a filter realizer to another realizer on a different base type. -/
def of_equiv {f : filter α} (F : f.realizer) (E : F.σ ≃ τ) : f.realizer :=
⟨τ, F.F.of_equiv E, by refine eq.trans _ F.eq; exact filter_eq (set.ext $ λ x,
⟨λ ⟨s, h⟩, ⟨E.symm s, by simpa using h⟩, λ ⟨t, h⟩, ⟨E t, by simp [h]⟩⟩)⟩

@[simp] theorem of_equiv_σ {f : filter α} (F : f.realizer) (E : F.σ ≃ τ) :
  (F.of_equiv E).σ = τ := rfl
@[simp]

/-- `unit` is a realizer for the principal filter -/
protected def principal (s : set α) : (principal s).realizer := ⟨unit,
{ f            := λ _, s,
  pt           := (),
  inf          := λ _ _, (),
  inf_le_left  := λ _ _, le_refl _,
  inf_le_right := λ _ _, le_refl _ },
filter_eq $ set.ext $ λ x,
⟨λ ⟨_, s⟩, s, λ h, ⟨(), h⟩⟩⟩

@[simp] theorem principal_σ (s : set α) : (realizer.principal s).σ = unit := rfl
@[simp] theorem principal_F (s : set α) (u : unit) : (realizer.principal s).F u = s := rfl

/-- `unit` is a realizer for the top filter -/
protected def top : (⊤ : filter α).realizer :=
(realizer.principal _).of_eq principal_univ

@[simp] theorem top_σ : (@realizer.top α).σ = unit := rfl
@[simp] theorem top_F (u : unit) : (@realizer.top α).F u = univ := rfl

/-- `unit` is a realizer for the bottom filter -/
protected def bot : (⊥ : filter α).realizer :=
(realizer.principal _).of_eq principal_empty

@[simp] theorem bot_σ : (@realizer.bot α).σ = unit := rfl
@[simp] theorem bot_F (u : unit) : (@realizer.bot α).F u = ∅ := rfl

/-- Construct a realizer for `map m f` given a realizer for `f` -/
protected def map (m : α → β) {f : filter α} (F : f.realizer) : (map m f).realizer := ⟨F.σ,
{ f            := λ s, image m (F.F s),
  pt           := F.F.pt,
  inf          := F.F.inf,
  inf_le_left  := λ a b, image_subset _ (F.F.inf_le_left _ _),
  inf_le_right := λ a b, image_subset _ (F.F.inf_le_right _ _) },
filter_eq $ set.ext $ λ x, by simp [cfilter.to_filter]; rw F.mem_sets; refl ⟩

@[simp] theorem map_σ (m : α → β) {f : filter α} (F : f.realizer) : (F.map m).σ = F.σ := rfl
@[simp] theorem map_F (m : α → β) {f : filter α} (F : f.realizer) (s) :
  (F.map m).F s = image m (F.F s) := rfl

/-- Construct a realizer for `comap m f` given a realizer for `f` -/
protected def comap (m : α → β) {f : filter β} (F : f.realizer) : (comap m f).realizer := ⟨F.σ,
{ f            := λ s, preimage m (F.F s),
  pt           := F.F.pt,
  inf          := F.F.inf,
  inf_le_left  := λ a b, preimage_mono (F.F.inf_le_left _ _),
  inf_le_right := λ a b, preimage_mono (F.F.inf_le_right _ _) },
filter_eq $ set.ext $ λ x, by cases F; subst f; simp [cfilter.to_filter, mem_comap]; exact
⟨λ ⟨s, h⟩, ⟨_, ⟨s, subset.refl _⟩, h⟩,
 λ ⟨y, ⟨s, h⟩, h₂⟩, ⟨s, subset.trans (preimage_mono h) h₂⟩⟩⟩

/-- Construct a realizer for the sup of two filters -/
protected def sup {f g : filter α} (F : f.realizer) (G : g.realizer) :
  (f ⊔ g).realizer := ⟨F.σ × G.σ,
{ f            := λ ⟨s, t⟩, F.F s ∪ G.F t,
  pt           := (F.F.pt, G.F.pt),
  inf          := λ ⟨a, a'⟩ ⟨b, b'⟩, (F.F.inf a b, G.F.inf a' b'),
  inf_le_left  := λ ⟨a, a'⟩ ⟨b, b'⟩, union_subset_union (F.F.inf_le_left _ _) (G.F.inf_le_left _ _),
  inf_le_right := λ ⟨a, a'⟩ ⟨b, b'⟩, union_subset_union (F.F.inf_le_right _ _)
                    (G.F.inf_le_right _ _) },
filter_eq $ set.ext $ λ x, by cases F; cases G; substs f g; simp [cfilter.to_filter]; exact
⟨λ ⟨s, t, h⟩, ⟨⟨s, subset.trans (subset_union_left _ _) h⟩,
               ⟨t, subset.trans (subset_union_right _ _) h⟩⟩,
 λ ⟨⟨s, h₁⟩, ⟨t, h₂⟩⟩, ⟨s, t, union_subset h₁ h₂⟩⟩⟩

/-- Construct a realizer for the inf of two filters -/
protected def inf {f g : filter α} (F : f.realizer) (G : g.realizer) :
  (f ⊓ g).realizer := ⟨F.σ × G.σ,
{ f            := λ ⟨s, t⟩, F.F s ∩ G.F t,
  pt           := (F.F.pt, G.F.pt),
  inf          := λ ⟨a, a'⟩ ⟨b, b'⟩, (F.F.inf a b, G.F.inf a' b'),
  inf_le_left  := λ ⟨a, a'⟩ ⟨b, b'⟩, inter_subset_inter (F.F.inf_le_left _ _) (G.F.inf_le_left _ _),
  inf_le_right := λ ⟨a, a'⟩ ⟨b, b'⟩, inter_subset_inter (F.F.inf_le_right _ _)
                    (G.F.inf_le_right _ _) },
 begin
   ext x,
   cases F; cases G; substs f g; simp [cfilter.to_filter],
   split,
   { rintro ⟨s : F_σ, t : G_σ, h⟩,
     apply mem_inf_of_inter _ _ h,
     use s,
     use t, },
   { rintros ⟨s, ⟨a, ha⟩, t, ⟨b, hb⟩, rfl⟩,
     exact ⟨a, b, inter_subset_inter ha hb⟩ }
 end⟩

/-- Construct a realizer for the cofinite filter -/
protected def cofinite [decidable_eq α] : (@cofinite α).realizer := ⟨finset α,
{ f            := λ s, {a | a ∉ s},
  pt           := ∅,
  inf          := (∪),
  inf_le_left  := λ s t a, mt (finset.mem_union_left _),
  inf_le_right := λ s t a, mt (finset.mem_union_right _) },
filter_eq $ set.ext $ λ x,
⟨λ ⟨s, h⟩, s.finite_to_set.subset (compl_subset_comm.1 h),
 λ ⟨fs⟩, by exactI ⟨xᶜ.to_finset, λ a (h : a ∉ xᶜ.to_finset),
  classical.by_contradiction $ λ h', h (mem_to_finset.2 h')⟩⟩⟩

/-- Construct a realizer for filter bind -/
protected def bind {f : filter α} {m : α → filter β} (F : f.realizer) (G : ∀ i, (m i).realizer) :
  (f.bind m).realizer :=
⟨Σ s : F.σ, Π i ∈ F.F s, (G i).σ,
{ f            := λ ⟨s, f⟩, ⋃ i ∈ F.F s, (G i).F (f i H),
  pt           := ⟨F.F.pt, λ i H, (G i).F.pt⟩,
  inf          := λ ⟨a, f⟩ ⟨b, f'⟩, ⟨F.F.inf a b, λ i h,
    (G i).F.inf (f i (F.F.inf_le_left _ _ h)) (f' i (F.F.inf_le_right _ _ h))⟩,
  inf_le_left  := λ ⟨a, f⟩ ⟨b, f'⟩ x,
    show (x ∈ ⋃ (i : α) (H : i ∈ F.F (F.F.inf a b)), _) →
          x ∈ ⋃ i (H : i ∈ F.F a), ((G i).F) (f i H), by simp; exact
    λ i h₁ h₂, ⟨i, F.F.inf_le_left _ _ h₁, (G i).F.inf_le_left _ _ h₂⟩,
  inf_le_right := λ ⟨a, f⟩ ⟨b, f'⟩ x,
    show (x ∈ ⋃ (i : α) (H : i ∈ F.F (F.F.inf a b)), _) →
          x ∈ ⋃ i (H : i ∈ F.F b), ((G i).F) (f' i H), by simp; exact
    λ i h₁ h₂, ⟨i, F.F.inf_le_right _ _ h₁, (G i).F.inf_le_right _ _ h₂⟩ },
filter_eq $ set.ext $ λ x,
by cases F with _ F _; subst f; simp [cfilter.to_filter, mem_bind]; exact
⟨λ ⟨s, f, h⟩, ⟨F s, ⟨s, subset.refl _⟩, λ i H, (G i).mem_sets.2
   ⟨f i H, λ a h', h ⟨_, ⟨i, rfl⟩, _, ⟨H, rfl⟩, h'⟩⟩⟩,
 λ ⟨y, ⟨s, h⟩, f⟩,
  let ⟨f', h'⟩ := classical.axiom_of_choice (λ i:F s, (G i).mem_sets.1 (f i (h i.2))) in
  ⟨s, λ i h, f' ⟨i, h⟩, λ a ⟨_, ⟨i, rfl⟩, _, ⟨H, rfl⟩, m⟩, h' ⟨_, H⟩ m⟩⟩⟩

/-- Construct a realizer for indexed supremum -/
protected def Sup {f : α → filter β} (F : ∀ i, (f i).realizer) : (⨆ i, f i).realizer :=
let F' : (⨆ i, f i).realizer :=
  ((realizer.bind realizer.top F).of_eq $
    filter_eq $ set.ext $ by simp [filter.bind, eq_univ_iff_forall, supr_sets_eq]) in
F'.of_equiv $ show (Σ u:unit, Π (i : α), true → (F i).σ) ≃ Π i, (F i).σ, from
⟨λ⟨_,f⟩ i, f i ⟨⟩, λ f, ⟨(), λ i _, f i⟩,
 λ ⟨⟨⟩, f⟩, by dsimp; congr; simp, λ f, rfl⟩

/-- Construct a realizer for the product of filters -/
protected def prod {f g : filter α} (F : f.realizer) (G : g.realizer) : (f.prod g).realizer :=
(F.comap _).inf (G.comap _)

theorem le_iff {f g : filter α} (F : f.realizer) (G : g.realizer) :
  f ≤ g ↔ ∀ b : G.σ, ∃ a : F.σ, F.F a ≤ G.F b :=
⟨λ H t, F.mem_sets.1 (H (G.mem_sets.2 ⟨t, subset.refl _⟩)),
 λ H x h, F.mem_sets.2 $
   let ⟨s, h₁⟩ := G.mem_sets.1 h, ⟨t, h₂⟩ := H s in ⟨t, subset.trans h₂ h₁⟩⟩

theorem tendsto_iff (f : α → β) {l₁ : filter α} {l₂ : filter β} (L₁ : l₁.realizer)
  (L₂ : l₂.realizer) :
  tendsto f l₁ l₂ ↔ ∀ b, ∃ a, ∀ x ∈ L₁.F a, f x ∈ L₂.F b :=
(le_iff (L₁.map f) L₂).trans $ forall_congr $ λ b, exists_congr $ λ a, image_subset_iff

theorem ne_bot_iff {f : filter α} (F : f.realizer) :
  f ≠ ⊥ ↔ ∀ a : F.σ, (F.F a).nonempty :=
begin
  classical,
  rw [not_iff_comm, ← le_bot_iff, F.le_iff realizer.bot, not_forall],
  simp only [set.not_nonempty_iff_eq_empty],
  exact ⟨λ ⟨x, e⟩ _, ⟨x, le_of_eq e⟩,
    λ h, let ⟨x, h⟩ := h () in ⟨x, le_bot_iff.1 h⟩⟩
end

end filter.realizer

author: jjaassoonn


text:
import tactic.converter.interactive
import topology.algebra.ring

import for_mathlib.data.set.basic
import for_mathlib.topology
import for_mathlib.rings

open topological_space

namespace topological_space
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
variables [topological_space β] [topological_space δ]

/-- A product of induced topologies is induced by the product map -/
lemma prod_induced_induced (f : α → β) (g : γ → δ) :
  @prod.topological_space _ _ (induced f ‹_›) (induced g ‹_›) = induced (λ p, (f p.1, g p.2)) prod.topological_space :=
begin
  letI := induced f ‹_›, letI := induced g ‹_›,
  set fxg := (λ p : α × γ, (f p.1, g p.2)),
  have key1 : f ∘ (prod.fst : α × γ → α) = (prod.fst : β × δ → β) ∘ fxg, from rfl,
  have key2 : g ∘ (prod.snd : α × γ → γ) = (prod.snd : β × δ → δ) ∘ fxg, from rfl,
  unfold prod.topological_space, -- product topology is a sup of induced topologies
  -- so let's be functorial
  conv_lhs {
    rw [induced_compose, induced_compose, key1, key2],
    congr, rw ← induced_compose, skip, rw ← induced_compose, },
  rw induced_inf
end
end topological_space

@[simp]
lemma division_ring.inv_val_eq_inv {α : Type*} [division_ring α] (x : units α) :(x : α)⁻¹ = x.inv :=
begin
  rw (show x.inv = (x⁻¹ : units α), from rfl),
  rw ←one_div_eq_inv,
  symmetry,
  apply eq_one_div_of_mul_eq_one,
  exact x.mul_inv
end

namespace topological_ring
open topological_space function
variables (R : Type*) [ring R]

lemma units.coe_inj : injective (coe : units R → R) :=
λ x y h, units.ext h

variables  [topological_space R]

-- This is not a global instance. Instead we introduced a class `induced_units` asserting
-- something equivalent to this construction holds
def topological_space_units : topological_space (units R) := induced units.val ‹_›

class induced_units (R : Type*) [ring R] [topological_space R] [t : topological_space $ units R] :
  Prop :=
(top_eq : t = induced (coe : units R → R) ‹_›)

variables [ring R] [topological_space R] [topological_space $ units R]

lemma induced_units.continuous_coe [induced_units R] : continuous (coe : units R → R) :=
(induced_units.top_eq R).symm ▸ continuous_induced_dom

lemma units_embedding [topological_space $ units R] [induced_units R] :
  embedding (units.val : units R → R) :=
{ induced := induced_units.top_eq R,
  inj := units.coe_inj _ }

instance top_monoid_units [topological_ring R] [topological_space $ units R] [induced_units R] :
  topological_monoid (units R) :=
⟨begin
  let mulR := (λ (p : R × R), p.1*p.2),
  let mulRx := (λ (p : units R × units R), p.1*p.2),
  have key : coe ∘ mulRx = mulR ∘ (λ p, (p.1.val, p.2.val)), from rfl,
  rw [continuous_iff_le_induced, induced_units.top_eq R, prod_induced_induced,
      induced_compose, key, ← induced_compose],
  apply induced_mono,
  rw ← continuous_iff_le_induced,
  exact continuous_mul,
end⟩
end topological_ring

variables (K : Type*) [division_ring K] [topological_space K]

/-- A topological division ring is a division ring with a topology where all operations are
    continuous, including inversion. -/
class topological_division_ring extends topological_ring K : Prop :=
(continuous_inv : ∀ x : K, x ≠ 0 → continuous_at (λ x : K, x⁻¹ : K → K) x)

namespace topological_division_ring
open filter set
/-
In this section, we show that units of a topological division ring endowed with the
induced topology form a topological group. These are not global instances because
one could want another topology on units. To turn on this feature, use:

```lean
local attribute [instance]
topological_ring.topological_space_units topological_division_ring.units_top_group
```
-/

variables [topological_division_ring K]

local attribute [instance] topological_ring.topological_space_units

def induced_units : topological_ring.induced_units K := ⟨rfl⟩
local attribute [instance] induced_units

def units_top_group : topological_group (units K) :=
{ continuous_inv := begin
     have : (units.val : units K → K) ∘ (λx, x⁻¹ : units K → units K) = (λx, x⁻¹ : K → K) ∘ (coe : units K → K),
      by { ext, apply units.inv_eq_inv },
     rw continuous_iff_continuous_at,
     intros x,
     rw [continuous_at, nhds_induced, nhds_induced, tendsto_iff_comap, comap_comm this],
     apply comap_mono,
     rw ← tendsto_iff_comap,
     convert topological_division_ring.continuous_inv x.val x.ne_zero,
     exact x.inv_eq_inv
   end ,
  ..topological_ring.top_monoid_units K}

local attribute [instance] units_top_group

lemma continuous_units_inv : continuous (λ x, x.inv : units K → K) :=
begin
  change continuous (coe ∘ (λ x, x⁻¹ : units K → units K)),
  refine (topological_ring.induced_units.continuous_coe K).comp _,
  exact _root_.continuous_inv,
end
end topological_division_ring

repo: lean-perfectoid-spaces


text:
import topology.subset_properties -- compactness of subsets of top spaces
/-!

# Topology, the traditional way

Let's do some topology! In this file we prove that

* the continuous image of a compact space is compact;
* A closed subset of a compact space is compact.

## Details

In fact we do a little more than this (but it's basically equivalent).
We do not work with compact topological spaces, we work with compact
subsets of topological spaces. What we will actually prove is this:

* If `f : X → Y` is a continuous map, and `S : set X` is a compact subset
(with the subspace topology), then `f '' S` (the image of `S` under `f`) is
compact (with the subspace topology).

* If `X` is a topological space, if `S` is a compact subset and if `C` is
a closed subset, then `S ∩ C` is a compact subset.

The original results are just the special case where `S` is `univ : set X`.
-/

-- Let X and Y be topological spaces, and let `f : X → Y` be a map.
variables (X Y : Type) [topological_space X] [topological_space Y] (f : X → Y)

-- I don't want to be typing `set.this` and `set.that` so let's open
-- the `set` namespace once and for all.
open set

/-!

## Compact subspaces

`is_compact` is a predicate on `set X`, if `X` is a topological space.
In other words, `is_compact X` doesn't make sense, but if `S : set X`
then `is_compact S` does. The actual definition in mathlib involves
filters! But it is a theorem in mathlib that `is_compact S` is true if and only
if every collection of open subsets of `X` whose union contains `S`
has a finite subcollection whose union contains `S`. Unfortunately,
mathlib's version of this, `compact_iff_finite_subcover`, uses a slightly
wacky notion of finite subcover involving `finset X`, the type of finite
subsets of `X` (a completely different type to the type `set X`!).
We prove an easier-to-use version involving `finite Z`, the predicate
saying that `Z : set ι` is finite. You can ignore this proof.
-/

lemma compact_iff_finite_subcover'
  {α : Type} [topological_space α] {S : set α} :
  is_compact S ↔ (∀ {ι : Type} (U : ι → (set α)), (∀ i, is_open (U i)) →
    S ⊆ (⋃ i, U i) → (∃ (t : set ι), t.finite ∧ S ⊆ (⋃ i ∈ t, U i))) :=
begin
  rw compact_iff_finite_subcover,
  split,
  { intros hs ι U hU hsU,
    cases hs U hU hsU with F hF,
    use [(↑F : set ι), finset.finite_to_set F],
    exact hF },
  { intros hs ι U hU hsU,
    rcases hs U hU hsU with ⟨F, hFfin, hF⟩,
    use hFfin.to_finset,
    convert hF,
    ext,
    simp }
end

/-!

## Continuous image of compact is compact

I would start with `rw compact_iff_finite_subcover' at hS ⊢,`

The proof that I recommend formalising is this. Say `S` is a compact
subset of `X`, and `f : X → Y` is continuous. We want to prove that
every cover of `f '' S` by open subsets of `Y` has a finite subcover.
So let's cover `f '' S` with opens `U i : set Y`, for `i : ι` and `ι` an index type.
Pull these opens back to `V i : set X` and observe that they cover `S`.
Choose a finite subcover corresponding to some `F : set ι` such that `F` is finite
(Lean writes this `h : F.finite`) and then check that the corresponding cover
of `f '' S` by the `U i` with `i ∈ F` is a finite subcover.

Good luck! Please ask questions (or DM me on discord if you don't want to
ask publically). Also feel free to DM me if you manage to do it!

Useful theorems:

`continuous.is_open_preimage` -- preimage of an open set under a
continuous map is open.

`is_open_compl_iff` -- complement `Sᶜ` of `S` is open iff `S` is closed.

## Some useful tactics:

### `specialize`

`specialize` can be used with `_`. If you have a hypothesis

`hS : ∀ {ι : Type} (U : ι → set X), (∀ (i : ι), is_open (U i)) → ...`

and `U : ι → set X`, then

`specialize hS U` will change `hS` to

`hS : (∀ (i : ι), is_open (U i)) → ...`

But what if you now want to prove `∀ i, is_open (U i)` so you can feed it
into `hS` as an input? You can put

`specialize hS _`

and then that goal will pop out. Unfortunately it pops out _under_ the
current goal! You can swap two goals with the `swap` tactic though :-)

### `change`

If your goal is `⊢ P` and `P` is definitionally equal to `Q`, then you
can write `change Q` and the goal will change to `Q`. Sometimes useful
because rewriting works up to syntactic equality, which is stronger
than definitional equality.

### `rwa`

`rwa h` just means `rw h, assumption`

### `contradiction`

If you have `h1 : P` and `h2 : ¬ P` as hypotheses, then you can prove any goal with
the `contradiction` tactic, which just does `exfalso, apply h2, exact h1`.

### `set`

Note : The `set` tactic is totally unrelated to the `set X` type of subsets of `X`!

The `set` tactic can be used to define things. For example
`set T := f '' S with hT_def,` will define `T` to be `f '' S`
and will also define `hT_def : T = f '' S`.

-/

lemma image_compact_of_compact (hf : continuous f) (S : set X) (hS : is_compact S) :
  is_compact (f '' S) :=
begin
  -- proof I recommend:
  -- (1) cover f''s with opens. Want finite subcover
  -- (2) pull back
  -- (3) finite subcover
  -- (4) push forward

  -- start by changing `is_compact` to something we can work with.
  rw compact_iff_finite_subcover' at hS ⊢,
  -- Define `T` to be `f '' S` -- why not?
  set T := f '' S with hT_def,
  -- Now `T = f '' S` and `hT_def` tells us that.
  -- Note that `set T := ...` is about the *tactic* `set`.

  -- OK let's go.
  sorry
end

/-

## Closed subset of a compact is compact.

This is a little trickier because given `U : ι → set X` we need
to produce `V : option ι → set X` at some point in the below
proof. We can make it using `option.rec`.

If `S` is compact and `C` is closed then we want to prove `S ∩ C` is compact.

Start with `rw compact_iff_finite_subcover' at hS ⊢,`.

Then given a cover `U : ι → set X`, define
`V : option ι → set X` like this:

`let V : option ι → set X := λ x, option.rec Cᶜ U x,`

For finiteness, if you have `F : set (option ι)` and `hF : F.finite`,
and you want `(some ⁻¹' F).finite`, then you can apply
`set.finite.preimage` and use `option.some_inj` to deal with the
injectivity.
-/
lemma closed_of_compact (S : set X) (hS : is_compact S)
  (C : set X) (hC : is_closed C) : is_compact (S ∩ C) :=
begin
  sorry,
end

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2022 Riccardo Brasca. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Riccardo Brasca
-/

import ring_theory.eisenstein_criterion
import ring_theory.polynomial.scale_roots

/-!
# Eisenstein polynomials
Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]` is
*Eisenstein at `𝓟`* if `f.leading_coeff ∉ 𝓟`, `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟` and
`f.coeff 0 ∉ 𝓟 ^ 2`. In this file we gather miscellaneous results about Eisenstein polynomials.

## Main definitions
* `polynomial.is_eisenstein_at f 𝓟`: the property of being Eisenstein at `𝓟`.

## Main results
* `polynomial.is_eisenstein_at.irreducible`: if a primitive `f` satisfies `f.is_eisenstein_at 𝓟`,
  where `𝓟.is_prime`, then `f` is irreducible.

## Implementation details
We also define a notion `is_weakly_eisenstein_at` requiring only that
`∀ n < f.nat_degree → f.coeff n ∈ 𝓟`. This makes certain results slightly more general and it is
useful since it is sometimes better behaved (for example it is stable under `polynomial.map`).

-/

universes u v w z

variables {R : Type u}

open ideal algebra finset

open_locale big_operators polynomial

namespace polynomial

/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
is *weakly Eisenstein at `𝓟`* if `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟`. -/
@[mk_iff] structure is_weakly_eisenstein_at [comm_semiring R] (f : R[X]) (𝓟 : ideal R) :
  Prop := (mem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟)

/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
is *Eisenstein at `𝓟`* if `f.leading_coeff ∉ 𝓟`, `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟` and
`f.coeff 0 ∉ 𝓟 ^ 2`. -/
@[mk_iff] structure is_eisenstein_at [comm_semiring R] (f : R[X]) (𝓟 : ideal R) : Prop :=
(leading : f.leading_coeff ∉ 𝓟)
(mem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟)
(not_mem : f.coeff 0 ∉ 𝓟 ^ 2)

namespace is_weakly_eisenstein_at

section comm_semiring

variables [comm_semiring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at 𝓟)

include hf

lemma map {A : Type v} [comm_ring A] (φ : R →+* A) : (f.map φ).is_weakly_eisenstein_at (𝓟.map φ) :=
begin
  refine (is_weakly_eisenstein_at_iff _ _).2 (λ n hn, _),
  rw [coeff_map],
  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (nat_degree_map_le _ _)))
end

end comm_semiring

section comm_ring

variables [comm_ring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at 𝓟)
variables {S : Type v} [comm_ring S] [algebra R S]

section principal

variable {p : R}

local notation `P` := submodule.span R {p}

lemma exists_mem_adjoin_mul_eq_pow_nat_degree {x : S} (hx : aeval x f = 0)
  (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) : ∃ y ∈ adjoin R ({x} : set S),
  (algebra_map R S) p * y = x ^ (f.map (algebra_map R S)).nat_degree :=
begin
  rw [aeval_def, polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one,
    sum_insert not_mem_range_self, sum_range, (hmo.map
    (algebra_map R S)).coeff_nat_degree, one_mul] at hx,
  replace hx := eq_neg_of_add_eq_zero_left hx,
  have : ∀ n < f.nat_degree, p ∣ f.coeff n,
  { intros n hn,
    refine mem_span_singleton.1 (by simpa using hf.mem hn) },
  choose! φ hφ using this,
  conv_rhs at hx { congr, congr, skip, funext,
    rw [fin.coe_eq_val, coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (nat_degree_map_le _ _)),
      ring_hom.map_mul, mul_assoc] },
  rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc],
  refine ⟨-1 * ∑ (i : fin (f.map (algebra_map R S)).nat_degree),
    (algebra_map R S) (φ i.1) * x ^ i.1, _, rfl⟩,
  exact subalgebra.mul_mem _ (subalgebra.neg_mem _ (subalgebra.one_mem _))
    (subalgebra.sum_mem _ (λ i hi, subalgebra.mul_mem _ (subalgebra.algebra_map_mem _ _)
    (subalgebra.pow_mem _ (subset_adjoin (set.mem_singleton x)) _)))
end

lemma exists_mem_adjoin_mul_eq_pow_nat_degree_le {x : S} (hx : aeval x f = 0)
  (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) :
  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i →
  ∃ y ∈ adjoin R ({x} : set S), (algebra_map R S) p * y = x ^ i :=
begin
  intros i hi,
  obtain ⟨k, hk⟩ := exists_add_of_le hi,
  rw [hk, pow_add],
  obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_nat_degree hx hmo hf,
  refine ⟨y * x ^ k, _, _⟩,
  { exact subalgebra.mul_mem _ hy (subalgebra.pow_mem _  (subset_adjoin (set.mem_singleton x)) _) },
  { rw [← mul_assoc _ y, H] }
end

end principal

include hf

lemma pow_nat_degree_le_of_root_of_monic_mem {x : R} (hroot : is_root f x) (hmo : f.monic) :
  ∀ i, f.nat_degree ≤ i → x ^ i ∈ 𝓟 :=
begin
  intros i hi,
  obtain ⟨k, hk⟩ := exists_add_of_le hi,
  rw [hk, pow_add],
  suffices : x ^ f.nat_degree ∈ 𝓟,
  { exact mul_mem_right (x ^ k) 𝓟 this },
  rw [is_root.def, eval_eq_sum_range, finset.range_add_one, finset.sum_insert
    finset.not_mem_range_self, finset.sum_range, hmo.coeff_nat_degree, one_mul] at hroot,
  rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff],
  refine submodule.sum_mem _ (λ i hi,  mul_mem_right _ _ (hf.mem (fin.is_lt i)))
end

lemma pow_nat_degree_le_of_aeval_zero_of_monic_mem_map {x : S} (hx : aeval x f = 0)
  (hmo : f.monic) :
  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i → x ^ i ∈ 𝓟.map (algebra_map R S) :=
begin
  suffices : x ^ (f.map (algebra_map R S)).nat_degree ∈ 𝓟.map (algebra_map R S),
  { intros i hi,
    obtain ⟨k, hk⟩ := exists_add_of_le hi,
    rw [hk, pow_add],
    refine mul_mem_right _ _ this },
  rw [aeval_def, eval₂_eq_eval_map, ← is_root.def] at hx,
  refine pow_nat_degree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
end

end comm_ring

end is_weakly_eisenstein_at

section scale_roots

variables {A : Type*} [comm_ring R] [comm_ring A]

lemma scale_roots.is_weakly_eisenstein_at (p : R[X]) {x : R}
  {P : ideal R} (hP : x ∈ P) : (scale_roots p x).is_weakly_eisenstein_at P :=
begin
  refine ⟨λ i hi, _⟩,
  rw coeff_scale_roots,
  rw [nat_degree_scale_roots, ← tsub_pos_iff_lt] at hi,
  exact ideal.mul_mem_left _ _ (ideal.pow_mem_of_mem P hP _ hi)
end

lemma dvd_pow_nat_degree_of_eval₂_eq_zero {f : R →+* A}
  (hf : function.injective f) {p : R[X]} (hp : p.monic) (x y : R) (z : A)
  (h : p.eval₂ f z = 0) (hz : f x * z = f y) : x ∣ y ^ p.nat_degree :=
begin
  rw [← nat_degree_scale_roots p x, ← ideal.mem_span_singleton],
  refine (scale_roots.is_weakly_eisenstein_at _ (ideal.mem_span_singleton.mpr $ dvd_refl x))
    .pow_nat_degree_le_of_root_of_monic_mem _ ((monic_scale_roots_iff x).mpr hp) _ le_rfl,
  rw injective_iff_map_eq_zero' at hf,
  have := scale_roots_eval₂_eq_zero f h,
  rwa [hz, polynomial.eval₂_at_apply, hf] at this
end

end scale_roots

namespace is_eisenstein_at

section comm_semiring

variables [comm_semiring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_eisenstein_at 𝓟)

lemma _root_.polynomial.monic.leading_coeff_not_mem (hf : f.monic) (h : 𝓟 ≠ ⊤) :
  ¬f.leading_coeff ∈ 𝓟 :=
hf.leading_coeff.symm ▸ (ideal.ne_top_iff_one _).1 h

lemma _root_.polynomial.monic.is_eisenstein_at_of_mem_of_not_mem (hf : f.monic) (h : 𝓟 ≠ ⊤)
  (hmem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟) (hnot_mem : f.coeff 0 ∉ 𝓟 ^ 2) :
  f.is_eisenstein_at 𝓟 :=
{ leading := hf.leading_coeff_not_mem h,
  mem := λ n hn, hmem hn,
  not_mem := hnot_mem }

include hf

lemma is_weakly_eisenstein_at : is_weakly_eisenstein_at f 𝓟 := ⟨λ _, hf.mem⟩

lemma coeff_mem {n : ℕ} (hn : n ≠ f.nat_degree) : f.coeff n ∈ 𝓟 :=
begin
  cases ne_iff_lt_or_gt.1 hn,
  { exact hf.mem h },
  { rw [coeff_eq_zero_of_nat_degree_lt h],
    exact ideal.zero_mem _}
end

end comm_semiring

section is_domain

variables [comm_ring R] [is_domain R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_eisenstein_at 𝓟)

/-- If a primitive `f` satisfies `f.is_eisenstein_at 𝓟`, where `𝓟.is_prime`, then `f` is
irreducible. -/
lemma irreducible (hprime : 𝓟.is_prime) (hu : f.is_primitive)
  (hfd0 : 0 < f.nat_degree) : irreducible f :=
irreducible_of_eisenstein_criterion hprime hf.leading (λ n hn, hf.mem (coe_lt_degree.1 hn))
  (nat_degree_pos_iff_degree_pos.1 hfd0) hf.not_mem hu

end is_domain

end is_eisenstein_at

end polynomial

repo: mathlib


text:
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import category_theory.limits.has_limits
import category_theory.products.basic
import category_theory.currying

/-!
# A Fubini theorem for categorical limits

We prove that $lim_{J × K} G = lim_J (lim_K G(j, -))$ for a functor `G : J × K ⥤ C`,
when all the appropriate limits exist.

We begin working with a functor `F : J ⥤ K ⥤ C`. We'll write `G : J × K ⥤ C` for the associated
"uncurried" functor.

In the first part, given a coherent family `D` of limit cones over the functors `F.obj j`,
and a cone `c` over `G`, we construct a cone over the cone points of `D`.
We then show that if `c` is a limit cone, the constructed cone is also a limit cone.

In the second part, we state the Fubini theorem in the setting where limits are
provided by suitable `has_limit` classes.

We construct
`limit_uncurry_iso_limit_comp_lim F : limit (uncurry.obj F) ≅ limit (F ⋙ lim)`
and give simp lemmas characterising it.
For convenience, we also provide
`limit_iso_limit_curry_comp_lim G : limit G ≅ limit ((curry.obj G) ⋙ lim)`
in terms of the uncurried functor.

## Future work

The dual statement.
-/

universes v u

open category_theory

namespace category_theory.limits

variables {J K : Type v} [small_category J] [small_category K]
variables {C : Type u} [category.{v} C]

variables (F : J ⥤ K ⥤ C)

/--
A structure carrying a diagram of cones over the functors `F.obj j`.
-/
-- We could try introducing a "dependent functor type" to handle this?
structure diagram_of_cones :=
(obj : Π j : J, cone (F.obj j))
(map : Π {j j' : J} (f : j ⟶ j'), (cones.postcompose (F.map f)).obj (obj j) ⟶ obj j')
(id : ∀ j : J, (map (𝟙 j)).hom = 𝟙 _ . obviously)
(comp : ∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
  (map (f ≫ g)).hom = (map f).hom ≫ (map g).hom . obviously)

variables {F}

/--
Extract the functor `J ⥤ C` consisting of the cone points and the maps between them,
from a `diagram_of_cones`.
-/
@[simps]
def diagram_of_cones.cone_points (D : diagram_of_cones F) :
  J ⥤ C :=
{ obj := λ j, (D.obj j).X,
  map := λ j j' f, (D.map f).hom,
  map_id' := λ j, D.id j,
  map_comp' := λ j₁ j₂ j₃ f g, D.comp f g, }

/--
Given a diagram `D` of limit cones over the `F.obj j`, and a cone over `uncurry.obj F`,
we can construct a cone over the diagram consisting of the cone points from `D`.
-/
@[simps]
def cone_of_cone_uncurry
  {D : diagram_of_cones F} (Q : Π j, is_limit (D.obj j))
  (c : cone (uncurry.obj F)) :
  cone (D.cone_points) :=
{ X := c.X,
  π :=
  { app := λ j, (Q j).lift
    { X := c.X,
      π :=
      { app := λ k, c.π.app (j, k),
        naturality' := λ k k' f,
        begin
          dsimp, simp only [category.id_comp],
          have := @nat_trans.naturality _ _ _ _ _ _ c.π (j, k) (j, k') (𝟙 j, f),
          dsimp at this,
          simp only [category.id_comp, category_theory.functor.map_id, nat_trans.id_app] at this,
          exact this,
        end } },
    naturality' := λ j j' f, (Q j').hom_ext
    begin
      dsimp,
      intro k,
      simp only [limits.cone_morphism.w, limits.cones.postcompose_obj_π, limits.is_limit.fac_assoc,
        limits.is_limit.fac, nat_trans.comp_app, category.id_comp, category.assoc],
      have := @nat_trans.naturality _ _ _ _ _ _ c.π (j, k) (j', k) (f, 𝟙 k),
      dsimp at this,
      simp only [category.id_comp, category.comp_id,
        category_theory.functor.map_id, nat_trans.id_app] at this,
      exact this,
    end, } }.

/--
`cone_of_cone_uncurry Q c` is a limit cone when `c` is a limit cone.`
-/
def cone_of_cone_uncurry_is_limit
  {D : diagram_of_cones F} (Q : Π j, is_limit (D.obj j))
  {c : cone (uncurry.obj F)} (P : is_limit c) :
  is_limit (cone_of_cone_uncurry Q c) :=
{ lift := λ s, P.lift
  { X := s.X,
    π :=
    { app := λ p, s.π.app p.1 ≫ (D.obj p.1).π.app p.2,
      naturality' := λ p p' f,
      begin
        dsimp, simp only [category.id_comp, category.assoc],
        rcases p with ⟨j, k⟩,
        rcases p' with ⟨j', k'⟩,
        rcases f with ⟨fj, fk⟩,
        dsimp,
        slice_rhs 3 4 { rw ←nat_trans.naturality, },
        slice_rhs 2 3 { rw ←(D.obj j).π.naturality, },
        simp only [functor.const.obj_map, category.id_comp, category.assoc],
        have w := (D.map fj).w k',
        dsimp at w,
        rw ←w,
        have n := s.π.naturality fj,
        dsimp at n,
        simp only [category.id_comp] at n,
        rw n,
        simp,
      end, } },
  fac' := λ s j,
  begin
    apply (Q j).hom_ext,
    intro k,
    simp,
  end,
  uniq' := λ s m w,
  begin
    refine P.uniq { X := s.X, π := _, } m _,
    rintro ⟨j, k⟩,
    dsimp,
    rw [←w j],
    simp,
  end, }

section
variables (F)
variables [has_limits_of_shape K C]

/--
Given a functor `F : J ⥤ K ⥤ C`, with all needed limits,
we can construct a diagram consisting of the limit cone over each functor `F.obj j`,
and the universal cone morphisms between these.
-/
@[simps]
noncomputable def diagram_of_cones.mk_of_has_limits : diagram_of_cones F :=
{ obj := λ j, limit.cone (F.obj j),
  map := λ j j' f, { hom := lim.map (F.map f), }, }

-- Satisfying the inhabited linter.
noncomputable instance diagram_of_cones_inhabited : inhabited (diagram_of_cones F) :=
⟨diagram_of_cones.mk_of_has_limits F⟩

@[simp]
lemma diagram_of_cones.mk_of_has_limits_cone_points :
  (diagram_of_cones.mk_of_has_limits F).cone_points = (F ⋙ lim) :=
rfl

variables [has_limit (uncurry.obj F)]
variables [has_limit (F ⋙ lim)]

/--
The Fubini theorem for a functor `F : J ⥤ K ⥤ C`,
showing that the limit of `uncurry.obj F` can be computed as
the limit of the limits of the functors `F.obj j`.
-/
noncomputable def limit_uncurry_iso_limit_comp_lim : limit (uncurry.obj F) ≅ limit (F ⋙ lim) :=
begin
  let c := limit.cone (uncurry.obj F),
  let P : is_limit c := limit.is_limit _,
  let G := diagram_of_cones.mk_of_has_limits F,
  let Q : Π j, is_limit (G.obj j) := λ j, limit.is_limit _,
  have Q' := cone_of_cone_uncurry_is_limit Q P,
  have Q'' := (limit.is_limit (F ⋙ lim)),
  exact is_limit.cone_point_unique_up_to_iso Q' Q'',
end

@[simp]
lemma limit_uncurry_iso_limit_comp_lim_hom_π_π {j} {k} :
  (limit_uncurry_iso_limit_comp_lim F).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k) :=
begin
  dsimp [limit_uncurry_iso_limit_comp_lim, is_limit.cone_point_unique_up_to_iso,
    is_limit.unique_up_to_iso],
  simp,
end

@[simp]
lemma limit_uncurry_iso_limit_comp_lim_inv_π {j} {k} :
  (limit_uncurry_iso_limit_comp_lim F).inv ≫ limit.π _ (j, k) = limit.π _ j ≫ limit.π _ k :=
begin
  rw [←cancel_epi (limit_uncurry_iso_limit_comp_lim F).hom],
  simp,
end
end

section
variables (G : J × K ⥤ C)

section
variables [has_limits_of_shape K C]
variables [has_limit G]
variables [has_limit ((curry.obj G) ⋙ lim)]

/--
The Fubini theorem for a functor `G : J × K ⥤ C`,
showing that the limit of `G` can be computed as
the limit of the limits of the functors `G.obj (j, _)`.
-/
noncomputable def limit_iso_limit_curry_comp_lim : limit G ≅ limit ((curry.obj G) ⋙ lim) :=
begin
  have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unit_iso.app G,
  haveI : limits.has_limit (uncurry.obj ((@curry J _ K _ C _).obj G)) :=
    has_limit_of_iso i,
  transitivity limit (uncurry.obj ((@curry J _ K _ C _).obj G)),
  apply has_limit.iso_of_nat_iso i,
  exact limit_uncurry_iso_limit_comp_lim ((@curry J _ K _ C _).obj G),
end

@[simp, reassoc]
lemma limit_iso_limit_curry_comp_lim_hom_π_π {j} {k} :
  (limit_iso_limit_curry_comp_lim G).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k) :=
by simp [limit_iso_limit_curry_comp_lim, is_limit.cone_point_unique_up_to_iso,
  is_limit.unique_up_to_iso]

@[simp, reassoc]
lemma limit_iso_limit_curry_comp_lim_inv_π {j} {k} :
  (limit_iso_limit_curry_comp_lim G).inv ≫ limit.π _ (j, k) = limit.π _ j ≫ limit.π _ k :=
begin
  rw [←cancel_epi (limit_iso_limit_curry_comp_lim G).hom],
  simp,
end
end

section
variables [has_limits C] -- Certainly one could weaken the hypotheses here.

open category_theory.prod

/--
A variant of the Fubini theorem for a functor `G : J × K ⥤ C`,
showing that $\lim_k \lim_j G(j,k) ≅ \lim_j \lim_k G(j,k)$.
-/
noncomputable
def limit_curry_swap_comp_lim_iso_limit_curry_comp_lim :
  limit ((curry.obj (swap K J ⋙ G)) ⋙ lim) ≅ limit ((curry.obj G) ⋙ lim) :=
calc
  limit ((curry.obj (swap K J ⋙ G)) ⋙ lim)
      ≅ limit (swap K J ⋙ G) : (limit_iso_limit_curry_comp_lim _).symm
  ... ≅ limit G : has_limit.iso_of_equivalence (braiding K J) (iso.refl _)
  ... ≅ limit ((curry.obj G) ⋙ lim) : limit_iso_limit_curry_comp_lim _

@[simp]
lemma limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_hom_π_π {j} {k} :
  (limit_curry_swap_comp_lim_iso_limit_curry_comp_lim G).hom ≫ limit.π _ j ≫ limit.π _ k =
   limit.π _ k ≫ limit.π _ j :=
begin
  dsimp [limit_curry_swap_comp_lim_iso_limit_curry_comp_lim],
  simp only [iso.refl_hom, braiding_counit_iso_hom_app, limits.has_limit.iso_of_equivalence_hom_π,
    iso.refl_inv, limit_iso_limit_curry_comp_lim_hom_π_π, eq_to_iso_refl, category.assoc],
  erw [nat_trans.id_app], -- Why can't `simp` do this`?
  dsimp, simp,
end

@[simp]
lemma limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_inv_π_π {j} {k} :
  (limit_curry_swap_comp_lim_iso_limit_curry_comp_lim G).inv ≫ limit.π _ k ≫ limit.π _ j =
   limit.π _ j ≫ limit.π _ k :=
begin
  dsimp [limit_curry_swap_comp_lim_iso_limit_curry_comp_lim],
  simp only [iso.refl_hom, braiding_counit_iso_hom_app, limits.has_limit.iso_of_equivalence_inv_π,
    iso.refl_inv, limit_iso_limit_curry_comp_lim_hom_π_π, eq_to_iso_refl, category.assoc],
  erw [nat_trans.id_app], -- Why can't `simp` do this`?
  dsimp, simp,
end

end

end

end category_theory.limits


text:
/-
Copyright (c) 2021 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.basic

/-!
# Monovariance of functions

Two functions *vary together* if a strict change in the first implies a change in the second.

This is in some sense a way to say that two functions `f : ι → α`, `g : ι → β` are "monotone
together", without actually having an order on `ι`.

This condition comes up in the rearrangement inequality. See `algebra.order.rearrangement`.

## Main declarations

* `monovary f g`: `f` monovaries with `g`. If `g i < g j`, then `f i ≤ f j`.
* `antivary f g`: `f` antivaries with `g`. If `g i < g j`, then `f j ≤ f i`.
* `monovary_on f g s`: `f` monovaries with `g` on `s`.
* `monovary_on f g s`: `f` antivaries with `g` on `s`.
-/

open function set

variables {ι ι' α β γ : Type*}

section preorder
variables [preorder α] [preorder β] [preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {g' : β → γ}
  {s t : set ι}

/--  `f` monovaries with `g` if `g i < g j` implies `f i ≤ f j`. -/
def monovary (f : ι → α) (g : ι → β) : Prop := ∀ ⦃i j⦄, g i < g j → f i ≤ f j

/--  `f` antivaries with `g` if `g i < g j` implies `f j ≤ f i`. -/
def antivary (f : ι → α) (g : ι → β) : Prop := ∀ ⦃i j⦄, g i < g j → f j ≤ f i

/--  `f` monovaries with `g` on `s` if `g i < g j` implies `f i ≤ f j` for all `i, j ∈ s`. -/
def monovary_on (f : ι → α) (g : ι → β) (s : set ι) : Prop :=
∀ ⦃i⦄ (hi : i ∈ s) ⦃j⦄ (hj : j ∈ s), g i < g j → f i ≤ f j

/--  `f` antivaries with `g` on `s` if `g i < g j` implies `f j ≤ f i` for all `i, j ∈ s`. -/
def antivary_on (f : ι → α) (g : ι → β) (s : set ι) : Prop :=
∀ ⦃i⦄ (hi : i ∈ s) ⦃j⦄ (hj : j ∈ s), g i < g j → f j ≤ f i

protected lemma monovary.monovary_on (h : monovary f g) (s : set ι) : monovary_on f g s :=
λ i _ j _ hij, h hij

protected lemma antivary.antivary_on (h : antivary f g) (s : set ι) : antivary_on f g s :=
λ i _ j _ hij, h hij

@[simp] lemma monovary_on.empty : monovary_on f g ∅ := λ i, false.elim
@[simp] lemma antivary_on.empty : antivary_on f g ∅ := λ i, false.elim

@[simp] lemma monovary_on_univ : monovary_on f g univ ↔ monovary f g :=
⟨λ h i j, h trivial trivial, λ h i _ j _ hij, h hij⟩

@[simp] lemma antivary_on_univ : antivary_on f g univ ↔ antivary f g :=
⟨λ h i j, h trivial trivial, λ h i _ j _ hij, h hij⟩

protected lemma monovary_on.subset (hst : s ⊆ t) (h : monovary_on f g t) : monovary_on f g s :=
λ i hi j hj, h (hst hi) (hst hj)

protected lemma antivary_on.subset (hst : s ⊆ t) (h : antivary_on f g t) : antivary_on f g s :=
λ i hi j hj, h (hst hi) (hst hj)

lemma monovary_const_left (g : ι → β) (a : α) : monovary (const ι a) g := λ i j _, le_rfl
lemma antivary_const_left (g : ι → β) (a : α) : antivary (const ι a) g := λ i j _, le_rfl
lemma monovary_const_right (f : ι → α) (b : β) : monovary f (const ι b) := λ i j h, (h.ne rfl).elim
lemma antivary_const_right (f : ι → α) (b : β) : antivary f (const ι b) := λ i j h, (h.ne rfl).elim

lemma monovary_self (f : ι → α) : monovary f f := λ i j, le_of_lt
lemma monovary_on_self (f : ι → α) (s : set ι) : monovary_on f f s := λ i _ j _, le_of_lt

protected lemma subsingleton.monovary [subsingleton ι] (f : ι → α) (g : ι → β) : monovary f g :=
λ i j h, (ne_of_apply_ne _ h.ne $ subsingleton.elim _ _).elim

protected lemma subsingleton.antivary [subsingleton ι] (f : ι → α) (g : ι → β) : antivary f g :=
λ i j h, (ne_of_apply_ne _ h.ne $ subsingleton.elim _ _).elim

protected lemma subsingleton.monovary_on [subsingleton ι] (f : ι → α) (g : ι → β) (s : set ι) :
  monovary_on f g s :=
λ i _ j _ h, (ne_of_apply_ne _ h.ne $ subsingleton.elim _ _).elim

protected lemma subsingleton.antivary_on [subsingleton ι] (f : ι → α) (g : ι → β) (s : set ι) :
  antivary_on f g s :=
λ i _ j _ h, (ne_of_apply_ne _ h.ne $ subsingleton.elim _ _).elim

lemma monovary_on_const_left (g : ι → β) (a : α) (s : set ι) : monovary_on (const ι a) g s :=
λ i _ j _ _, le_rfl

lemma antivary_on_const_left (g : ι → β) (a : α) (s : set ι) : antivary_on (const ι a) g s :=
λ i _ j _ _, le_rfl

lemma monovary_on_const_right (f : ι → α) (b : β) (s : set ι) : monovary_on f (const ι b) s :=
λ i _ j _ h, (h.ne rfl).elim

lemma antivary_on_const_right (f : ι → α) (b : β) (s : set ι) : antivary_on f (const ι b) s :=
λ i _ j _ h, (h.ne rfl).elim

lemma monovary.comp_right (h : monovary f g) (k : ι' → ι) : monovary (f ∘ k) (g ∘ k) :=
λ i j hij, h hij

lemma antivary.comp_right (h : antivary f g) (k : ι' → ι) : antivary (f ∘ k) (g ∘ k) :=
λ i j hij, h hij

lemma monovary_on.comp_right (h : monovary_on f g s) (k : ι' → ι) :
  monovary_on (f ∘ k) (g ∘ k) (k ⁻¹' s) :=
λ i hi j hj, h hi hj

lemma antivary_on.comp_right (h : antivary_on f g s) (k : ι' → ι) :
  antivary_on (f ∘ k) (g ∘ k) (k ⁻¹' s) :=
λ i hi j hj, h hi hj

lemma monovary.comp_monotone_left (h : monovary f g) (hf : monotone f') : monovary (f' ∘ f) g :=
λ i j hij, hf $ h hij

lemma monovary.comp_antitone_left (h : monovary f g) (hf : antitone f') : antivary (f' ∘ f) g :=
λ i j hij, hf $ h hij

lemma antivary.comp_monotone_left (h : antivary f g) (hf : monotone f') : antivary (f' ∘ f) g :=
λ i j hij, hf $ h hij

lemma antivary.comp_antitone_left (h : antivary f g) (hf : antitone f') : monovary (f' ∘ f) g :=
λ i j hij, hf $ h hij

lemma monovary_on.comp_monotone_on_left (h : monovary_on f g s) (hf : monotone f') :
  monovary_on (f' ∘ f) g s :=
λ i hi j hj hij, hf $ h hi hj hij

lemma monovary_on.comp_antitone_on_left (h : monovary_on f g s) (hf : antitone f') :
  antivary_on (f' ∘ f) g s :=
λ i hi j hj hij, hf $ h hi hj hij

lemma antivary_on.comp_monotone_on_left (h : antivary_on f g s) (hf : monotone f') :
  antivary_on (f' ∘ f) g s :=
λ i hi j hj hij, hf $ h hi hj hij

lemma antivary_on.comp_antitone_on_left (h : antivary_on f g s) (hf : antitone f') :
  monovary_on (f' ∘ f) g s :=
λ i hi j hj hij, hf $ h hi hj hij

section order_dual
open order_dual

lemma monovary.dual : monovary f g → monovary (to_dual ∘ f) (to_dual ∘ g) := swap
lemma antivary.dual : antivary f g → antivary (to_dual ∘ f) (to_dual ∘ g) := swap
lemma monovary.dual_left : monovary f g → antivary (to_dual ∘ f) g := id
lemma antivary.dual_left : antivary f g → monovary (to_dual ∘ f) g := id
lemma monovary.dual_right : monovary f g → antivary f (to_dual ∘ g) := swap
lemma antivary.dual_right : antivary f g → monovary f (to_dual ∘ g) := swap

lemma monovary_on.dual : monovary_on f g s → monovary_on (to_dual ∘ f) (to_dual ∘ g) s := swap₂
lemma antivary_on.dual : antivary_on f g s → antivary_on (to_dual ∘ f) (to_dual ∘ g) s := swap₂
lemma monovary_on.dual_left : monovary_on f g s → antivary_on (to_dual ∘ f) g s := id
lemma antivary_on.dual_left : antivary_on f g s → monovary_on (to_dual ∘ f) g s := id
lemma monovary_on.dual_right : monovary_on f g s → antivary_on f (to_dual ∘ g) s := swap₂
lemma antivary_on.dual_right : antivary_on f g s → monovary_on f (to_dual ∘ g) s := swap₂

@[simp] lemma monovary_to_dual_left : monovary (to_dual ∘ f) g ↔ antivary f g := iff.rfl
@[simp] lemma monovary_to_dual_right : monovary f (to_dual ∘ g) ↔ antivary f g := forall_swap
@[simp] lemma antivary_to_dual_left : antivary (to_dual ∘ f) g ↔ monovary f g := iff.rfl
@[simp] lemma antivary_to_dual_right : antivary f (to_dual ∘ g) ↔ monovary f g := forall_swap

@[simp] lemma monovary_on_to_dual_left : monovary_on (to_dual ∘ f) g s ↔ antivary_on f g s :=
iff.rfl
@[simp] lemma monovary_on_to_dual_right : monovary_on f (to_dual ∘ g) s ↔ antivary_on f g s :=
forall₂_swap
@[simp] lemma antivary_on_to_dual_left : antivary_on (to_dual ∘ f) g s ↔ monovary_on f g s :=
iff.rfl
@[simp] lemma antivary_on_to_dual_right : antivary_on f (to_dual ∘ g) s ↔ monovary_on f g s :=
forall₂_swap

end order_dual

section partial_order
variables [partial_order ι]

@[simp] lemma monovary_id_iff : monovary f id ↔ monotone f := monotone_iff_forall_lt.symm
@[simp] lemma antivary_id_iff : antivary f id ↔ antitone f := antitone_iff_forall_lt.symm

@[simp] lemma monovary_on_id_iff : monovary_on f id s ↔ monotone_on f s :=
monotone_on_iff_forall_lt.symm

@[simp] lemma antivary_on_id_iff : antivary_on f id s ↔ antitone_on f s :=
antitone_on_iff_forall_lt.symm

end partial_order

variables [linear_order ι]

protected lemma monotone.monovary (hf : monotone f) (hg : monotone g) : monovary f g :=
λ i j hij, hf (hg.reflect_lt hij).le

protected lemma monotone.antivary (hf : monotone f) (hg : antitone g) : antivary f g :=
(hf.monovary hg.dual_right).dual_right

protected lemma antitone.monovary (hf : antitone f) (hg : antitone g) : monovary f g :=
(hf.dual_right.antivary hg).dual_left

protected lemma antitone.antivary (hf : antitone f) (hg : monotone g) : antivary f g :=
(hf.monovary hg.dual_right).dual_right

protected lemma monotone_on.monovary_on (hf : monotone_on f s) (hg : monotone_on g s) :
  monovary_on f g s :=
λ i hi j hj hij, hf hi hj (hg.reflect_lt hi hj hij).le

protected lemma monotone_on.antivary_on (hf : monotone_on f s) (hg : antitone_on g s) :
  antivary_on f g s :=
(hf.monovary_on hg.dual_right).dual_right

protected lemma antitone_on.monovary_on (hf : antitone_on f s) (hg : antitone_on g s) :
  monovary_on f g s :=
(hf.dual_right.antivary_on hg).dual_left

protected lemma antitone_on.antivary_on (hf : antitone_on f s) (hg : monotone_on g s) :
  antivary_on f g s :=
(hf.monovary_on hg.dual_right).dual_right

end preorder

section linear_order
variables [preorder α] [linear_order β] [preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}
  {g' : β → γ} {s : set ι}

lemma monovary_on.comp_monotone_on_right (h : monovary_on f g s) (hg : monotone_on g' (g '' s)) :
  monovary_on f (g' ∘ g) s :=
λ i hi j hj hij, h hi hj $ hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

lemma monovary_on.comp_antitone_on_right (h : monovary_on f g s) (hg : antitone_on g' (g '' s)) :
  antivary_on f (g' ∘ g) s :=
λ i hi j hj hij, h hj hi $ hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

lemma antivary_on.comp_monotone_on_right (h : antivary_on f g s) (hg : monotone_on g' (g '' s)) :
  antivary_on f (g' ∘ g) s :=
λ i hi j hj hij, h hi hj $ hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

lemma antivary_on.comp_antitone_on_right (h : antivary_on f g s) (hg : antitone_on g' (g '' s)) :
  monovary_on f (g' ∘ g) s :=
λ i hi j hj hij, h hj hi $ hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

protected lemma monovary.symm (h : monovary f g) : monovary g f :=
λ i j hf, le_of_not_lt $ λ hg, hf.not_le $ h hg

protected lemma antivary.symm (h : antivary f g) : antivary g f :=
λ i j hf, le_of_not_lt $ λ hg, hf.not_le $ h hg

protected lemma monovary_on.symm (h : monovary_on f g s) : monovary_on g f s :=
λ i hi j hj hf, le_of_not_lt $ λ hg, hf.not_le $ h hj hi hg

protected lemma antivary_on.symm (h : antivary_on f g s) : antivary_on g f s :=
λ i hi j hj hf, le_of_not_lt $ λ hg, hf.not_le $ h hi hj hg

end linear_order

section linear_order
variables [linear_order α] [linear_order β] {f : ι → α} {g : ι → β} {s : set ι}

protected lemma monovary_comm : monovary f g ↔ monovary g f := ⟨monovary.symm, monovary.symm⟩
protected lemma antivary_comm : antivary f g ↔ antivary g f := ⟨antivary.symm, antivary.symm⟩

protected lemma monovary_on_comm : monovary_on f g s ↔ monovary_on g f s :=
⟨monovary_on.symm, monovary_on.symm⟩

protected lemma antivary_on_comm : antivary_on f g s ↔ antivary_on g f s :=
⟨antivary_on.symm, antivary_on.symm⟩

end linear_order

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools