From c8922d33629788528cbfa02f9c56afb909d1c72d Mon Sep 17 00:00:00 2001 From: FR Date: Sat, 19 Oct 2024 15:25:40 +0000 Subject: [PATCH 01/10] chore: make `Quotient.mk''` an abbrev of `Quotient.mk _` (#16264) The plan is to deprecate `Quotient.mk''` in future PRs. --- Mathlib/Algebra/BigOperators/Group/Finset.lean | 4 ++-- Mathlib/Algebra/CharZero/Quotient.lean | 6 +++--- Mathlib/Data/List/Cycle.lean | 6 +++--- Mathlib/Data/Multiset/Basic.lean | 3 +++ Mathlib/Data/Quot.lean | 6 ++---- Mathlib/Data/Set/Image.lean | 2 +- Mathlib/GroupTheory/Coset/Basic.lean | 4 ++-- Mathlib/GroupTheory/GroupAction/Quotient.lean | 6 +++--- Mathlib/GroupTheory/PGroup.lean | 2 +- 9 files changed, 20 insertions(+), 19 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean index ed79af0319d28..1dbe92862bdb6 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset.lean @@ -1611,13 +1611,13 @@ theorem dvd_prod_of_mem (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) /-- A product can be partitioned into a product of products, each equivalent under a setoid. -/ @[to_additive "A sum can be partitioned into a sum of sums, each equivalent under a setoid."] theorem prod_partition (R : Setoid α) [DecidableRel R.r] : - ∏ x ∈ s, f x = ∏ xbar ∈ s.image Quotient.mk'', ∏ y ∈ s.filter (⟦·⟧ = xbar), f y := by + ∏ x ∈ s, f x = ∏ xbar ∈ s.image (Quotient.mk _), ∏ y ∈ s.filter (⟦·⟧ = xbar), f y := by refine (Finset.prod_image' f fun x _hx => ?_).symm rfl /-- If we can partition a product into subsets that cancel out, then the whole product cancels. -/ @[to_additive "If we can partition a sum into subsets that cancel out, then the whole sum cancels."] -theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R.r] +theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R] (h : ∀ x ∈ s, ∏ a ∈ s.filter fun y => R y x, f a = 1) : ∏ x ∈ s, f x = 1 := by rw [prod_partition R, ← Finset.prod_eq_one] intro xbar xbar_in_s diff --git a/Mathlib/Algebra/CharZero/Quotient.lean b/Mathlib/Algebra/CharZero/Quotient.lean index 8a44865763c7e..79b566ed37ce1 100644 --- a/Mathlib/Algebra/CharZero/Quotient.lean +++ b/Mathlib/Algebra/CharZero/Quotient.lean @@ -51,11 +51,11 @@ namespace QuotientAddGroup theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) : z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z) : R) := by - induction ψ using Quotient.inductionOn' - induction θ using Quotient.inductionOn' + induction ψ using Quotient.inductionOn + induction θ using Quotient.inductionOn -- Porting note: Introduced Zp notation to shorten lines let Zp := AddSubgroup.zmultiples p - have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl + have : (Quotient.mk _ : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl simp only [this] simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add, QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub] diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean index 9c8cbaa143209..18607fde71b44 100644 --- a/Mathlib/Data/List/Cycle.lean +++ b/Mathlib/Data/List/Cycle.lean @@ -824,11 +824,11 @@ theorem chain_ne_nil (r : α → α → Prop) {l : List α} : theorem chain_map {β : Type*} {r : α → α → Prop} (f : β → α) {s : Cycle β} : Chain r (s.map f) ↔ Chain (fun a b => r (f a) (f b)) s := - Quotient.inductionOn' s fun l => by + Quotient.inductionOn s fun l => by cases' l with a l · rfl - dsimp only [Chain, ← mk''_eq_coe, Quotient.liftOn'_mk'', Cycle.map, Quotient.map', Quot.map, - Quotient.mk'', Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map] + dsimp only [Chain, Quotient.liftOn_mk, Cycle.map, Quotient.map', Quot.map, + Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map] rw [← concat_eq_append, ← List.map_concat, List.chain_map f] simp diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index e04ef7fa7a1dc..97366784110f6 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -67,6 +67,9 @@ theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Multiset α) = l₂ ↔ l₁ instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ ≈ l₂) := inferInstanceAs (Decidable (l₁ ~ l₂)) +instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (isSetoid α l₁ l₂) := + inferInstanceAs (Decidable (l₁ ~ l₂)) + -- Porting note: `Quotient.recOnSubsingleton₂ s₁ s₂` was in parens which broke elaboration instance decidableEq [DecidableEq α] : DecidableEq (Multiset α) | s₁, s₂ => Quotient.recOnSubsingleton₂ s₁ s₂ fun _ _ => decidable_of_iff' _ Quotient.eq_iff_equiv diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean index 2bec860ba95b9..8dfbafe4dbf99 100644 --- a/Mathlib/Data/Quot.lean +++ b/Mathlib/Data/Quot.lean @@ -546,8 +546,8 @@ several different quotient relations on a type, for example quotient groups, rin -- Porting note: Quotient.mk' is the equivalent of Lean 3's `Quotient.mk` /-- A version of `Quotient.mk` taking `{s : Setoid α}` as an implicit argument instead of an instance argument. -/ -protected def mk'' (a : α) : Quotient s₁ := - Quot.mk s₁.1 a +protected abbrev mk'' (a : α) : Quotient s₁ := + ⟦a⟧ /-- `Quotient.mk''` is a surjective function. -/ theorem surjective_Quotient_mk'' : Function.Surjective (Quotient.mk'' : α → Quotient s₁) := @@ -693,7 +693,6 @@ protected theorem eq' {s₁ : Setoid α} {a b : α} : @Quotient.mk' α s₁ a = @Quotient.mk' α s₁ b ↔ s₁ a b := Quotient.eq -@[simp] protected theorem eq'' {a b : α} : @Quotient.mk'' α s₁ a = Quotient.mk'' b ↔ s₁ a b := Quotient.eq @@ -725,7 +724,6 @@ protected theorem liftOn₂'_mk {t : Setoid β} (f : α → β → γ) (h) (a : Quotient.liftOn₂' (Quotient.mk s a) (Quotient.mk t b) f h = f a b := Quotient.liftOn₂'_mk'' _ _ _ _ -@[simp] theorem map'_mk {t : Setoid β} (f : α → β) (h) (x : α) : (Quotient.mk s x).map' f h = (Quotient.mk t (f x)) := rfl diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index 00387c99f2202..1da452c8964d3 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -836,7 +836,7 @@ theorem range_quotient_lift [s : Setoid ι] (hf) : theorem range_quotient_mk' {s : Setoid α} : range (Quotient.mk' : α → Quotient s) = univ := range_quot_mk _ -@[simp] lemma Quotient.range_mk'' {sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ := +lemma Quotient.range_mk'' {sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ := range_quotient_mk @[simp] diff --git a/Mathlib/GroupTheory/Coset/Basic.lean b/Mathlib/GroupTheory/Coset/Basic.lean index e7aa809a354ae..c5df256757ef5 100644 --- a/Mathlib/GroupTheory/Coset/Basic.lean +++ b/Mathlib/GroupTheory/Coset/Basic.lean @@ -491,7 +491,7 @@ open MulAction in lemma orbit_mk_eq_smul (x : α) : MulAction.orbitRel.Quotient.orbit (x : α ⧸ s) = x • s := by ext rw [orbitRel.Quotient.mem_orbit] - simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply] using Setoid.comm' _ + simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _ @[to_additive] lemma orbit_eq_out'_smul (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x.out' • s := by @@ -530,7 +530,7 @@ noncomputable def groupEquivQuotientProdSubgroup : α ≃ (α ⧸ s) × s := show (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃ _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _ - simp [-Quotient.eq''] + simp rfl _ ≃ Σ _L : α ⧸ s, s := Equiv.sigmaCongrRight fun _ => leftCosetEquivSubgroup _ _ ≃ (α ⧸ s) × s := Equiv.sigmaEquivProd _ _ diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index f58416df124ac..e532945e65310 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -320,10 +320,10 @@ noncomputable def equivSubgroupOrbitsSetoidComap (H : Subgroup α) (ω : Ω) : toFun := fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, by simp only [Set.mem_preimage, Set.mem_singleton_iff] have hx := x.property - rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk] at hx⟩⟧) fun a b h ↦ by - simp only [← Quotient.eq'', Quotient.mk''_eq_mk, + rwa [orbitRel.Quotient.mem_orbit] at hx⟩⟧) fun a b h ↦ by + simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h - simp only [← Quotient.mk''_eq_mk, Quotient.eq''] at h ⊢ + simp only [Quotient.eq] at h ⊢ exact h invFun := fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, by have hx := x.property diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean index d882d7e22ca40..eb9cdfbf182a9 100644 --- a/Mathlib/GroupTheory/PGroup.lean +++ b/Mathlib/GroupTheory/PGroup.lean @@ -179,7 +179,7 @@ theorem card_modEq_card_fixedPoints : Nat.card α ≡ Nat.card (fixedPoints G α rw [Nat.card_eq_fintype_card] at hk have : k = 0 := by contrapose! hb - simp [-Quotient.eq'', key, hk, hb] + simp [-Quotient.eq, key, hk, hb] exact ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩ From 64ac27ea68f1e00fc29e2ce69a1c73c348dcdfb4 Mon Sep 17 00:00:00 2001 From: Paul Lezeau Date: Sat, 19 Oct 2024 16:03:51 +0000 Subject: [PATCH 02/10] chore(Order/Bounds/Basic): Split long file into two shorter files (#16539) This PR transfers some of the content from `Order/Bounds/Basic` into a new file, `Order/Bounds/Image`. --- Mathlib.lean | 1 + Mathlib/Order/Bounds/Basic.lean | 482 --------------------------- Mathlib/Order/Bounds/Image.lean | 498 ++++++++++++++++++++++++++++ Mathlib/Order/Bounds/OrderIso.lean | 2 +- Mathlib/Order/CompleteLattice.lean | 1 + Mathlib/Order/GaloisConnection.lean | 2 +- 6 files changed, 502 insertions(+), 484 deletions(-) create mode 100644 Mathlib/Order/Bounds/Image.lean diff --git a/Mathlib.lean b/Mathlib.lean index 4c5d00a1fa732..5fcbb05388323 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3621,6 +3621,7 @@ import Mathlib.Order.Bounded import Mathlib.Order.BoundedOrder import Mathlib.Order.Bounds.Basic import Mathlib.Order.Bounds.Defs +import Mathlib.Order.Bounds.Image import Mathlib.Order.Bounds.OrderIso import Mathlib.Order.Category.BddDistLat import Mathlib.Order.Category.BddLat diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index fb6e31a954dff..66d0f19bb54b8 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/Mathlib/Order/Bounds/Basic.lean @@ -3,7 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Yury Kudryashov -/ -import Mathlib.Data.Set.NAry import Mathlib.Order.Bounds.Defs import Mathlib.Order.Directed import Mathlib.Order.Interval.Set.Basic @@ -905,484 +904,3 @@ theorem IsGLB.exists_between' (h : IsGLB s a) (h' : a ∉ s) (hb : a < b) : ∃ ⟨c, hcs, hac.lt_of_ne fun hac => h' <| hac.symm ▸ hcs, hcb⟩ end LinearOrder - -/-! -### Images of upper/lower bounds under monotone functions --/ - - -namespace MonotoneOn - -variable [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} - -theorem mem_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) - (Hat : a ∈ t) : f a ∈ upperBounds (f '' s) := - forall_mem_image.2 fun _ H => Hf (Hst H) Hat (Has H) - -theorem mem_upperBounds_image_self (Hf : MonotoneOn f t) : - a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t) := - Hf.mem_upperBounds_image subset_rfl - -theorem mem_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) - (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s) := - forall_mem_image.2 fun _ H => Hf Hat (Hst H) (Has H) - -theorem mem_lowerBounds_image_self (Hf : MonotoneOn f t) : - a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) := - Hf.mem_lowerBounds_image subset_rfl - -theorem image_upperBounds_subset_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) : - f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s) := by - rintro _ ⟨a, ha, rfl⟩ - exact Hf.mem_upperBounds_image Hst ha.1 ha.2 - -theorem image_lowerBounds_subset_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) : - f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s) := - Hf.dual.image_upperBounds_subset_upperBounds_image Hst - -/-- The image under a monotone function on a set `t` of a subset which has an upper bound in `t` - is bounded above. -/ -theorem map_bddAbove (Hf : MonotoneOn f t) (Hst : s ⊆ t) : - (upperBounds s ∩ t).Nonempty → BddAbove (f '' s) := fun ⟨C, hs, ht⟩ => - ⟨f C, Hf.mem_upperBounds_image Hst hs ht⟩ - -/-- The image under a monotone function on a set `t` of a subset which has a lower bound in `t` - is bounded below. -/ -theorem map_bddBelow (Hf : MonotoneOn f t) (Hst : s ⊆ t) : - (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s) := fun ⟨C, hs, ht⟩ => - ⟨f C, Hf.mem_lowerBounds_image Hst hs ht⟩ - -/-- A monotone map sends a least element of a set to a least element of its image. -/ -theorem map_isLeast (Hf : MonotoneOn f t) (Ha : IsLeast t a) : IsLeast (f '' t) (f a) := - ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image_self Ha.2 Ha.1⟩ - -/-- A monotone map sends a greatest element of a set to a greatest element of its image. -/ -theorem map_isGreatest (Hf : MonotoneOn f t) (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a) := - ⟨mem_image_of_mem _ Ha.1, Hf.mem_upperBounds_image_self Ha.2 Ha.1⟩ - -end MonotoneOn - -namespace AntitoneOn - -variable [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} - -theorem mem_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : - a ∈ t → f a ∈ upperBounds (f '' s) := - Hf.dual_right.mem_lowerBounds_image Hst Has - -theorem mem_upperBounds_image_self (Hf : AntitoneOn f t) : - a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t) := - Hf.dual_right.mem_lowerBounds_image_self - -theorem mem_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) : - a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s) := - Hf.dual_right.mem_upperBounds_image Hst - -theorem mem_lowerBounds_image_self (Hf : AntitoneOn f t) : - a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) := - Hf.dual_right.mem_upperBounds_image_self - -theorem image_lowerBounds_subset_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) : - f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s) := - Hf.dual_right.image_lowerBounds_subset_lowerBounds_image Hst - -theorem image_upperBounds_subset_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) : - f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s) := - Hf.dual_right.image_upperBounds_subset_upperBounds_image Hst - -/-- The image under an antitone function of a set which is bounded above is bounded below. -/ -theorem map_bddAbove (Hf : AntitoneOn f t) (Hst : s ⊆ t) : - (upperBounds s ∩ t).Nonempty → BddBelow (f '' s) := - Hf.dual_right.map_bddAbove Hst - -/-- The image under an antitone function of a set which is bounded below is bounded above. -/ -theorem map_bddBelow (Hf : AntitoneOn f t) (Hst : s ⊆ t) : - (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s) := - Hf.dual_right.map_bddBelow Hst - -/-- An antitone map sends a greatest element of a set to a least element of its image. -/ -theorem map_isGreatest (Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a) := - Hf.dual_right.map_isGreatest - -/-- An antitone map sends a least element of a set to a greatest element of its image. -/ -theorem map_isLeast (Hf : AntitoneOn f t) : IsLeast t a → IsGreatest (f '' t) (f a) := - Hf.dual_right.map_isLeast - -end AntitoneOn - -namespace Monotone - -variable [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} - -include Hf - -theorem mem_upperBounds_image (Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s) := - forall_mem_image.2 fun _ H => Hf (Ha H) - -theorem mem_lowerBounds_image (Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s) := - forall_mem_image.2 fun _ H => Hf (Ha H) - -theorem image_upperBounds_subset_upperBounds_image : - f '' upperBounds s ⊆ upperBounds (f '' s) := by - rintro _ ⟨a, ha, rfl⟩ - exact Hf.mem_upperBounds_image ha - -theorem image_lowerBounds_subset_lowerBounds_image : f '' lowerBounds s ⊆ lowerBounds (f '' s) := - Hf.dual.image_upperBounds_subset_upperBounds_image - -/-- The image under a monotone function of a set which is bounded above is bounded above. See also -`BddAbove.image2`. -/ -theorem map_bddAbove : BddAbove s → BddAbove (f '' s) - | ⟨C, hC⟩ => ⟨f C, Hf.mem_upperBounds_image hC⟩ - -/-- The image under a monotone function of a set which is bounded below is bounded below. See also -`BddBelow.image2`. -/ -theorem map_bddBelow : BddBelow s → BddBelow (f '' s) - | ⟨C, hC⟩ => ⟨f C, Hf.mem_lowerBounds_image hC⟩ - -/-- A monotone map sends a least element of a set to a least element of its image. -/ -theorem map_isLeast (Ha : IsLeast s a) : IsLeast (f '' s) (f a) := - ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image Ha.2⟩ - -/-- A monotone map sends a greatest element of a set to a greatest element of its image. -/ -theorem map_isGreatest (Ha : IsGreatest s a) : IsGreatest (f '' s) (f a) := - ⟨mem_image_of_mem _ Ha.1, Hf.mem_upperBounds_image Ha.2⟩ - -end Monotone - -namespace Antitone - -variable [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} - -include hf - -theorem mem_upperBounds_image : a ∈ lowerBounds s → f a ∈ upperBounds (f '' s) := - hf.dual_right.mem_lowerBounds_image - -theorem mem_lowerBounds_image : a ∈ upperBounds s → f a ∈ lowerBounds (f '' s) := - hf.dual_right.mem_upperBounds_image - -theorem image_lowerBounds_subset_upperBounds_image : f '' lowerBounds s ⊆ upperBounds (f '' s) := - hf.dual_right.image_lowerBounds_subset_lowerBounds_image - -theorem image_upperBounds_subset_lowerBounds_image : f '' upperBounds s ⊆ lowerBounds (f '' s) := - hf.dual_right.image_upperBounds_subset_upperBounds_image - -/-- The image under an antitone function of a set which is bounded above is bounded below. -/ -theorem map_bddAbove : BddAbove s → BddBelow (f '' s) := - hf.dual_right.map_bddAbove - -/-- The image under an antitone function of a set which is bounded below is bounded above. -/ -theorem map_bddBelow : BddBelow s → BddAbove (f '' s) := - hf.dual_right.map_bddBelow - -/-- An antitone map sends a greatest element of a set to a least element of its image. -/ -theorem map_isGreatest : IsGreatest s a → IsLeast (f '' s) (f a) := - hf.dual_right.map_isGreatest - -/-- An antitone map sends a least element of a set to a greatest element of its image. -/ -theorem map_isLeast : IsLeast s a → IsGreatest (f '' s) (f a) := - hf.dual_right.map_isLeast - -end Antitone - -section Image2 - -variable [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} - {b : β} - -section MonotoneMonotone - -variable (h₀ : ∀ b, Monotone (swap f b)) (h₁ : ∀ a, Monotone (f a)) - -include h₀ h₁ - -theorem mem_upperBounds_image2 (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : - f a b ∈ upperBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem mem_lowerBounds_image2 (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : - f a b ∈ lowerBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem image2_upperBounds_upperBounds_subset : - image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ mem_upperBounds_image2 h₀ h₁ ha hb - -theorem image2_lowerBounds_lowerBounds_subset : - image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ mem_lowerBounds_image2 h₀ h₁ ha hb - -/-- See also `Monotone.map_bddAbove`. -/ -protected theorem BddAbove.image2 : - BddAbove s → BddAbove t → BddAbove (image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩ - -/-- See also `Monotone.map_bddBelow`. -/ -protected theorem BddBelow.image2 : - BddBelow s → BddBelow t → BddBelow (image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_lowerBounds_image2 h₀ h₁ ha hb⟩ - -protected theorem IsGreatest.image2 (ha : IsGreatest s a) (hb : IsGreatest t b) : - IsGreatest (image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2 h₀ h₁ ha.2 hb.2⟩ - -protected theorem IsLeast.image2 (ha : IsLeast s a) (hb : IsLeast t b) : - IsLeast (image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2 h₀ h₁ ha.2 hb.2⟩ - -end MonotoneMonotone - -section MonotoneAntitone - -variable (h₀ : ∀ b, Monotone (swap f b)) (h₁ : ∀ a, Antitone (f a)) - -include h₀ h₁ - -theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds (ha : a ∈ upperBounds s) - (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s) - (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 : - image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ - mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb - -theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 : - image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ - mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb - -theorem BddAbove.bddAbove_image2_of_bddBelow : - BddAbove s → BddBelow t → BddAbove (Set.image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩ - -theorem BddBelow.bddBelow_image2_of_bddAbove : - BddBelow s → BddAbove t → BddBelow (Set.image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb⟩ - -theorem IsGreatest.isGreatest_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) : - IsGreatest (Set.image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, - mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩ - -theorem IsLeast.isLeast_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) : - IsLeast (Set.image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, - mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩ - -end MonotoneAntitone - -section AntitoneAntitone - -variable (h₀ : ∀ b, Antitone (swap f b)) (h₁ : ∀ a, Antitone (f a)) - -include h₀ h₁ - -theorem mem_upperBounds_image2_of_mem_lowerBounds (ha : a ∈ lowerBounds s) - (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem mem_lowerBounds_image2_of_mem_upperBounds (ha : a ∈ upperBounds s) - (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem image2_upperBounds_upperBounds_subset_upperBounds_image2 : - image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ - mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb - -theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 : - image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ - mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb - -theorem BddBelow.image2_bddAbove : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩ - -theorem BddAbove.image2_bddBelow : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb⟩ - -theorem IsLeast.isGreatest_image2 (ha : IsLeast s a) (hb : IsLeast t b) : - IsGreatest (Set.image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩ - -theorem IsGreatest.isLeast_image2 (ha : IsGreatest s a) (hb : IsGreatest t b) : - IsLeast (Set.image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩ - -end AntitoneAntitone - -section AntitoneMonotone - -variable (h₀ : ∀ b, Antitone (swap f b)) (h₁ : ∀ a, Monotone (f a)) - -include h₀ h₁ - -theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s) - (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds (ha : a ∈ upperBounds s) - (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (image2 f s t) := - forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy - -theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2 : - image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ - mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb - -theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 : - image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) := - image2_subset_iff.2 fun _ ha _ hb ↦ - mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb - -theorem BddBelow.bddAbove_image2_of_bddAbove : - BddBelow s → BddAbove t → BddAbove (Set.image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩ - -theorem BddAbove.bddBelow_image2_of_bddAbove : - BddAbove s → BddBelow t → BddBelow (Set.image2 f s t) := by - rintro ⟨a, ha⟩ ⟨b, hb⟩ - exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩ - -theorem IsLeast.isGreatest_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) : - IsGreatest (Set.image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, - mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩ - -theorem IsGreatest.isLeast_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) : - IsLeast (Set.image2 f s t) (f a b) := - ⟨mem_image2_of_mem ha.1 hb.1, - mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩ - -end AntitoneMonotone - -end Image2 - -section Prod - -variable {α β : Type*} [Preorder α] [Preorder β] - -lemma bddAbove_prod {s : Set (α × β)} : - BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s) := - ⟨fun ⟨p, hp⟩ ↦ ⟨⟨p.1, forall_mem_image.2 fun _q hq ↦ (hp hq).1⟩, - ⟨p.2, forall_mem_image.2 fun _q hq ↦ (hp hq).2⟩⟩, - fun ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ ↦ ⟨⟨x, y⟩, fun _p hp ↦ - ⟨hx <| mem_image_of_mem _ hp, hy <| mem_image_of_mem _ hp⟩⟩⟩ - -lemma bddBelow_prod {s : Set (α × β)} : - BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s) := - bddAbove_prod (α := αᵒᵈ) (β := βᵒᵈ) - -lemma bddAbove_range_prod {F : ι → α × β} : - BddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F) := by - simp only [bddAbove_prod, ← range_comp] - -lemma bddBelow_range_prod {F : ι → α × β} : - BddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F) := - bddAbove_range_prod (α := αᵒᵈ) (β := βᵒᵈ) - -theorem isLUB_prod {s : Set (α × β)} (p : α × β) : - IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 := by - refine - ⟨fun H => - ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩, - ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩, - fun H => ⟨?_, ?_⟩⟩ - · suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1 - exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩ - · suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2 - exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩ - · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩ - · exact fun q hq => - ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq, - H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩ - -theorem isGLB_prod {s : Set (α × β)} (p : α × β) : - IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 := - @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _ - -end Prod - - -section Pi - -variable {π : α → Type*} [∀ a, Preorder (π a)] - -lemma bddAbove_pi {s : Set (∀ a, π a)} : - BddAbove s ↔ ∀ a, BddAbove (Function.eval a '' s) := - ⟨fun ⟨f, hf⟩ a ↦ ⟨f a, forall_mem_image.2 fun _ hg ↦ hf hg a⟩, - fun h ↦ ⟨fun a ↦ (h a).some, fun _ hg a ↦ (h a).some_mem <| mem_image_of_mem _ hg⟩⟩ - -lemma bddBelow_pi {s : Set (∀ a, π a)} : - BddBelow s ↔ ∀ a, BddBelow (Function.eval a '' s) := - bddAbove_pi (π := fun a ↦ (π a)ᵒᵈ) - -lemma bddAbove_range_pi {F : ι → ∀ a, π a} : - BddAbove (range F) ↔ ∀ a, BddAbove (range fun i ↦ F i a) := by - simp only [bddAbove_pi, ← range_comp] - rfl - -lemma bddBelow_range_pi {F : ι → ∀ a, π a} : - BddBelow (range F) ↔ ∀ a, BddBelow (range fun i ↦ F i a) := - bddAbove_range_pi (π := fun a ↦ (π a)ᵒᵈ) - -theorem isLUB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} : - IsLUB s f ↔ ∀ a, IsLUB (Function.eval a '' s) (f a) := by - classical - refine - ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H => - ⟨?_, ?_⟩⟩ - · suffices h : Function.update f a b ∈ upperBounds s from Function.update_same a b f ▸ H.2 h a - exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩ - · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg) - · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg) - -theorem isGLB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} : - IsGLB s f ↔ ∀ a, IsGLB (Function.eval a '' s) (f a) := - @isLUB_pi α (fun a => (π a)ᵒᵈ) _ s f - -end Pi - -theorem IsGLB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) - {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) : IsGLB s x := - ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy => - hf.1 <| hx.2 <| Monotone.mem_lowerBounds_image (fun _ _ => hf.2) hy⟩ - -theorem IsLUB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) - {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x := - ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy => - hf.1 <| hx.2 <| Monotone.mem_upperBounds_image (fun _ _ => hf.2) hy⟩ - -lemma BddAbove.range_mono [Preorder β] {f : α → β} (g : α → β) (h : ∀ a, f a ≤ g a) - (hbdd : BddAbove (range g)) : BddAbove (range f) := by - obtain ⟨C, hC⟩ := hbdd - use C - rintro - ⟨x, rfl⟩ - exact (h x).trans (hC <| mem_range_self x) - -lemma BddBelow.range_mono [Preorder β] (f : α → β) {g : α → β} (h : ∀ a, f a ≤ g a) - (hbdd : BddBelow (range f)) : BddBelow (range g) := - BddAbove.range_mono (β := βᵒᵈ) f h hbdd - -lemma BddAbove.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} - (hf : BddAbove (range f)) (hg : Monotone g) : BddAbove (range (fun x => g (f x))) := by - change BddAbove (range (g ∘ f)) - simpa only [Set.range_comp] using hg.map_bddAbove hf - -lemma BddBelow.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} - (hf : BddBelow (range f)) (hg : Monotone g) : BddBelow (range (fun x => g (f x))) := by - change BddBelow (range (g ∘ f)) - simpa only [Set.range_comp] using hg.map_bddBelow hf diff --git a/Mathlib/Order/Bounds/Image.lean b/Mathlib/Order/Bounds/Image.lean new file mode 100644 index 0000000000000..910c466332520 --- /dev/null +++ b/Mathlib/Order/Bounds/Image.lean @@ -0,0 +1,498 @@ +/- +Copyright (c) 2017 Paul Lezeau. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Yury Kudryashov, Paul Lezeau +-/ +import Mathlib.Data.Set.NAry +import Mathlib.Order.Bounds.Defs + +/-! + +# Images of upper/lower bounds under monotone functions + +In this file we prove various results about the behaviour of bounds under monotone/antitone maps. +-/ + +open Function Set + +open OrderDual (toDual ofDual) + +universe u v w x + +variable {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} + +namespace MonotoneOn + +variable [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} + +theorem mem_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) + (Hat : a ∈ t) : f a ∈ upperBounds (f '' s) := + forall_mem_image.2 fun _ H => Hf (Hst H) Hat (Has H) + +theorem mem_upperBounds_image_self (Hf : MonotoneOn f t) : + a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t) := + Hf.mem_upperBounds_image subset_rfl + +theorem mem_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) + (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s) := + forall_mem_image.2 fun _ H => Hf Hat (Hst H) (Has H) + +theorem mem_lowerBounds_image_self (Hf : MonotoneOn f t) : + a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) := + Hf.mem_lowerBounds_image subset_rfl + +theorem image_upperBounds_subset_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) : + f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s) := by + rintro _ ⟨a, ha, rfl⟩ + exact Hf.mem_upperBounds_image Hst ha.1 ha.2 + +theorem image_lowerBounds_subset_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) : + f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s) := + Hf.dual.image_upperBounds_subset_upperBounds_image Hst + +/-- The image under a monotone function on a set `t` of a subset which has an upper bound in `t` + is bounded above. -/ +theorem map_bddAbove (Hf : MonotoneOn f t) (Hst : s ⊆ t) : + (upperBounds s ∩ t).Nonempty → BddAbove (f '' s) := fun ⟨C, hs, ht⟩ => + ⟨f C, Hf.mem_upperBounds_image Hst hs ht⟩ + +/-- The image under a monotone function on a set `t` of a subset which has a lower bound in `t` + is bounded below. -/ +theorem map_bddBelow (Hf : MonotoneOn f t) (Hst : s ⊆ t) : + (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s) := fun ⟨C, hs, ht⟩ => + ⟨f C, Hf.mem_lowerBounds_image Hst hs ht⟩ + +/-- A monotone map sends a least element of a set to a least element of its image. -/ +theorem map_isLeast (Hf : MonotoneOn f t) (Ha : IsLeast t a) : IsLeast (f '' t) (f a) := + ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image_self Ha.2 Ha.1⟩ + +/-- A monotone map sends a greatest element of a set to a greatest element of its image. -/ +theorem map_isGreatest (Hf : MonotoneOn f t) (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a) := + ⟨mem_image_of_mem _ Ha.1, Hf.mem_upperBounds_image_self Ha.2 Ha.1⟩ + +end MonotoneOn + +namespace AntitoneOn + +variable [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} + +theorem mem_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : + a ∈ t → f a ∈ upperBounds (f '' s) := + Hf.dual_right.mem_lowerBounds_image Hst Has + +theorem mem_upperBounds_image_self (Hf : AntitoneOn f t) : + a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t) := + Hf.dual_right.mem_lowerBounds_image_self + +theorem mem_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) : + a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s) := + Hf.dual_right.mem_upperBounds_image Hst + +theorem mem_lowerBounds_image_self (Hf : AntitoneOn f t) : + a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) := + Hf.dual_right.mem_upperBounds_image_self + +theorem image_lowerBounds_subset_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) : + f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s) := + Hf.dual_right.image_lowerBounds_subset_lowerBounds_image Hst + +theorem image_upperBounds_subset_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) : + f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s) := + Hf.dual_right.image_upperBounds_subset_upperBounds_image Hst + +/-- The image under an antitone function of a set which is bounded above is bounded below. -/ +theorem map_bddAbove (Hf : AntitoneOn f t) (Hst : s ⊆ t) : + (upperBounds s ∩ t).Nonempty → BddBelow (f '' s) := + Hf.dual_right.map_bddAbove Hst + +/-- The image under an antitone function of a set which is bounded below is bounded above. -/ +theorem map_bddBelow (Hf : AntitoneOn f t) (Hst : s ⊆ t) : + (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s) := + Hf.dual_right.map_bddBelow Hst + +/-- An antitone map sends a greatest element of a set to a least element of its image. -/ +theorem map_isGreatest (Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a) := + Hf.dual_right.map_isGreatest + +/-- An antitone map sends a least element of a set to a greatest element of its image. -/ +theorem map_isLeast (Hf : AntitoneOn f t) : IsLeast t a → IsGreatest (f '' t) (f a) := + Hf.dual_right.map_isLeast + +end AntitoneOn + +namespace Monotone + +variable [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} + +include Hf + +theorem mem_upperBounds_image (Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s) := + forall_mem_image.2 fun _ H => Hf (Ha H) + +theorem mem_lowerBounds_image (Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s) := + forall_mem_image.2 fun _ H => Hf (Ha H) + +theorem image_upperBounds_subset_upperBounds_image : + f '' upperBounds s ⊆ upperBounds (f '' s) := by + rintro _ ⟨a, ha, rfl⟩ + exact Hf.mem_upperBounds_image ha + +theorem image_lowerBounds_subset_lowerBounds_image : f '' lowerBounds s ⊆ lowerBounds (f '' s) := + Hf.dual.image_upperBounds_subset_upperBounds_image + +/-- The image under a monotone function of a set which is bounded above is bounded above. See also +`BddAbove.image2`. -/ +theorem map_bddAbove : BddAbove s → BddAbove (f '' s) + | ⟨C, hC⟩ => ⟨f C, Hf.mem_upperBounds_image hC⟩ + +/-- The image under a monotone function of a set which is bounded below is bounded below. See also +`BddBelow.image2`. -/ +theorem map_bddBelow : BddBelow s → BddBelow (f '' s) + | ⟨C, hC⟩ => ⟨f C, Hf.mem_lowerBounds_image hC⟩ + +/-- A monotone map sends a least element of a set to a least element of its image. -/ +theorem map_isLeast (Ha : IsLeast s a) : IsLeast (f '' s) (f a) := + ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image Ha.2⟩ + +/-- A monotone map sends a greatest element of a set to a greatest element of its image. -/ +theorem map_isGreatest (Ha : IsGreatest s a) : IsGreatest (f '' s) (f a) := + ⟨mem_image_of_mem _ Ha.1, Hf.mem_upperBounds_image Ha.2⟩ + +end Monotone + +namespace Antitone + +variable [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} + +include hf + +theorem mem_upperBounds_image : a ∈ lowerBounds s → f a ∈ upperBounds (f '' s) := + hf.dual_right.mem_lowerBounds_image + +theorem mem_lowerBounds_image : a ∈ upperBounds s → f a ∈ lowerBounds (f '' s) := + hf.dual_right.mem_upperBounds_image + +theorem image_lowerBounds_subset_upperBounds_image : f '' lowerBounds s ⊆ upperBounds (f '' s) := + hf.dual_right.image_lowerBounds_subset_lowerBounds_image + +theorem image_upperBounds_subset_lowerBounds_image : f '' upperBounds s ⊆ lowerBounds (f '' s) := + hf.dual_right.image_upperBounds_subset_upperBounds_image + +/-- The image under an antitone function of a set which is bounded above is bounded below. -/ +theorem map_bddAbove : BddAbove s → BddBelow (f '' s) := + hf.dual_right.map_bddAbove + +/-- The image under an antitone function of a set which is bounded below is bounded above. -/ +theorem map_bddBelow : BddBelow s → BddAbove (f '' s) := + hf.dual_right.map_bddBelow + +/-- An antitone map sends a greatest element of a set to a least element of its image. -/ +theorem map_isGreatest : IsGreatest s a → IsLeast (f '' s) (f a) := + hf.dual_right.map_isGreatest + +/-- An antitone map sends a least element of a set to a greatest element of its image. -/ +theorem map_isLeast : IsLeast s a → IsGreatest (f '' s) (f a) := + hf.dual_right.map_isLeast + +end Antitone + +section Image2 + +variable [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} + {b : β} + +section MonotoneMonotone + +variable (h₀ : ∀ b, Monotone (swap f b)) (h₁ : ∀ a, Monotone (f a)) + +include h₀ h₁ + +theorem mem_upperBounds_image2 (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : + f a b ∈ upperBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem mem_lowerBounds_image2 (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : + f a b ∈ lowerBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem image2_upperBounds_upperBounds_subset : + image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ mem_upperBounds_image2 h₀ h₁ ha hb + +theorem image2_lowerBounds_lowerBounds_subset : + image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ mem_lowerBounds_image2 h₀ h₁ ha hb + +/-- See also `Monotone.map_bddAbove`. -/ +protected theorem BddAbove.image2 : + BddAbove s → BddAbove t → BddAbove (image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩ + +/-- See also `Monotone.map_bddBelow`. -/ +protected theorem BddBelow.image2 : + BddBelow s → BddBelow t → BddBelow (image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_lowerBounds_image2 h₀ h₁ ha hb⟩ + +protected theorem IsGreatest.image2 (ha : IsGreatest s a) (hb : IsGreatest t b) : + IsGreatest (image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2 h₀ h₁ ha.2 hb.2⟩ + +protected theorem IsLeast.image2 (ha : IsLeast s a) (hb : IsLeast t b) : + IsLeast (image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2 h₀ h₁ ha.2 hb.2⟩ + +end MonotoneMonotone + +section MonotoneAntitone + +variable (h₀ : ∀ b, Monotone (swap f b)) (h₁ : ∀ a, Antitone (f a)) + +include h₀ h₁ + +theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds (ha : a ∈ upperBounds s) + (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s) + (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 : + image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ + mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb + +theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 : + image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ + mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb + +theorem BddAbove.bddAbove_image2_of_bddBelow : + BddAbove s → BddBelow t → BddAbove (Set.image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩ + +theorem BddBelow.bddBelow_image2_of_bddAbove : + BddBelow s → BddAbove t → BddBelow (Set.image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb⟩ + +theorem IsGreatest.isGreatest_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) : + IsGreatest (Set.image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, + mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩ + +theorem IsLeast.isLeast_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) : + IsLeast (Set.image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, + mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩ + +end MonotoneAntitone + +section AntitoneAntitone + +variable (h₀ : ∀ b, Antitone (swap f b)) (h₁ : ∀ a, Antitone (f a)) + +include h₀ h₁ + +theorem mem_upperBounds_image2_of_mem_lowerBounds (ha : a ∈ lowerBounds s) + (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem mem_lowerBounds_image2_of_mem_upperBounds (ha : a ∈ upperBounds s) + (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem image2_upperBounds_upperBounds_subset_upperBounds_image2 : + image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ + mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb + +theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 : + image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ + mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb + +theorem BddBelow.image2_bddAbove : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩ + +theorem BddAbove.image2_bddBelow : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb⟩ + +theorem IsLeast.isGreatest_image2 (ha : IsLeast s a) (hb : IsLeast t b) : + IsGreatest (Set.image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩ + +theorem IsGreatest.isLeast_image2 (ha : IsGreatest s a) (hb : IsGreatest t b) : + IsLeast (Set.image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩ + +end AntitoneAntitone + +section AntitoneMonotone + +variable (h₀ : ∀ b, Antitone (swap f b)) (h₁ : ∀ a, Monotone (f a)) + +include h₀ h₁ + +theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s) + (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds (ha : a ∈ upperBounds s) + (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (image2 f s t) := + forall_image2_iff.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy + +theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2 : + image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ + mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb + +theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 : + image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) := + image2_subset_iff.2 fun _ ha _ hb ↦ + mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb + +theorem BddBelow.bddAbove_image2_of_bddAbove : + BddBelow s → BddAbove t → BddAbove (Set.image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩ + +theorem BddAbove.bddBelow_image2_of_bddAbove : + BddAbove s → BddBelow t → BddBelow (Set.image2 f s t) := by + rintro ⟨a, ha⟩ ⟨b, hb⟩ + exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩ + +theorem IsLeast.isGreatest_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) : + IsGreatest (Set.image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, + mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩ + +theorem IsGreatest.isLeast_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) : + IsLeast (Set.image2 f s t) (f a b) := + ⟨mem_image2_of_mem ha.1 hb.1, + mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩ + +end AntitoneMonotone + +end Image2 + +section Prod + +variable {α β : Type*} [Preorder α] [Preorder β] + +lemma bddAbove_prod {s : Set (α × β)} : + BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s) := + ⟨fun ⟨p, hp⟩ ↦ ⟨⟨p.1, forall_mem_image.2 fun _q hq ↦ (hp hq).1⟩, + ⟨p.2, forall_mem_image.2 fun _q hq ↦ (hp hq).2⟩⟩, + fun ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ ↦ ⟨⟨x, y⟩, fun _p hp ↦ + ⟨hx <| mem_image_of_mem _ hp, hy <| mem_image_of_mem _ hp⟩⟩⟩ + +lemma bddBelow_prod {s : Set (α × β)} : + BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s) := + bddAbove_prod (α := αᵒᵈ) (β := βᵒᵈ) + +lemma bddAbove_range_prod {F : ι → α × β} : + BddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F) := by + simp only [bddAbove_prod, ← range_comp] + +lemma bddBelow_range_prod {F : ι → α × β} : + BddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F) := + bddAbove_range_prod (α := αᵒᵈ) (β := βᵒᵈ) + +theorem isLUB_prod {s : Set (α × β)} (p : α × β) : + IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 := by + refine + ⟨fun H => + ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩, + ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩, + fun H => ⟨?_, ?_⟩⟩ + · suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1 + exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩ + · suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2 + exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩ + · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩ + · exact fun q hq => + ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq, + H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩ + +theorem isGLB_prod {s : Set (α × β)} (p : α × β) : + IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 := + @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _ + +end Prod + + +section Pi + +variable {π : α → Type*} [∀ a, Preorder (π a)] + +lemma bddAbove_pi {s : Set (∀ a, π a)} : + BddAbove s ↔ ∀ a, BddAbove (Function.eval a '' s) := + ⟨fun ⟨f, hf⟩ a ↦ ⟨f a, forall_mem_image.2 fun _ hg ↦ hf hg a⟩, + fun h ↦ ⟨fun a ↦ (h a).some, fun _ hg a ↦ (h a).some_mem <| mem_image_of_mem _ hg⟩⟩ + +lemma bddBelow_pi {s : Set (∀ a, π a)} : + BddBelow s ↔ ∀ a, BddBelow (Function.eval a '' s) := + bddAbove_pi (π := fun a ↦ (π a)ᵒᵈ) + +lemma bddAbove_range_pi {F : ι → ∀ a, π a} : + BddAbove (range F) ↔ ∀ a, BddAbove (range fun i ↦ F i a) := by + simp only [bddAbove_pi, ← range_comp] + rfl + +lemma bddBelow_range_pi {F : ι → ∀ a, π a} : + BddBelow (range F) ↔ ∀ a, BddBelow (range fun i ↦ F i a) := + bddAbove_range_pi (π := fun a ↦ (π a)ᵒᵈ) + +theorem isLUB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} : + IsLUB s f ↔ ∀ a, IsLUB (Function.eval a '' s) (f a) := by + classical + refine + ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H => + ⟨?_, ?_⟩⟩ + · suffices h : Function.update f a b ∈ upperBounds s from Function.update_same a b f ▸ H.2 h a + exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩ + · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg) + · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg) + +theorem isGLB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} : + IsGLB s f ↔ ∀ a, IsGLB (Function.eval a '' s) (f a) := + @isLUB_pi α (fun a => (π a)ᵒᵈ) _ s f + +end Pi + +theorem IsGLB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) + {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) : IsGLB s x := + ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy => + hf.1 <| hx.2 <| Monotone.mem_lowerBounds_image (fun _ _ => hf.2) hy⟩ + +theorem IsLUB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) + {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x := + ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy => + hf.1 <| hx.2 <| Monotone.mem_upperBounds_image (fun _ _ => hf.2) hy⟩ + +lemma BddAbove.range_mono [Preorder β] {f : α → β} (g : α → β) (h : ∀ a, f a ≤ g a) + (hbdd : BddAbove (range g)) : BddAbove (range f) := by + obtain ⟨C, hC⟩ := hbdd + use C + rintro - ⟨x, rfl⟩ + exact (h x).trans (hC <| mem_range_self x) + +lemma BddBelow.range_mono [Preorder β] (f : α → β) {g : α → β} (h : ∀ a, f a ≤ g a) + (hbdd : BddBelow (range f)) : BddBelow (range g) := + BddAbove.range_mono (β := βᵒᵈ) f h hbdd + +lemma BddAbove.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} + (hf : BddAbove (range f)) (hg : Monotone g) : BddAbove (range (fun x => g (f x))) := by + change BddAbove (range (g ∘ f)) + simpa only [Set.range_comp] using hg.map_bddAbove hf + +lemma BddBelow.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} + (hf : BddBelow (range f)) (hg : Monotone g) : BddBelow (range (fun x => g (f x))) := by + change BddBelow (range (g ∘ f)) + simpa only [Set.range_comp] using hg.map_bddBelow hf diff --git a/Mathlib/Order/Bounds/OrderIso.lean b/Mathlib/Order/Bounds/OrderIso.lean index 913266a83c0cc..d3fda94252a64 100644 --- a/Mathlib/Order/Bounds/OrderIso.lean +++ b/Mathlib/Order/Bounds/OrderIso.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Yury Kudryashov -/ -import Mathlib.Order.Bounds.Basic +import Mathlib.Order.Bounds.Image import Mathlib.Order.Hom.Set /-! diff --git a/Mathlib/Order/CompleteLattice.lean b/Mathlib/Order/CompleteLattice.lean index 2d47e7b97ad07..b2c06f1f0a3d0 100644 --- a/Mathlib/Order/CompleteLattice.lean +++ b/Mathlib/Order/CompleteLattice.lean @@ -5,6 +5,7 @@ Authors: Johannes Hölzl -/ import Mathlib.Data.Bool.Set import Mathlib.Data.Nat.Set +import Mathlib.Data.Set.NAry import Mathlib.Data.Set.Prod import Mathlib.Data.ULift import Mathlib.Order.Bounds.Basic diff --git a/Mathlib/Order/GaloisConnection.lean b/Mathlib/Order/GaloisConnection.lean index 7420bcaf290d1..5995f271ba962 100644 --- a/Mathlib/Order/GaloisConnection.lean +++ b/Mathlib/Order/GaloisConnection.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl import Mathlib.Order.CompleteLattice import Mathlib.Order.Synonym import Mathlib.Order.Hom.Set -import Mathlib.Order.Bounds.Basic +import Mathlib.Order.Bounds.Image /-! # Galois connections, insertions and coinsertions From e06fe3e853532f908b0e52e0e65db18e4dd65a76 Mon Sep 17 00:00:00 2001 From: FR Date: Sat, 19 Oct 2024 16:03:52 +0000 Subject: [PATCH 03/10] =?UTF-8?q?chore:=20do=20not=20use=20`=C2=B7=20?= =?UTF-8?q?=E2=89=88=20=C2=B7`=20in=20`Quotient.mk=5Fout`=20(#17940)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Data/Quot.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean index 8dfbafe4dbf99..b9ff59544232d 100644 --- a/Mathlib/Data/Quot.lean +++ b/Mathlib/Data/Quot.lean @@ -355,7 +355,7 @@ noncomputable def Quotient.out {s : Setoid α} : Quotient s → α := theorem Quotient.out_eq {s : Setoid α} (q : Quotient s) : ⟦q.out⟧ = q := Quot.out_eq q -theorem Quotient.mk_out {s : Setoid α} (a : α) : (⟦a⟧ : Quotient s).out ≈ a := +theorem Quotient.mk_out {s : Setoid α} (a : α) : s (⟦a⟧ : Quotient s).out a := Quotient.exact (Quotient.out_eq _) theorem Quotient.mk_eq_iff_out {s : Setoid α} {x : α} {y : Quotient s} : From 2c5ee0d7efdb723afdf718540ddfabaa477015fc Mon Sep 17 00:00:00 2001 From: Yongle Hu Date: Sat, 19 Oct 2024 18:37:47 +0000 Subject: [PATCH 04/10] feat(RingTheory/Ideal/Over): define a class for an ideal lying over an ideal (#17415) Define `class` of an ideal lies over an ideal. Co-authored-by: Yongle Hu @mbkybky Co-authored-by: Jiedong Jiang @jjdishere Co-authored-by: Hu Yongle <2065545849@qq.com> Co-authored-by: Yongle Hu <2065545849@qq.com> --- Mathlib/RingTheory/FiniteType.lean | 5 + Mathlib/RingTheory/Ideal/Maps.lean | 16 +++ Mathlib/RingTheory/Ideal/Over.lean | 126 +++++++++++++++++- .../IsIntegralClosure/Basic.lean | 25 ++++ Mathlib/RingTheory/Noetherian.lean | 8 +- 5 files changed, 176 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean index 8eb4df96ddf80..97c79c644e56a 100644 --- a/Mathlib/RingTheory/FiniteType.lean +++ b/Mathlib/RingTheory/FiniteType.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin -/ import Mathlib.RingTheory.Adjoin.Tower +import Mathlib.RingTheory.Ideal.QuotientOperations /-! # Finiteness conditions in commutative algebra @@ -111,6 +112,10 @@ theorem trans [Algebra S A] [IsScalarTower R S A] (hRS : FiniteType R S) (hSA : FiniteType R A := ⟨fg_trans' hRS.1 hSA.1⟩ +instance quotient (R : Type*) {S : Type*} [CommSemiring R] [CommRing S] [Algebra R S] (I : Ideal S) + [h : Algebra.FiniteType R S] : Algebra.FiniteType R (S ⧸ I) := + Algebra.FiniteType.trans h inferInstance + /-- An algebra is finitely generated if and only if it is a quotient of a free algebra whose variables are indexed by a finset. -/ theorem iff_quotient_freeAlgebra : diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index faa5fc206c934..80ddaa2813840 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -846,3 +846,19 @@ def idealMap (I : Ideal R) : I →ₗ[R] I.map (algebraMap R S) := (fun _ ↦ Ideal.mem_map_of_mem _) end Algebra + +namespace NoZeroSMulDivisors + +theorem of_ker_algebraMap_eq_bot (R A : Type*) [CommRing R] [Semiring A] [Algebra R A] + [NoZeroDivisors A] (h : RingHom.ker (algebraMap R A) = ⊥) : NoZeroSMulDivisors R A := + of_algebraMap_injective ((RingHom.injective_iff_ker_eq_bot _).mpr h) + +theorem ker_algebraMap_eq_bot (R A : Type*) [CommRing R] [Ring A] [Nontrivial A] [Algebra R A] + [NoZeroSMulDivisors R A] : RingHom.ker (algebraMap R A) = ⊥ := + (RingHom.injective_iff_ker_eq_bot _).mp (algebraMap_injective R A) + +theorem iff_ker_algebraMap_eq_bot {R A : Type*} [CommRing R] [Ring A] [IsDomain A] [Algebra R A] : + NoZeroSMulDivisors R A ↔ RingHom.ker (algebraMap R A) = ⊥ := + iff_algebraMap_injective.trans (RingHom.injective_iff_ker_eq_bot (algebraMap R A)) + +end NoZeroSMulDivisors diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean index f8586e0f2559a..bbc4a002eeb87 100644 --- a/Mathlib/RingTheory/Ideal/Over.lean +++ b/Mathlib/RingTheory/Ideal/Over.lean @@ -3,7 +3,6 @@ Copyright (c) 2020 Anne Baanen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen -/ -import Mathlib.RingTheory.Algebraic import Mathlib.RingTheory.Localization.AtPrime import Mathlib.RingTheory.Localization.Integral @@ -429,4 +428,129 @@ lemma map_eq_top_iff {R S} [CommRing R] [CommRing S] end IsDomain +section ideal_liesOver + +section Semiring + +variable (A : Type*) [CommSemiring A] {B : Type*} [Semiring B] [Algebra A B] + (P : Ideal B) (p : Ideal A) + +/-- The ideal obtained by pulling back the ideal `P` from `B` to `A`. -/ +abbrev under : Ideal A := Ideal.comap (algebraMap A B) P + +theorem under_def : P.under A = Ideal.comap (algebraMap A B) P := rfl + +instance IsPrime.under [hP : P.IsPrime] : (P.under A).IsPrime := + hP.comap (algebraMap A B) + +variable {A} + +/-- `P` lies over `p` if `p` is the preimage of `P` of the `algebraMap`. -/ +class LiesOver : Prop where + over : p = P.under A + +instance over_under : P.LiesOver (P.under A) where over := rfl + +theorem over_def [P.LiesOver p] : p = P.under A := LiesOver.over + +theorem mem_of_liesOver [P.LiesOver p] (x : A) : x ∈ p ↔ algebraMap A B x ∈ P := by + rw [P.over_def p] + rfl + +end Semiring + +section CommSemiring + +variable {A : Type*} [CommSemiring A] {B : Type*} [CommSemiring B] {C : Type*} [Semiring C] + [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] + (𝔓 : Ideal C) (P : Ideal B) (p : Ideal A) + +@[simp] +theorem under_under : (𝔓.under B).under A = 𝔓.under A := by + simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq] + +theorem LiesOver.trans [𝔓.LiesOver P] [P.LiesOver p] : 𝔓.LiesOver p where + over := by rw [P.over_def p, 𝔓.over_def P, under_under] + +theorem LiesOver.tower_bot [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] : P.LiesOver p where + over := by rw [𝔓.over_def p, 𝔓.over_def P, under_under] + +variable (B) + +instance under_liesOver_of_liesOver [𝔓.LiesOver p] : (𝔓.under B).LiesOver p := + LiesOver.tower_bot 𝔓 (𝔓.under B) p + +end CommSemiring + +section CommRing + +namespace Quotient + +variable (R : Type*) [CommSemiring R] {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] + [Algebra R A] [Algebra R B] [IsScalarTower R A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] + +/-- If `P` lies over `p`, then canonically `B ⧸ P` is a `A ⧸ p`-algebra. -/ +instance algebraOfLiesOver : Algebra (A ⧸ p) (B ⧸ P) := + algebraQuotientOfLEComap (le_of_eq (P.over_def p)) + +instance isScalarTower_of_liesOver : IsScalarTower R (A ⧸ p) (B ⧸ P) := + IsScalarTower.of_algebraMap_eq' <| + congrArg (algebraMap B (B ⧸ P)).comp (IsScalarTower.algebraMap_eq R A B) + +/-- `B ⧸ P` is a finite `A ⧸ p`-module if `B` is a finite `A`-module. -/ +instance module_finite_of_liesOver [Module.Finite A B] : Module.Finite (A ⧸ p) (B ⧸ P) := + Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ P) + +example [Module.Finite A B] : Module.Finite (A ⧸ P.under A) (B ⧸ P) := inferInstance + +/-- `B ⧸ P` is a finitely generated `A ⧸ p`-algebra if `B` is a finitely generated `A`-algebra. -/ +instance algebra_finiteType_of_liesOver [Algebra.FiniteType A B] : + Algebra.FiniteType (A ⧸ p) (B ⧸ P) := + Algebra.FiniteType.of_restrictScalars_finiteType A (A ⧸ p) (B ⧸ P) + +/-- `B ⧸ P` is a Noetherian `A ⧸ p`-module if `B` is a Noetherian `A`-module. -/ +instance isNoetherian_of_liesOver [IsNoetherian A B] : IsNoetherian (A ⧸ p) (B ⧸ P) := + isNoetherian_of_tower A inferInstance + +theorem algebraMap_injective_of_liesOver : + Function.Injective (algebraMap (A ⧸ p) (B ⧸ P)) := by + rintro ⟨a⟩ ⟨b⟩ hab + apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _) + rw [RingHom.map_sub] + exact Quotient.eq.mp hab + +instance [P.IsPrime] : NoZeroSMulDivisors (A ⧸ p) (B ⧸ P) := + NoZeroSMulDivisors.of_algebraMap_injective (Quotient.algebraMap_injective_of_liesOver P p) + +end Quotient + +end CommRing + +section IsIntegral + +variable {A : Type*} [CommRing A] {B : Type*} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] + (P : Ideal B) (p : Ideal A) [P.LiesOver p] + +variable (A) in +/-- If `B` is an integral `A`-algebra, `P` is a maximal ideal of `B`, then the pull back of + `P` is also a maximal ideal of `A`. -/ +instance IsMaximal.under [P.IsMaximal] : (P.under A).IsMaximal := + isMaximal_comap_of_isIntegral_of_isMaximal P + +theorem IsMaximal.of_liesOver_isMaximal [hpm : p.IsMaximal] [P.IsPrime] : P.IsMaximal := by + rw [P.over_def p] at hpm + exact isMaximal_of_isIntegral_of_isMaximal_comap P hpm + +theorem IsMaximal.of_isMaximal_liesOver [P.IsMaximal] : p.IsMaximal := by + rw [P.over_def p] + exact isMaximal_comap_of_isIntegral_of_isMaximal P + +/-- `B ⧸ P` is an integral `A ⧸ p`-algebra if `B` is a integral `A`-algebra. -/ +instance Quotient.algebra_isIntegral_of_liesOver : Algebra.IsIntegral (A ⧸ p) (B ⧸ P) := + Algebra.IsIntegral.tower_top A + +end IsIntegral + +end ideal_liesOver + end Ideal diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean index 59406a95b8ec6..eabc18718c598 100644 --- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean +++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean @@ -558,6 +558,18 @@ nonrec theorem RingHom.IsIntegral.tower_bot (hg : Function.Injective g) haveI : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl fun x ↦ IsIntegral.tower_bot hg (hfg (g x)) +variable (T) in +/-- Let `T / S / R` be a tower of algebras, `T` is non-trivial and is a torsion free `S`-module, + then if `T` is an integral `R`-algebra, then `S` is an integral `R`-algebra. -/ +theorem Algebra.IsIntegral.tower_bot [Algebra R S] [Algebra R T] [Algebra S T] + [NoZeroSMulDivisors S T] [Nontrivial T] [IsScalarTower R S T] + [h : Algebra.IsIntegral R T] : Algebra.IsIntegral R S where + isIntegral := by + apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T) + (NoZeroSMulDivisors.algebraMap_injective S T) + rw [← IsScalarTower.algebraMap_eq R S T] + exact h.isIntegral + theorem IsIntegral.tower_bot_of_field {R A B : Type*} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x := @@ -571,6 +583,16 @@ theorem RingHom.isIntegralElem.of_comp {x : T} (h : (g.comp f).IsIntegralElem x) theorem RingHom.IsIntegral.tower_top (h : (g.comp f).IsIntegral) : g.IsIntegral := fun x ↦ RingHom.isIntegralElem.of_comp f g (h x) +variable (R) in +/-- Let `T / S / R` be a tower of algebras, `T` is an integral `R`-algebra, then it is integral + as an `S`-algebra. -/ +theorem Algebra.IsIntegral.tower_top [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] + [h : Algebra.IsIntegral R T] : Algebra.IsIntegral S T where + isIntegral := by + apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T) + rw [← IsScalarTower.algebraMap_eq R S T] + exact h.isIntegral + theorem RingHom.IsIntegral.quotient {I : Ideal S} (hf : f.IsIntegral) : (Ideal.quotientMap I f le_rfl).IsIntegral := by rintro ⟨x⟩ @@ -578,6 +600,9 @@ theorem RingHom.IsIntegral.quotient {I : Ideal S} (hf : f.IsIntegral) : refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩ simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx +instance {I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral R (A ⧸ I) := + Algebra.IsIntegral.trans A + instance Algebra.IsIntegral.quotient {I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) := ⟨RingHom.IsIntegral.quotient (algebraMap R A) Algebra.IsIntegral.isIntegral⟩ diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean index 903c8862e2b78..411b9fdf6c5a4 100644 --- a/Mathlib/RingTheory/Noetherian.lean +++ b/Mathlib/RingTheory/Noetherian.lean @@ -112,9 +112,11 @@ theorem isNoetherian_of_surjective (f : M →ₗ[R] P) (hf : LinearMap.range f = variable {M} -instance isNoetherian_quotient {R} [Ring R] {M} [AddCommGroup M] [Module R M] - (N : Submodule R M) [IsNoetherian R M] : IsNoetherian R (M ⧸ N) := - isNoetherian_of_surjective _ _ (LinearMap.range_eq_top.mpr N.mkQ_surjective) +instance isNoetherian_quotient {A M : Type*} [Ring A] [AddCommGroup M] [SMul R A] [Module R M] + [Module A M] [IsScalarTower R A M] (N : Submodule A M) [IsNoetherian R M] : + IsNoetherian R (M ⧸ N) := + isNoetherian_of_surjective M ((Submodule.mkQ N).restrictScalars R) <| + LinearMap.range_eq_top.mpr N.mkQ_surjective @[deprecated (since := "2024-04-27"), nolint defLemma] alias Submodule.Quotient.isNoetherian := isNoetherian_quotient From 37de4d77648a7d69b80dfc65ad9ef35e65696d2f Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Sat, 19 Oct 2024 19:08:11 +0000 Subject: [PATCH 05/10] feat(CategoryTheory/KanExtensions): Evaluating `lan` twice amounts to taking a colimit (#17531) --- .../Functor/KanExtension/Adjunction.lean | 44 +++++++++++++++++ .../Functor/KanExtension/Pointwise.lean | 48 +++++++++++++++++++ 2 files changed, 92 insertions(+) diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean index fe8433c905fb7..274273b8794c3 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean +++ b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean @@ -56,6 +56,28 @@ noncomputable def isPointwiseLeftKanExtensionLanUnit (LeftExtension.mk _ (L.lanUnit.app F)).IsPointwiseLeftKanExtension := isPointwiseLeftKanExtensionOfIsLeftKanExtension (F := F) _ (L.lanUnit.app F) +/-- If a left Kan extension is pointwise, then evaluating it at an object is isomorphic to +taking a colimit. -/ +noncomputable def lanObjObjIsoColimit (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] (X : D) : + (L.lan.obj F).obj X ≅ Limits.colimit (CostructuredArrow.proj L X ⋙ F) := + LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit (F := F) + (isPointwiseLeftKanExtensionLanUnit L F X) + +@[reassoc (attr := simp)] +lemma ι_lanObjObjIsoColimit_inv + (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] (X : D) (f : CostructuredArrow L X) : + Limits.colimit.ι _ f ≫ (L.lanObjObjIsoColimit F X).inv = + (L.lanUnit.app F).app f.left ≫ (L.lan.obj F).map f.hom := by + simp [lanObjObjIsoColimit, lanUnit] + +@[reassoc (attr := simp)] +lemma ι_lanObjObjIsoColimit_hom + (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] (X : D) (f : CostructuredArrow L X) : + (L.lanUnit.app F).app f.left ≫ (L.lan.obj F).map f.hom ≫ (L.lanObjObjIsoColimit F X).hom = + Limits.colimit.ι (CostructuredArrow.proj L X ⋙ F) f := + LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom (F := F) + (isPointwiseLeftKanExtensionLanUnit L F X) f + variable (H) in /-- The left Kan extension functor `L.Lan` is left adjoint to the precomposition by `L`. -/ @@ -162,6 +184,28 @@ noncomputable def isPointwiseRightKanExtensionRanCounit (RightExtension.mk _ (L.ranCounit.app F)).IsPointwiseRightKanExtension := isPointwiseRightKanExtensionOfIsRightKanExtension (F := F) _ (L.ranCounit.app F) +/-- If a right Kan extension is pointwise, then evaluating it at an object is isomorphic to +taking a limit. -/ +noncomputable def ranObjObjIsoLimit (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) : + (L.ran.obj F).obj X ≅ Limits.limit (StructuredArrow.proj X L ⋙ F) := + RightExtension.IsPointwiseRightKanExtensionAt.isoLimit (F := F) + (isPointwiseRightKanExtensionRanCounit L F X) + +@[reassoc (attr := simp)] +lemma ranObjObjIsoLimit_hom_π + (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) : + (L.ranObjObjIsoLimit F X).hom ≫ Limits.limit.π _ f = + (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right := by + simp [ranObjObjIsoLimit, ran, ranCounit] + +@[reassoc (attr := simp)] +lemma ranObjObjIsoLimit_inv_π + (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) : + (L.ranObjObjIsoLimit F X).inv ≫ (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right = + Limits.limit.π _ f := + RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π (F := F) + (isPointwiseRightKanExtensionRanCounit L F X) f + variable (H) in /-- The right Kan extension functor `L.ran` is right adjoint to the precomposition by `L`. -/ diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean index 9d4cb7a6c2ea1..a1a044d1a3846 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean +++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean @@ -98,6 +98,30 @@ lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app IsIso (E.hom.app X) := by simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal +namespace IsPointwiseLeftKanExtensionAt + +variable {E} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) + [HasColimit (CostructuredArrow.proj L Y ⋙ F)] + +/-- A pointwise left Kan extension of `F` along `L` applied to an object `Y` is isomorphic to +`colimit (CostructuredArrow.proj L Y ⋙ F)`. -/ +noncomputable def isoColimit : + E.right.obj Y ≅ colimit (CostructuredArrow.proj L Y ⋙ F) := + h.coconePointUniqueUpToIso (colimit.isColimit _) + +@[reassoc (attr := simp)] +lemma ι_isoColimit_inv (g : CostructuredArrow L Y) : + colimit.ι _ g ≫ h.isoColimit.inv = E.hom.app g.left ≫ E.right.map g.hom := + IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _ + +@[reassoc (attr := simp)] +lemma ι_isoColimit_hom (g : CostructuredArrow L Y) : + E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom = + colimit.ι (CostructuredArrow.proj L Y ⋙ F) g := by + simpa using h.comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) g + +end IsPointwiseLeftKanExtensionAt + /-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension when it is a pointwise left Kan extension at any object. -/ abbrev IsPointwiseLeftKanExtension := ∀ (Y : D), E.IsPointwiseLeftKanExtensionAt Y @@ -211,6 +235,30 @@ lemma IsPointwiseRightKanExtensionAt.isIso_hom_app IsIso (E.hom.app X) := by simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial +namespace IsPointwiseRightKanExtensionAt + +variable {E} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) + [HasLimit (StructuredArrow.proj Y L ⋙ F)] + +/-- A pointwise right Kan extension of `F` along `L` applied to an object `Y` is isomorphic to +`limit (StructuredArrow.proj Y L ⋙ F)`. -/ +noncomputable def isoLimit : + E.left.obj Y ≅ limit (StructuredArrow.proj Y L ⋙ F) := + h.conePointUniqueUpToIso (limit.isLimit _) + +@[reassoc (attr := simp)] +lemma isoLimit_hom_π (g : StructuredArrow Y L) : + h.isoLimit.hom ≫ limit.π _ g = E.left.map g.hom ≫ E.hom.app g.right := + IsLimit.conePointUniqueUpToIso_hom_comp _ _ _ + +@[reassoc (attr := simp)] +lemma isoLimit_inv_π (g : StructuredArrow Y L) : + h.isoLimit.inv ≫ E.left.map g.hom ≫ E.hom.app g.right = + limit.π (StructuredArrow.proj Y L ⋙ F) g := by + simpa using h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g + +end IsPointwiseRightKanExtensionAt + /-- A right extension `E : RightExtension L F` is a pointwise right Kan extension when it is a pointwise right Kan extension at any object. -/ abbrev IsPointwiseRightKanExtension := ∀ (Y : D), E.IsPointwiseRightKanExtensionAt Y From 19e2abfdd236a1feb36b33a6e219be17097d587f Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Sat, 19 Oct 2024 19:20:12 +0000 Subject: [PATCH 06/10] feat (AlgebraicGeometry/Modules): stalks of the sheaf `M^~` (#14247) Construct the isomorphism of $R$-modules from the stalk of the sheaf $M^{\~}$ on $Spec(R)$ to the localization $M_x$ as an $R$-module, where $R$ is a commutative ring and $M$ is an $R$-module. ## Main definition * `ModuleCat.tilde.stalkIso`: The isomorphism of `R`-modules from the stalk of `M^~` at `x` to the localization of `M` at the prime ideal corresponding to `x`. ## Technical note To get the `R`-module structure on the stalks on `M^~`, we had to define `ModuleCat.tildeInModuleCat`, which is `M^~` seen as sheaf of `R`-modules. We get it by applying a forgetful functor to `ModuleCat.tilde M`. Co-authored-by: Weihong Xu Co-authored-by: Sophie Morel Co-authored-by: Amelia Livingston This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024. Co-authored-by: morel Co-authored-by: Weihong Xu --- Mathlib/AlgebraicGeometry/Modules/Tilde.lean | 140 +++++++++++++++++++ 1 file changed, 140 insertions(+) diff --git a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean index 7fd34c2070d7a..d14b580db3d1a 100644 --- a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean +++ b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean @@ -22,6 +22,8 @@ such that `M^~(U)` is the set of dependent functions that are locally fractions. * `ModuleCat.tildeInType` : `M^~` as a sheaf of types groups. * `ModuleCat.tilde` : `M^~` as a sheaf of `𝒪_{Spec R}`-modules. +* `ModuleCat.tilde.stalkIso`: The isomorphism of `R`-modules from the stalk of `M^~` at `x` to +the localization of `M` at the prime ideal corresponding to `x`. ## Technical note @@ -252,6 +254,144 @@ noncomputable def localizationToStalk (x : PrimeSpectrum.Top R) : (TopCat.Presheaf.stalk (tildeInModuleCat M) x) := LocalizedModule.lift _ (toStalk M x) <| isUnit_toStalk M x + +/-- The ring homomorphism that takes a section of the structure sheaf of `R` on the open set `U`, +implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates +the section on the point corresponding to a given prime ideal. -/ +def openToLocalization (U : Opens (PrimeSpectrum R)) (x : PrimeSpectrum R) (hx : x ∈ U) : + (tildeInModuleCat M).obj (op U) ⟶ + ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) where + toFun s := (s.1 ⟨x, hx⟩ : _) + map_add' _ _ := rfl + map_smul' _ _ := rfl + +/-- +The morphism of `R`-modules from the stalk of `M^~` at `x` to the localization of `M` at the +prime ideal of `R` corresponding to `x`. +-/ +noncomputable def stalkToFiberLinearMap (x : PrimeSpectrum.Top R) : + (tildeInModuleCat M).stalk x ⟶ + ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) := + Limits.colimit.desc ((OpenNhds.inclusion x).op ⋙ (tildeInModuleCat M)) + { pt := _ + ι := + { app := fun U => openToLocalization M ((OpenNhds.inclusion _).obj U.unop) x U.unop.2 } } + +@[simp] +theorem germ_comp_stalkToFiberLinearMap (U : Opens (PrimeSpectrum.Top R)) (x) (hx : x ∈ U) : + (tildeInModuleCat M).germ U x hx ≫ stalkToFiberLinearMap M x = + openToLocalization M U x hx := + Limits.colimit.ι_desc _ _ + +@[simp] +theorem stalkToFiberLinearMap_germ (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) + (hx : x ∈ U) (s : (tildeInModuleCat M).1.obj (op U)) : + stalkToFiberLinearMap M x + (TopCat.Presheaf.germ (tildeInModuleCat M) U x hx s) = (s.1 ⟨x, hx⟩ : _) := + DFunLike.ext_iff.1 (germ_comp_stalkToFiberLinearMap M U x hx) s + +@[reassoc (attr := simp), elementwise (attr := simp)] +theorem toOpen_germ (U : Opens (PrimeSpectrum.Top R)) (x) (hx : x ∈ U) : + toOpen M U ≫ M.tildeInModuleCat.germ U x hx = toStalk M x := by + rw [← toOpen_res M ⊤ U (homOfLE le_top : U ⟶ ⊤), Category.assoc, Presheaf.germ_res]; rfl + +@[reassoc (attr := simp)] +theorem toStalk_comp_stalkToFiberLinearMap (x : PrimeSpectrum.Top R) : + toStalk M x ≫ stalkToFiberLinearMap M x = + LocalizedModule.mkLinearMap x.asIdeal.primeCompl M := by + rw [toStalk, Category.assoc, germ_comp_stalkToFiberLinearMap]; rfl + +theorem stalkToFiberLinearMap_toStalk (x : PrimeSpectrum.Top R) (m : M) : + (stalkToFiberLinearMap M x) (toStalk M x m) = + LocalizedModule.mk m 1 := + LinearMap.ext_iff.1 (toStalk_comp_stalkToFiberLinearMap M x) _ + +/-- +If `U` is an open subset of `Spec R`, `m` is an element of `M` and `r` is an element of `R` +that is invertible on `U` (i.e. does not belong to any prime ideal corresponding to a point +in `U`), this is `m / r` seen as a section of `M^~` over `U`. +-/ +def const (m : M) (r : R) (U : Opens (PrimeSpectrum.Top R)) + (hu : ∀ x ∈ U, r ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) : + (tildeInModuleCat M).obj (op U) := + ⟨fun x => LocalizedModule.mk m ⟨r, hu x x.2⟩, fun x => + ⟨U, x.2, 𝟙 _, m, r, fun y => ⟨hu _ y.2, by + simpa only [LocalizedModule.mkLinearMap_apply, LocalizedModule.smul'_mk, + LocalizedModule.mk_eq] using ⟨1, by simp⟩⟩⟩⟩ + +@[simp] +theorem const_apply (m : M) (r : R) (U : Opens (PrimeSpectrum.Top R)) + (hu : ∀ x ∈ U, r ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) (x : U) : + (const M m r U hu).1 x = LocalizedModule.mk m ⟨r, hu x x.2⟩ := + rfl + +theorem exists_const (U) (s : (tildeInModuleCat M).obj (op U)) (x : PrimeSpectrum.Top R) + (hx : x ∈ U) : + ∃ (V : Opens (PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f : M) (g : R) (hg : _), + const M f g V hg = (tildeInModuleCat M).map i.op s := + let ⟨V, hxV, iVU, f, g, hfg⟩ := s.2 ⟨x, hx⟩ + ⟨V, hxV, iVU, f, g, fun y hyV => (hfg ⟨y, hyV⟩).1, Subtype.eq <| funext fun y => by + obtain ⟨h1, (h2 : g • s.1 ⟨y, _⟩ = LocalizedModule.mk f 1)⟩ := hfg y + exact show LocalizedModule.mk f ⟨g, by exact h1⟩ = s.1 (iVU y) by + set x := s.1 (iVU y); change g • x = _ at h2; clear_value x + induction x using LocalizedModule.induction_on with + | h a b => + rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq] at h2 + obtain ⟨c, hc⟩ := h2 + exact LocalizedModule.mk_eq.mpr ⟨c, by simpa using hc.symm⟩⟩ + +@[simp] +theorem res_const (f : M) (g : R) (U hu V hv i) : + (tildeInModuleCat M).map i (const M f g U hu) = const M f g V hv := + rfl + +@[simp] +theorem localizationToStalk_mk (x : PrimeSpectrum.Top R) (f : M) (s : x.asIdeal.primeCompl) : + localizationToStalk M x (LocalizedModule.mk f s) = + (tildeInModuleCat M).germ (PrimeSpectrum.basicOpen (s : R)) x s.2 + (const M f s (PrimeSpectrum.basicOpen s) fun _ => id) := + (Module.End_isUnit_iff _ |>.1 (isUnit_toStalk M x s)).injective <| by + erw [← LinearMap.mul_apply] + simp only [IsUnit.mul_val_inv, LinearMap.one_apply, Module.algebraMap_end_apply] + show (M.tildeInModuleCat.germ ⊤ x ⟨⟩) ((toOpen M ⊤) f) = _ + rw [← map_smul] + fapply TopCat.Presheaf.germ_ext (W := PrimeSpectrum.basicOpen s.1) (hxW := s.2) + · exact homOfLE le_top + · exact 𝟙 _ + refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_ + show LocalizedModule.mk f 1 = s.1 • LocalizedModule.mk f _ + rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq] + exact ⟨1, by simp⟩ + +/-- +The isomorphism of `R`-modules from the stalk of `M^~` at `x` to the localization of `M` at the +prime ideal corresponding to `x`. +-/ +@[simps] +noncomputable def stalkIso (x : PrimeSpectrum.Top R) : + TopCat.Presheaf.stalk (tildeInModuleCat M) x ≅ + ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) where + hom := stalkToFiberLinearMap M x + inv := localizationToStalk M x + hom_inv_id := TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ext _ fun s ↦ by + show localizationToStalk M x (stalkToFiberLinearMap M x (M.tildeInModuleCat.germ U x hxU s)) = + M.tildeInModuleCat.germ U x hxU s + rw [stalkToFiberLinearMap_germ] + obtain ⟨V, hxV, iVU, f, g, (hg : V ≤ PrimeSpectrum.basicOpen _), hs⟩ := + exists_const _ _ s x hxU + rw [← res_apply M U V iVU s ⟨x, hxV⟩, ← hs, const_apply, localizationToStalk_mk] + exact (tildeInModuleCat M).germ_ext V hxV (homOfLE hg) iVU <| hs ▸ rfl + inv_hom_id := by ext x; exact x.induction_on (fun _ _ => by simp) + +instance (x : PrimeSpectrum.Top R) : + IsLocalizedModule x.asIdeal.primeCompl (toStalk M x) := by + convert IsLocalizedModule.of_linearEquiv + (hf := localizedModuleIsLocalizedModule (M := M) x.asIdeal.primeCompl) + (e := (stalkIso M x).symm.toLinearEquiv) + simp only [of_coe, show (stalkIso M x).symm.toLinearEquiv.toLinearMap = (stalkIso M x).inv by rfl, + stalkIso_inv] + erw [LocalizedModule.lift_comp] + end Tilde end ModuleCat From 721c01e4de26b2bb91e0c32ddcdcdf842e97c405 Mon Sep 17 00:00:00 2001 From: FR Date: Sat, 19 Oct 2024 19:27:05 +0000 Subject: [PATCH 07/10] chore(Data/Nat/{Bit, Bitwise}): make `Nat.bit_mod_two` `Nat.bit_eq_zero_iff` be `simp` (#17924) Also deprecate `Nat.bit_eq_zero`. It is identical to `Nat.bit_eq_zero_iff`. --- Mathlib/Data/Nat/Bits.lean | 1 + Mathlib/Data/Nat/Bitwise.lean | 13 +++++-------- Mathlib/Data/Nat/Multiplicity.lean | 7 +++---- 3 files changed, 9 insertions(+), 12 deletions(-) diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean index 71f01660fc34f..6ea51b387201e 100644 --- a/Mathlib/Data/Nat/Bits.lean +++ b/Mathlib/Data/Nat/Bits.lean @@ -328,6 +328,7 @@ theorem bit_cases_on_inj {motive : ℕ → Sort u} (H₁ H₂ : ∀ b n, motive ((fun n => bitCasesOn n H₁) = fun n => bitCasesOn n H₂) ↔ H₁ = H₂ := bit_cases_on_injective.eq_iff +@[simp] theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by constructor · cases b <;> simp [Nat.bit]; omega diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index cce15c0d55eee..07873ec6fd976 100644 --- a/Mathlib/Data/Nat/Bitwise.lean +++ b/Mathlib/Data/Nat/Bitwise.lean @@ -88,19 +88,18 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by cases a <;> cases b <;> simp [h2, h4] <;> split_ifs <;> simp_all (config := {decide := true}) [two_mul] +@[simp] lemma bit_mod_two (a : Bool) (x : ℕ) : bit a x % 2 = a.toNat := by cases a <;> simp [bit_val, mul_add_mod] -@[simp] lemma bit_mod_two_eq_zero_iff (a x) : bit a x % 2 = 0 ↔ !a := by - simp [bit_mod_two] + simp -@[simp] lemma bit_mod_two_eq_one_iff (a x) : bit a x % 2 = 1 ↔ a := by - simp [bit_mod_two] + simp @[simp] theorem lor_bit : ∀ a m b n, bit a m ||| bit b n = bit (a || b) (m ||| n) := @@ -142,12 +141,10 @@ theorem bit_false : bit false = (2 * ·) := theorem bit_true : bit true = (2 * · + 1) := rfl -@[simp] -theorem bit_eq_zero {n : ℕ} {b : Bool} : n.bit b = 0 ↔ n = 0 ∧ b = false := by - cases b <;> simp [bit, Nat.mul_eq_zero] +@[deprecated (since := "2024-10-19")] alias bit_eq_zero := bit_eq_zero_iff theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true := by - simpa only [not_and, Bool.not_eq_false] using (@bit_eq_zero n b).not + simp /-- An alternative for `bitwise_bit` which replaces the `f false false = false` assumption with assumptions that neither `bit a m` nor `bit b n` are `0` diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean index e86d693f824f5..61b86c32c88a8 100644 --- a/Mathlib/Data/Nat/Multiplicity.lean +++ b/Mathlib/Data/Nat/Multiplicity.lean @@ -6,7 +6,6 @@ Authors: Chris Hughes import Mathlib.Algebra.BigOperators.Intervals import Mathlib.Algebra.GeomSum import Mathlib.Algebra.Order.Ring.Abs -import Mathlib.Data.Nat.Bitwise import Mathlib.Data.Nat.Log import Mathlib.Data.Nat.Prime.Defs import Mathlib.Data.Nat.Digits @@ -282,10 +281,10 @@ theorem emultiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), emultiplic · intro b n ih h by_cases hn : n = 0 · subst hn - simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h - simp only [h, bit_true, factorial, mul_one, Nat.isUnit_iff, cast_one] + simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h + simp only [h, factorial, mul_one, Nat.isUnit_iff, cast_one] rw [Prime.emultiplicity_one] - · simp [zero_lt_one] + · exact zero_lt_one · decide have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) := by rw [prime_two.emultiplicity_factorial_mul] From fee48cc34cea5902fd163549acb01e413d7e7243 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Sat, 19 Oct 2024 19:57:03 +0000 Subject: [PATCH 08/10] =?UTF-8?q?feat(AlgebraicGeometry/ResidueField):=20c?= =?UTF-8?q?lassification=20of=20`Spec=20K=20=E2=9F=B6=20X`=20with=20`K`=20?= =?UTF-8?q?a=20field=20(#17768)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds more API for residue fields and in particular the classification of morphisms `Spec K ⟶ X` with `K` a field. From the valuative criterion project. Co-authored-by: Qi Ge Co-authored-by: Andrew Yang Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> Co-authored-by: Christian Merten --- .../Morphisms/ClosedImmersion.lean | 6 +- .../Morphisms/Preimmersion.lean | 27 +++++ Mathlib/AlgebraicGeometry/ResidueField.lean | 108 +++++++++++++++++- Mathlib/AlgebraicGeometry/Stalk.lean | 15 ++- 4 files changed, 150 insertions(+), 6 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean index 932325058e426..03d557fa0c469 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean @@ -3,12 +3,10 @@ Copyright (c) 2023 Jonas van der Schaaf. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Amelia Livingston, Christian Merten, Jonas van der Schaaf -/ -import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties import Mathlib.AlgebraicGeometry.Morphisms.FiniteType import Mathlib.AlgebraicGeometry.ResidueField -import Mathlib.RingTheory.RingHom.Surjective /-! @@ -134,6 +132,10 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion simp_rw [Scheme.stalkMap_comp] at h exact Function.Surjective.of_comp h +instance Spec_map_residue {X : Scheme.{u}} (x) : IsClosedImmersion (Spec.map (X.residue x)) := + IsClosedImmersion.spec_of_surjective (X.residue x) + Ideal.Quotient.mk_surjective + instance {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : QuasiCompact f where isCompact_preimage _ _ hU' := base_closed.isCompact_preimage hU' diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean index 9336dbb858cde..f504cc230196f 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean @@ -5,6 +5,7 @@ Authors: Andrew Yang -/ import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap import Mathlib.RingTheory.RingHom.Surjective +import Mathlib.RingTheory.SurjectiveOnStalks /-! @@ -95,6 +96,32 @@ theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] IsPreimmersion (f ≫ g) ↔ IsPreimmersion f := ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩ +lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) : + IsPreimmersion (Spec.map f) ↔ Embedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by + haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso := by + rw [← RingHom.toMorphismProperty_respectsIso_iff] + exact RingHom.surjective_respectsIso + refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, fun (x : PrimeSpectrum S) ↦ ?_⟩⟩ + · intro p hp + let e := Scheme.arrowStalkMapSpecIso f ⟨p, hp⟩ + apply ((RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).arrow_mk_iso_iff e).mp + exact h₂ ⟨p, hp⟩ + · let e := Scheme.arrowStalkMapSpecIso f x + apply ((RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).arrow_mk_iso_iff e).mpr + exact h₂ x.asIdeal x.isPrime + +lemma mk_Spec_map {R S : CommRingCat.{u}} {f : R ⟶ S} + (h₁ : Embedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) : + IsPreimmersion (Spec.map f) := + (Spec_map_iff f).mpr ⟨h₁, h₂⟩ + +lemma of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S] + [Algebra R S] [IsLocalization M S] : + IsPreimmersion (Spec.map (CommRingCat.ofHom <| algebraMap R S)) := + IsPreimmersion.mk_Spec_map + (PrimeSpectrum.localization_comap_embedding (R := R) S M) + (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S) + end IsPreimmersion end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/ResidueField.lean b/Mathlib/AlgebraicGeometry/ResidueField.lean index ac1d5d1e8dcc2..c7fcb54274fd0 100644 --- a/Mathlib/AlgebraicGeometry/ResidueField.lean +++ b/Mathlib/AlgebraicGeometry/ResidueField.lean @@ -3,8 +3,8 @@ Copyright (c) 2024 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ -import Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField import Mathlib.AlgebraicGeometry.Stalk +import Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField /-! @@ -20,12 +20,15 @@ The following are in the `AlgebraicGeometry.Scheme` namespace: - `AlgebraicGeometry.Scheme.Hom.residueFieldMap`: A morphism of schemes induce a homomorphism of residue fields. - `AlgebraicGeometry.Scheme.fromSpecResidueField`: The canonical map `Spec κ(x) ⟶ X`. +- `AlgebraicGeometry.Scheme.SpecToEquivOfField`: morphisms `Spec K ⟶ X` for a field `K` correspond + to pairs of `x : X` with embedding `κ(x) ⟶ K`. + -/ universe u -open CategoryTheory TopologicalSpace Opposite +open CategoryTheory TopologicalSpace Opposite LocalRing noncomputable section @@ -45,12 +48,37 @@ instance (x : X) : Field (X.residueField x) := def residue (X : Scheme.{u}) (x) : X.presheaf.stalk x ⟶ X.residueField x := LocalRing.residue _ +/-- See `AlgebraicGeometry.IsClosedImmersion.Spec_map_residue` for the stronger result that +`Spec.map (X.residue x)` is a closed immersion. -/ +instance {X : Scheme.{u}} (x) : IsPreimmersion (Spec.map (X.residue x)) := + IsPreimmersion.mk_Spec_map + (PrimeSpectrum.closedEmbedding_comap_of_surjective _ _ (Ideal.Quotient.mk_surjective)).embedding + (RingHom.surjectiveOnStalks_of_surjective (Ideal.Quotient.mk_surjective)) + +@[simp] +lemma Spec_map_residue_apply {X : Scheme.{u}} (x : X) (s : Spec (X.residueField x)) : + (Spec.map (X.residue x)).base s = closedPoint (X.presheaf.stalk x) := + LocalRing.PrimeSpectrum.comap_residue _ s + lemma residue_surjective (X : Scheme.{u}) (x) : Function.Surjective (X.residue x) := Ideal.Quotient.mk_surjective instance (X : Scheme.{u}) (x) : Epi (X.residue x) := ConcreteCategory.epi_of_surjective _ (X.residue_surjective x) +/-- If `K` is a field and `f : 𝒪_{X, x} ⟶ K` is a ring map, then this is the induced +map `κ(x) ⟶ K`. -/ +def descResidueField {K : Type u} [Field K] {X : Scheme.{u}} {x : X} + (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f] : + X.residueField x ⟶ .of K := + LocalRing.ResidueField.lift (S := K) f + +@[reassoc (attr := simp)] +lemma residue_descResidueField {K : Type u} [Field K] {X : Scheme.{u}} {x} + (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f] : + X.residue x ≫ X.descResidueField f = f := + RingHom.ext fun _ ↦ rfl + /-- If `U` is an open of `X` containing `x`, we have a canonical ring map from the sections over `U` to the residue field of `x`. @@ -171,6 +199,10 @@ lemma residue_residueFieldCongr (X : Scheme) {x y : X} (h : x = y) : subst h simp +lemma Hom.residueFieldMap_congr {f g : X ⟶ Y} (e : f = g) (x : X) : + f.residueFieldMap x = (Y.residueFieldCongr (by subst e; rfl)).hom ≫ g.residueFieldMap x := by + subst e; simp + end congr section fromResidueField @@ -178,7 +210,12 @@ section fromResidueField /-- The canonical map `Spec κ(x) ⟶ X`. -/ def fromSpecResidueField (X : Scheme) (x : X) : Spec (X.residueField x) ⟶ X := - Spec.map (CommRingCat.ofHom (X.residue x)) ≫ X.fromSpecStalk x + Spec.map (X.residue x) ≫ X.fromSpecStalk x + +instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecResidueField x) := by + dsimp only [Scheme.fromSpecResidueField] + rw [IsPreimmersion.comp_iff] + infer_instance @[reassoc (attr := simp)] lemma residueFieldCongr_fromSpecResidueField {x y : X} (h : x = y) : @@ -186,8 +223,73 @@ lemma residueFieldCongr_fromSpecResidueField {x y : X} (h : x = y) : X.fromSpecResidueField _ := by subst h; simp +@[reassoc] +lemma Hom.Spec_map_residueFieldMap_fromSpecResidueField (x : X) : + Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ = + X.fromSpecResidueField x ≫ f := by + dsimp only [fromSpecResidueField] + rw [Category.assoc, ← Spec_map_stalkMap_fromSpecStalk, ← Spec.map_comp_assoc, + ← Spec.map_comp_assoc] + rfl + +@[simp] +lemma fromSpecResidueField_apply (x : X.carrier) (s : Spec (X.residueField x)) : + (X.fromSpecResidueField x).base s = x := by + simp [fromSpecResidueField] + +lemma range_fromSpecResidueField (x : X.carrier) : + Set.range (X.fromSpecResidueField x).base = {x} := by + ext s + simp only [Set.mem_range, fromSpecResidueField_apply, Set.mem_singleton_iff, eq_comm (a := s)] + constructor + · rintro ⟨-, h⟩ + exact h + · rintro rfl + exact ⟨closedPoint (X.residueField x), rfl⟩ + +lemma descResidueField_fromSpecResidueField {K : Type*} [Field K] (X : Scheme) {x} + (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f] : + Spec.map (X.descResidueField f) ≫ + X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x := by + simp [fromSpecResidueField, ← Spec.map_comp_assoc] + +lemma descResidueField_stalkClosedPointTo_fromSpecResidueField + (K : Type u) [Field K] (X : Scheme.{u}) (f : Spec (.of K) ⟶ X) : + Spec.map (X.descResidueField (Scheme.stalkClosedPointTo f)) ≫ + X.fromSpecResidueField (f.base (closedPoint K)) = f := by + erw [X.descResidueField_fromSpecResidueField] + rw [Scheme.Spec_stalkClosedPointTo_fromSpecStalk] + end fromResidueField +/-- A helper lemma to work with `AlgebraicGeometry.Scheme.SpecToEquivOfField`. -/ +lemma SpecToEquivOfField_eq_iff {K : Type*} [Field K] {X : Scheme} + {f₁ f₂ : Σ x : X.carrier, X.residueField x ⟶ .of K} : + f₁ = f₂ ↔ ∃ e : f₁.1 = f₂.1, f₁.2 = (X.residueFieldCongr e).hom ≫ f₂.2 := by + constructor + · rintro rfl + simp + · obtain ⟨f, _⟩ := f₁ + obtain ⟨g, _⟩ := f₂ + rintro ⟨(rfl : f = g), h⟩ + simpa + +/-- For a field `K` and a scheme `X`, the morphisms `Spec K ⟶ X` bijectively correspond +to pairs of points `x` of `X` and embeddings `κ(x) ⟶ K`. -/ +def SpecToEquivOfField (K : Type u) [Field K] (X : Scheme.{u}) : + (Spec (.of K) ⟶ X) ≃ Σ x, X.residueField x ⟶ .of K where + toFun f := + ⟨_, X.descResidueField (Scheme.stalkClosedPointTo f)⟩ + invFun xf := Spec.map xf.2 ≫ X.fromSpecResidueField xf.1 + left_inv := Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField K X + right_inv f := by + rw [SpecToEquivOfField_eq_iff] + simp only [CommRingCat.coe_of, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply, + Scheme.fromSpecResidueField_apply, exists_true_left] + rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)] + erw [Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField] + simp + end Scheme end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/Stalk.lean b/Mathlib/AlgebraicGeometry/Stalk.lean index 251d379d23a14..92b56c3849cc3 100644 --- a/Mathlib/AlgebraicGeometry/Stalk.lean +++ b/Mathlib/AlgebraicGeometry/Stalk.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang, Fangming Li -/ import Mathlib.AlgebraicGeometry.AffineScheme +import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion /-! # Stalks of a Scheme @@ -68,6 +69,19 @@ noncomputable def Scheme.fromSpecStalk (X : Scheme) (x : X) : theorem IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {x : X} (hxU : x ∈ U) : hU.fromSpecStalk hxU = X.fromSpecStalk x := fromSpecStalk_eq .. +instance IsAffineOpen.fromSpecStalk_isPreimmersion {X : Scheme.{u}} {U : Opens X} + (hU : IsAffineOpen U) (x : X) (hx : x ∈ U) : IsPreimmersion (hU.fromSpecStalk hx) := by + dsimp [IsAffineOpen.fromSpecStalk] + haveI : IsPreimmersion (Spec.map (X.presheaf.germ U x hx)) := + letI : Algebra Γ(X, U) (X.presheaf.stalk x) := (X.presheaf.germ U x hx).toAlgebra + haveI := hU.isLocalization_stalk ⟨x, hx⟩ + IsPreimmersion.of_isLocalization (R := Γ(X, U)) (S := X.presheaf.stalk x) + (hU.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl + apply IsPreimmersion.comp + +instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecStalk x) := + IsAffineOpen.fromSpecStalk_isPreimmersion _ _ _ + lemma IsAffineOpen.fromSpecStalk_closedPoint {U : Opens X} (hU : IsAffineOpen U) {x : X} (hxU : x ∈ U) : (hU.fromSpecStalk hxU).base (closedPoint (X.presheaf.stalk x)) = x := by @@ -184,7 +198,6 @@ section stalkClosedPointTo variable {R} (f : Spec R ⟶ X) - namespace Scheme /-- From 227950d6190a304c6d697f37d74425bebe12917d Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 19 Oct 2024 21:32:09 +0000 Subject: [PATCH 09/10] feat: topology on module over topological ring (#16895) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Given a module over a topological ring, we define the module topology on this module to be the finest module making it into a topological module (i.e. the finest topology making addition and scalar multiplication continuous). NB this PR gave rise to a discussion about whether `⨆ a ∈ s, f a` or `sSup (f '' s)` should be the simp normal form, which was discussed on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/normal.20form.20for.20pullback.20of.20Inf.20of.20topologies/near/472676441) without any clear conclusion. Co-authored-by: Eric Wieser --- Mathlib.lean | 1 + Mathlib/Topology/Algebra/Module/Basic.lean | 13 + .../Algebra/Module/ModuleTopology.lean | 265 ++++++++++++++++++ Mathlib/Topology/Order.lean | 10 + 4 files changed, 289 insertions(+) create mode 100644 Mathlib/Topology/Algebra/Module/ModuleTopology.lean diff --git a/Mathlib.lean b/Mathlib.lean index 5fcbb05388323..c75bbf3dd05cd 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4553,6 +4553,7 @@ import Mathlib.Topology.Algebra.Module.Determinant import Mathlib.Topology.Algebra.Module.FiniteDimension import Mathlib.Topology.Algebra.Module.LinearPMap import Mathlib.Topology.Algebra.Module.LocallyConvex +import Mathlib.Topology.Algebra.Module.ModuleTopology import Mathlib.Topology.Algebra.Module.Multilinear.Basic import Mathlib.Topology.Algebra.Module.Multilinear.Bounded import Mathlib.Topology.Algebra.Module.Multilinear.Topology diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index 4296c9b917999..943df043c2c09 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -12,6 +12,7 @@ import Mathlib.Algebra.Algebra.Defs import Mathlib.LinearAlgebra.Projection import Mathlib.LinearAlgebra.Pi import Mathlib.LinearAlgebra.Finsupp +import Mathlib.Algebra.Module.Opposites /-! # Theory of topological modules and continuous linear maps. @@ -2379,4 +2380,16 @@ end Submodule end Quotient +namespace MulOpposite + +variable (R : Type*) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemiring R] + {M : Type*} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousSMul R M] + +/-- The function `op` is a continuous linear equivalence. -/ +@[simps!] +def opContinuousLinearEquiv : M ≃L[R] Mᵐᵒᵖ where + __ := MulOpposite.opLinearEquiv R + +end MulOpposite + set_option linter.style.longFile 2500 diff --git a/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/Mathlib/Topology/Algebra/Module/ModuleTopology.lean new file mode 100644 index 0000000000000..6fdfe9edc0b90 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ModuleTopology.lean @@ -0,0 +1,265 @@ +/- +Copyright (c) 2024 Kevin Buzzard. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Buzzard, Will Sawin +-/ +import Mathlib.Topology.Algebra.Module.Basic + +/-! +# A "module topology" for modules over a topological ring + +If `R` is a topological ring acting on an additive abelian group `A`, we define the +*module topology* to be the finest topology on `A` making both the maps +`• : R × A → A` and `+ : A × A → A` continuous (with all the products having the +product topology). Note that `- : A → A` is also automatically continuous as it is `a ↦ (-1) • a`. + +This topology was suggested by Will Sawin [here](https://mathoverflow.net/a/477763/1384). + + +## Mathematical details + +I (buzzard) don't know of any reference for this other than Sawin's mathoverflow answer, +so I expand some of the details here. + +First note that the definition makes sense in far more generality (for example `R` just needs to +be a topological space acting on an additive monoid). + +Next note that there *is* a finest topology with this property! Indeed, topologies on a fixed +type form a complete lattice (infinite infs and sups exist). So if `τ` is the Inf of all +the topologies on `A` which make `+` and `•` continuous, then the claim is that `+` and `•` +are still continuous for `τ` (note that topologies are ordered so that finer topologies +are smaller). To show `+ : A × A → A` is continuous we equivalently need to show +that the pushforward of the product topology `τ × τ` along `+` is `≤ τ`, and because `τ` is +the greatest lower bound of the topologies making `•` and `+` continuous, +it suffices to show that it's `≤ σ` for any topology `σ` on `A` which makes `+` and `•` continuous. +However pushforward and products are monotone, so `τ × τ ≤ σ × σ`, and the pushforward of +`σ × σ` is `≤ σ` because that's precisely the statement that `+` is continuous for `σ`. +The proof for `•` follows mutatis mutandis. + +A *topological module* for a topological ring `R` is an `R`-module `A` with a topology +making `+` and `•` continuous. The discussion so far has shown that the module topology makes +an `R`-module `A` into a topological module, and moreover is the finest topology with this property. + +A crucial observation is that if `M` is a topological `R`-module, if `A` is an `R`-module with no +topology, and if `φ : A → M` is linear, then the pullback of `M`'s topology to `A` is a topology +making `A` into a topological module. Let's for example check that `•` is continuous. +If `U ⊆ A` is open then by definition of the pullback topology, `U = φ⁻¹(V)` for some open `V ⊆ M`, +and now the pullback of `U` under `•` is just the pullback along the continuous map +`id × φ : R × A → R × M` of the preimage of `V` under the continuous map `• : R × M → M`, +so it's open. The proof for `+` is similar. + +As a consequence of this, we see that if `φ : A → M` is a linear map between topological `R`-modules +modules and if `A` has the module topology, then `φ` is automatically continuous. +Indeed the argument above shows that if `A → M` is linear then the module +topology on `A` is `≤` the pullback of the module topology on `M` (because it's the inf of a set +containing this topology) which is the definition of continuity. + +We also deduce that the module topology is a functor from the category of `R`-modules +(`R` a topological ring) to the category of topological `R`-modules, and it is perhaps +unsurprising that this is an adjoint to the forgetful functor. Indeed, if `A` is an `R`-module +and `M` is a topological `R`-module, then the previous paragraph shows that +the linear maps `A → M` are precisely the continuous linear maps +from (`A` with its module topology) to `M`, so the module topology is a left adjoint +to the forgetful functor. + +This file develops the theory of the module topology. We prove that the module topology on +`R` as a module over itself is `R`'s original topology, and that the module topology +is isomorphism-invariant. + +## Main theorems + +* `TopologicalSemiring.toIsModuleTopology : IsModuleTopology R R`. The module + topology on `R` is `R`'s topology. +* `IsModuleTopology.iso [IsModuleTopology R A] (e : A ≃L[R] B) : IsModuleTopology R B`. If `A` and + `B` are `R`-modules with topologies, if `e` is a topological isomorphism between them, + and if `A` has the module topology, then `B` has the module topology. + +## TODO + +Forthcoming PRs from the FLT repo will show that the module topology on a (binary or finite) product +of modules is the product of the module topologies, and that the module topology on the quotient +of a module `M` is the quotient topology when `M` is equipped with the module topology. + +We will also show the slightly more subtle result that if `M`, `N` and `P` are `R`-modules +equipped with the module topology and if furthermore `M` is finite as an `R`-module, +then any bilinear map `M × N → P` is continuous. + +As a consequence of this, we deduce that if `R` is a commutative topological ring +and `A` is an `R`-algebra of finite type as `R`-module, then `A` with its module +topology becomes a topological ring (i.e., multiplication is continuous). + +Other TODOs (not done in the FLT repo): + +* The module topology is a functor from the category of `R`-modules + to the category of topological `R`-modules, and it's an adjoint to the forgetful functor. + +-/ + +section basics + +/- +This section is just boilerplate, defining the module topology and making +some infrastructure. Note that we don't even need that `R` is a ring +in the main definitions, just that it acts on `A`. +-/ +variable (R : Type*) [TopologicalSpace R] (A : Type*) [Add A] [SMul R A] + +/-- The module topology, for a module `A` over a topological ring `R`. It's the finest topology +making addition and the `R`-action continuous, or equivalently the finest topology making `A` +into a topological `R`-module. More precisely it's the Inf of the set of +topologies with these properties; theorems `continuousSMul` and `continuousAdd` show +that the module topology also has these properties. -/ +abbrev moduleTopology : TopologicalSpace A := + sInf {t | @ContinuousSMul R A _ _ t ∧ @ContinuousAdd A t _} + +/-- A class asserting that the topology on a module over a topological ring `R` is +the module topology. See `moduleTopology` for more discussion of the module topology. -/ +class IsModuleTopology [τA : TopologicalSpace A] : Prop where + /-- Note that this should not be used directly, and `eq_moduleTopology`, which takes `R` and `A` + explicitly, should be used instead. -/ + eq_moduleTopology' : τA = moduleTopology R A + +theorem eq_moduleTopology [τA : TopologicalSpace A] [IsModuleTopology R A] : + τA = moduleTopology R A := + IsModuleTopology.eq_moduleTopology' (R := R) (A := A) + +/-- Scalar multiplication `• : R × A → A` is continuous if `R` is a topological +ring, and `A` is an `R` module with the module topology. -/ +theorem ModuleTopology.continuousSMul : @ContinuousSMul R A _ _ (moduleTopology R A) := + /- Proof: We need to prove that the product topology is finer than the pullback + of the module topology. But the module topology is an Inf and thus a limit, + and pullback is a right adjoint, so it preserves limits. + We must thus show that the product topology is finer than an Inf, so it suffices + to show it's a lower bound, which is not hard. All this is wrapped into + `continuousSMul_sInf`. + -/ + continuousSMul_sInf fun _ h ↦ h.1 + +/-- Addition `+ : A × A → A` is continuous if `R` is a topological +ring, and `A` is an `R` module with the module topology. -/ +theorem ModuleTopology.continuousAdd : @ContinuousAdd A (moduleTopology R A) _ := + continuousAdd_sInf fun _ h ↦ h.2 + +instance IsModuleTopology.toContinuousSMul [TopologicalSpace A] [IsModuleTopology R A] : + ContinuousSMul R A := eq_moduleTopology R A ▸ ModuleTopology.continuousSMul R A + +-- this can't be an instance because typclass inference can't be expected to find `R`. +theorem IsModuleTopology.toContinuousAdd [TopologicalSpace A] [IsModuleTopology R A] : + ContinuousAdd A := eq_moduleTopology R A ▸ ModuleTopology.continuousAdd R A + +/-- The module topology is `≤` any topology making `A` into a topological module. -/ +theorem moduleTopology_le [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A] : + moduleTopology R A ≤ τA := sInf_le ⟨inferInstance, inferInstance⟩ + +end basics + +namespace IsModuleTopology + +section basics + +variable {R : Type*} [TopologicalSpace R] + {A : Type*} [Add A] [SMul R A] [τA : TopologicalSpace A] + +/-- If `A` is a topological `R`-module and the identity map from (`A` with its given +topology) to (`A` with the module topology) is continuous, then the topology on `A` is +the module topology. -/ +theorem of_continuous_id [ContinuousAdd A] [ContinuousSMul R A] + (h : @Continuous A A τA (moduleTopology R A) id): + IsModuleTopology R A where + -- The topologies are equal because each is finer than the other. One inclusion + -- follows from the continuity hypothesis; the other is because the module topology + -- is the inf of all the topologies making `A` a topological module. + eq_moduleTopology' := le_antisymm (continuous_id_iff_le.1 h) (moduleTopology_le _ _) + +/-- The zero module has the module topology. -/ +instance instSubsingleton [Subsingleton A] : IsModuleTopology R A where + eq_moduleTopology' := Subsingleton.elim _ _ + +end basics + +section iso + +variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] +variable {A : Type*} [AddCommMonoid A] [Module R A] [τA : TopologicalSpace A] [IsModuleTopology R A] +variable {B : Type*} [AddCommMonoid B] [Module R B] [τB : TopologicalSpace B] + +/-- If `A` and `B` are `R`-modules, homeomorphic via an `R`-linear homeomorphism, and if +`A` has the module topology, then so does `B`. -/ +theorem iso (e : A ≃L[R] B) : IsModuleTopology R B where + eq_moduleTopology' := by + -- get these in before I start putting new topologies on A and B and have to use `@` + let g : A →ₗ[R] B := e + let g' : B →ₗ[R] A := e.symm + let h : A →+ B := e + let h' : B →+ A := e.symm + simp_rw [e.toHomeomorph.symm.inducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf] + apply congr_arg + ext τ -- from this point on the definitions of `g`, `g'` etc above don't work without `@`. + rw [Set.mem_image] + constructor + · rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩ + exact ⟨continuousSMul_induced g', continuousAdd_induced h'⟩ + · rintro ⟨h1, h2⟩ + use τ.induced e + rw [induced_compose] + refine ⟨⟨continuousSMul_induced g, continuousAdd_induced h⟩, ?_⟩ + nth_rw 2 [← induced_id (t := τ)] + simp + +end iso + +section self + +variable (R : Type*) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemiring R] + +/-! +We now fix once and for all a topological semiring `R`. + +We first prove that the module topology on `R` considered as a module over itself, +is `R`'s topology. +-/ + +/-- The topology on a topological semiring `R` agrees with the module topology when considering +`R` as an `R`-module in the obvious way (i.e., via `Semiring.toModule`). -/ +instance _root_.TopologicalSemiring.toIsModuleTopology : IsModuleTopology R R := by + /- By a previous lemma it suffices to show that the identity from (R,usual) to + (R, module topology) is continuous. -/ + apply of_continuous_id + /- + The idea needed here is to rewrite the identity function as the composite of `r ↦ (r,1)` + from `R` to `R × R`, and multiplication `R × R → R`. + -/ + rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp] + /- + It thus suffices to show that each of these maps are continuous. For this claim to even make + sense, we need to topologise `R × R`. The trick is to do this by giving the first `R` the usual + topology `τR` and the second `R` the module topology. To do this we have to "fight mathlib" + a bit with `@`, because there is more than one topology on `R` here. + -/ + apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R)) + (moduleTopology R R) + · /- + The map R × R → R is `•`, so by a fundamental property of the module topology, + this is continuous. -/ + exact @continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul .. + · /- + The map `R → R × R` sending `r` to `(r,1)` is a map into a product, so it suffices to show + that each of the two factors is continuous. But the first is the identity function + on `(R, usual topology)` and the second is a constant function. -/ + exact @Continuous.prod_mk _ _ _ _ (moduleTopology R R) _ _ _ continuous_id <| + @continuous_const _ _ _ (moduleTopology R R) _ + +end self + +section MulOpposite + +variable (R : Type*) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemiring R] + +/-- The module topology coming from the action of the topological ring `Rᵐᵒᵖ` on `R` + (via `Semiring.toOppositeModule`, i.e. via `(op r) • m = m * r`) is `R`'s topology. -/ +instance _root_.TopologicalSemiring.toOppositeIsModuleTopology : IsModuleTopology Rᵐᵒᵖ R := + .iso (MulOpposite.opContinuousLinearEquiv Rᵐᵒᵖ).symm + +end MulOpposite + +end IsModuleTopology diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean index 05a207e173994..173ade1245b1d 100644 --- a/Mathlib/Topology/Order.lean +++ b/Mathlib/Topology/Order.lean @@ -393,6 +393,11 @@ theorem induced_iInf {ι : Sort w} {t : ι → TopologicalSpace α} : (⨅ i, t i).induced g = ⨅ i, (t i).induced g := (gc_coinduced_induced g).u_iInf +@[simp] +theorem induced_sInf {s : Set (TopologicalSpace α)} : + TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s) := by + rw [sInf_eq_iInf', sInf_image', induced_iInf] + @[simp] theorem coinduced_bot : (⊥ : TopologicalSpace α).coinduced f = ⊥ := (gc_coinduced_induced f).l_bot @@ -406,6 +411,11 @@ theorem coinduced_iSup {ι : Sort w} {t : ι → TopologicalSpace α} : (⨆ i, t i).coinduced f = ⨆ i, (t i).coinduced f := (gc_coinduced_induced f).l_iSup +@[simp] +theorem coinduced_sSup {s : Set (TopologicalSpace α)} : + TopologicalSpace.coinduced f (sSup s) = sSup ((TopologicalSpace.coinduced f) '' s) := by + rw [sSup_eq_iSup', sSup_image', coinduced_iSup] + theorem induced_id [t : TopologicalSpace α] : t.induced id = t := TopologicalSpace.ext <| funext fun s => propext <| ⟨fun ⟨_, hs, h⟩ => h ▸ hs, fun hs => ⟨s, hs, rfl⟩⟩ From e9f0a88e5333f1edc2843a9164fb035a96406f5e Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 19 Oct 2024 21:53:49 +0000 Subject: [PATCH 10/10] feat(Normed/Group): add `nndist_one_right` etc (#17954) Add - `nndist_one_right`, `nndist_zero_right`, `nndist_one_left`, `nndist_zero_left`; - `edist_one_right`, `edist_zero_right`, `edist_one_left`, `edist_zero_left`. --- Mathlib/Analysis/Normed/Group/Basic.lean | 14 ++++++++++++++ Mathlib/MeasureTheory/Function/L1Space.lean | 6 ++---- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean index e379a64547598..b3742ef73f777 100644 --- a/Mathlib/Analysis/Normed/Group/Basic.lean +++ b/Mathlib/Analysis/Normed/Group/Basic.lean @@ -635,6 +635,13 @@ theorem nndist_eq_nnnorm_div (a b : E) : nndist a b = ‖a / b‖₊ := alias nndist_eq_nnnorm := nndist_eq_nnnorm_sub +@[to_additive (attr := simp)] +theorem nndist_one_right (a : E) : nndist a 1 = ‖a‖₊ := by simp [nndist_eq_nnnorm_div] + +@[to_additive (attr := simp)] +theorem edist_one_right (a : E) : edist a 1 = ‖a‖₊ := by + rw [edist_nndist, nndist_one_right] + @[to_additive (attr := simp) nnnorm_zero] theorem nnnorm_one' : ‖(1 : E)‖₊ = 0 := NNReal.eq norm_one' @@ -653,6 +660,13 @@ theorem nnnorm_mul_le' (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊ := theorem nnnorm_inv' (a : E) : ‖a⁻¹‖₊ = ‖a‖₊ := NNReal.eq <| norm_inv' a +@[to_additive (attr := simp)] +theorem nndist_one_left (a : E) : nndist 1 a = ‖a‖₊ := by simp [nndist_eq_nnnorm_div] + +@[to_additive (attr := simp)] +theorem edist_one_left (a : E) : edist 1 a = ‖a‖₊ := by + rw [edist_nndist, nndist_one_left] + open scoped symmDiff in @[to_additive] theorem nndist_mulIndicator (s t : Set α) (f : α → E) (x : α) : diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index 9994ae4d6e8b1..87c029742d760 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -1375,12 +1375,10 @@ theorem edist_toL1_toL1 (f g : α → β) (hf : Integrable f μ) (hg : Integrabl ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false] simp [edist_eq_coe_nnnorm_sub] -@[simp] theorem edist_toL1_zero (f : α → β) (hf : Integrable f μ) : edist (hf.toL1 f) 0 = ∫⁻ a, edist (f a) 0 ∂μ := by - simp only [toL1, Lp.edist_toLp_zero, eLpNorm, one_ne_zero, eLpNorm', one_toReal, ENNReal.rpow_one, - ne_eq, not_false_eq_true, div_self, ite_false] - simp [edist_eq_coe_nnnorm] + simp only [edist_zero_right, Lp.nnnorm_coe_ennreal, toL1_eq_mk, eLpNorm_aeeqFun] + apply eLpNorm_one_eq_lintegral_nnnorm variable {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β]