From 7cd93d73c0b7a21e0b63fe15c4d1188a820b2470 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 29 Nov 2023 18:18:37 +1100 Subject: [PATCH] chore: bump Std, changes for leanprover/std4#366 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit revert . fix a bit blech one more comment out broken and unused results chore: bump Std remove redundant simp lemmas cleanup fix: make `Nat.testBit_bitwise` a simp-lemma again. This fixes the Int.testbit_bitwise proofs fix `castNum_testBit` fix `testBit_eq_inth` fixes golf golf Apply suggestions from code review Co-authored-by: Eric Wieser fix whitespace fix name conflict more efficient restore lemma feat: Mapping extreme points under continuous maps (#8574) Prove that extreme points are preserved under affine equivalences, and the less trivial statement that a continuous affine map sends extreme points of a compact set to a superset of the extreme points of the image of that set. Also fix a few name and tweak the API a bit. Co-authored-by: Yury G. Kudryashov chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit (#8613) We allow the indexing category for the cofiltered limit in the result `Profinite.exists_locallyConstant` to live in a smaller universe than our profinite sets. feat(CategoryTheory): `Preregular` and `FinitaryPreExtensive` implies `Precoherent` (#8643) We prove some results about effective epimorphisms which allow us to deduce that a category which is `FinitaryPreExtensive` and `Preregular` is also `Precoherent`. feat(Analysis/Seminorm): add more `*ball_smul_*ball` (#8724) We had `ball_smul_ball` and `closedBall_smul_closedBall`. Add versions with mixed `ball` and `closedBall`. Also move this lemmas below and golf the proofs. feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739) fix breakage in BitVec lemmas --- Mathlib/Algebra/Lie/Killing.lean | 24 +-- Mathlib/Algebra/Module/LinearMap.lean | 25 ++- Mathlib/Analysis/Convex/Exposed.lean | 2 +- Mathlib/Analysis/Convex/Extreme.lean | 35 ++-- Mathlib/Analysis/Convex/KreinMilman.lean | 33 +++- Mathlib/Analysis/Seminorm.lean | 56 +++--- .../Limits/Shapes/Products.lean | 5 + .../Sites/EffectiveEpimorphic.lean | 169 ++++++++++++++---- .../Sites/RegularExtensive.lean | 42 ++++- Mathlib/Data/BitVec/Defs.lean | 8 +- Mathlib/Data/BitVec/Lemmas.lean | 37 +--- Mathlib/Data/Bool/Basic.lean | 16 -- Mathlib/Data/Int/Bitwise.lean | 10 +- Mathlib/Data/Nat/Basic.lean | 7 +- Mathlib/Data/Nat/Bitwise.lean | 71 ++------ Mathlib/Data/Nat/Order/Lemmas.lean | 5 - Mathlib/Data/Nat/Size.lean | 5 +- Mathlib/Data/Num/Lemmas.lean | 36 ++-- Mathlib/Init/Data/Nat/Bitwise.lean | 29 +-- Mathlib/LinearAlgebra/Dual.lean | 31 ++-- .../Topology/Category/Profinite/AsLimit.lean | 10 +- .../Topology/Category/Profinite/Basic.lean | 33 ++-- .../Category/Profinite/CofilteredLimit.lean | 16 +- .../Topology/Category/Profinite/Nobeling.lean | 4 +- .../Topology/Category/Profinite/Product.lean | 10 +- lake-manifest.json | 4 + 26 files changed, 437 insertions(+), 286 deletions(-) diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean index 2b5b750a7d96ae..6e6e38659238a2 100644 --- a/Mathlib/Algebra/Lie/Killing.lean +++ b/Mathlib/Algebra/Lie/Killing.lean @@ -242,7 +242,8 @@ lemma traceForm_eq_sum_weightSpaceOf [IsTriangularizable R L M] (z : L) : LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy] exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl) --- In characteristic zero a stronger result holds (no `⊓ LieAlgebra.center K L`) TODO prove this! +-- In characteristic zero (or even just `LinearWeights R L M`) a stronger result holds (no +-- `⊓ LieAlgebra.center R L`) TODO prove this using `LieModule.traceForm_eq_sum_finrank_nsmul_mul`. lemma lowerCentralSeries_one_inf_center_le_ker_traceForm : lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L ≤ LinearMap.ker (traceForm R L M) := by /- Sketch of proof (due to Zassenhaus): @@ -490,32 +491,33 @@ lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L] LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy] exact Finset.sum_congr (by simp) (fun χ _ ↦ traceForm_weightSpace_eq K L M χ x y) -@[simp] -lemma LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot [LieAlgebra.IsNilpotent K L] - [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L] - (h : LinearMap.ker (traceForm K L M) = ⊥) : - span K (range (weight.toLinear K L M)) = ⊤ := by +-- The reverse inclusion should also hold: TODO prove this! +lemma LieModule.dualAnnihilator_ker_traceForm_le_span_weight [LieAlgebra.IsNilpotent K L] + [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L] : + (LinearMap.ker (traceForm K L M)).dualAnnihilator ≤ span K (range (weight.toLinear K L M)) := by + intro g hg + simp only [Submodule.mem_dualAnnihilator, LinearMap.mem_ker] at hg by_contra contra obtain ⟨f : Module.Dual K (Module.Dual K L), hf, hf'⟩ := - Module.exists_dual_map_eq_bot_of_lt_top K (lt_top_iff_ne_top.mpr contra) inferInstance + Submodule.exists_dual_map_eq_bot_of_nmem contra inferInstance let x : L := (Module.evalEquiv K L).symm f replace hf' : ∀ χ ∈ weight K L M, χ x = 0 := by intro χ hχ change weight.toLinear K L M ⟨χ, hχ⟩ x = 0 rw [Module.apply_evalEquiv_symm_apply, ← Submodule.mem_bot (R := K), ← hf', Submodule.mem_map] exact ⟨weight.toLinear K L M ⟨χ, hχ⟩, Submodule.subset_span (mem_range_self _), rfl⟩ - have hx : x ≠ 0 := (LinearEquiv.map_ne_zero_iff _).mpr hf - apply hx - rw [← Submodule.mem_bot (R := K), ← h, LinearMap.mem_ker] + have hx : g x ≠ 0 := by simpa + refine hx (hg _ ?_) ext y rw [LieModule.traceForm_eq_sum_finrank_nsmul_mul, LinearMap.zero_apply] exact Finset.sum_eq_zero fun χ hχ ↦ by simp [hf' χ hχ] /-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular Killing form, the corresponding roots span the dual space of `H`. -/ +@[simp] lemma LieAlgebra.IsKilling.span_weight_eq_top [FiniteDimensional K L] [IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsTriangularizable K H L] : span K (range (weight.toLinear K H L)) = ⊤ := by - simp + simpa using LieModule.dualAnnihilator_ker_traceForm_le_span_weight K H L end Field diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index 12edcc9dd6b55f..bf1e3186147f98 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -62,10 +62,7 @@ open Function universe u u' v w x y z -variable {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} -variable {k : Type*} {S : Type*} {S₃ : Type*} {T : Type*} -variable {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} -variable {N₁ : Type*} {N₂ : Type*} {N₃ : Type*} {ι : Type*} +variable {R R₁ R₂ R₃ k S S₃ T M M₁ M₂ M₃ N₁ N₂ N₃ ι : Type*} /-- A map `f` between modules over a semiring is linear if it satisfies the two properties `f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `IsLinearMap R f` asserts this @@ -87,7 +84,7 @@ is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and `M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which `σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. -/ -structure LinearMap {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type*) +structure LinearMap {R S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type*) (M₂ : Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHom M M₂ where /-- A linear map preserves scalar multiplication. @@ -150,7 +147,6 @@ namespace SemilinearMapClass variable (F : Type*) variable [Semiring R] [Semiring S] variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] -variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] variable [Module R M] [Module R M₂] [Module S M₃] variable {σ : R →+* S} @@ -174,8 +170,23 @@ theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x) := by simp #align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_inv +/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/ +abbrev semilinearMap : M →ₛₗ[σ] M₃ where + toFun := f + map_add' := map_add f + map_smul' := map_smulₛₗ f + end SemilinearMapClass +namespace LinearMapClass +variable {F : Type*} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] + (f : F) [LinearMapClass F R M₁ M₂] + +/-- Reinterpret an element of a type of linear maps as a linear map. -/ +abbrev linearMap : M₁ →ₗ[R] M₂ := SemilinearMapClass.semilinearMap f + +end LinearMapClass + namespace LinearMap section AddCommMonoid @@ -566,7 +577,7 @@ theorem id_comp : id.comp f = f := #align linear_map.id_comp LinearMap.id_comp theorem comp_assoc - {R₄ : Type*} {M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄] + {R₄ M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) : diff --git a/Mathlib/Analysis/Convex/Exposed.lean b/Mathlib/Analysis/Convex/Exposed.lean index 0127c66091db29..ec319f3003a811 100644 --- a/Mathlib/Analysis/Convex/Exposed.lean +++ b/Mathlib/Analysis/Convex/Exposed.lean @@ -265,7 +265,7 @@ protected theorem isExtreme (hAB : IsExposed 𝕜 A B) : IsExtreme 𝕜 A B := b end IsExposed theorem exposedPoints_subset_extremePoints : A.exposedPoints 𝕜 ⊆ A.extremePoints 𝕜 := fun _ hx => - mem_extremePoints_iff_extreme_singleton.2 (mem_exposedPoints_iff_exposed_singleton.1 hx).isExtreme + (mem_exposedPoints_iff_exposed_singleton.1 hx).isExtreme.mem_extremePoints #align exposed_points_subset_extreme_points exposedPoints_subset_extremePoints end LinearOrderedRing diff --git a/Mathlib/Analysis/Convex/Extreme.lean b/Mathlib/Analysis/Convex/Extreme.lean index 5f230df5881a9c..ecb3290468a2b6 100644 --- a/Mathlib/Analysis/Convex/Extreme.lean +++ b/Mathlib/Analysis/Convex/Extreme.lean @@ -123,12 +123,7 @@ theorem isExtreme_biInter {F : Set (Set E)} (hF : F.Nonempty) (hA : ∀ B ∈ F, #align is_extreme_bInter isExtreme_biInter theorem isExtreme_sInter {F : Set (Set E)} (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExtreme 𝕜 A B) : - IsExtreme 𝕜 A (⋂₀ F) := by - obtain ⟨B, hB⟩ := hF - refine' ⟨(sInter_subset_of_mem hB).trans (hAF B hB).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ _⟩ - simp_rw [mem_sInter] at hxF ⊢ - have h := fun B hB ↦ (hAF B hB).2 hx₁A hx₂A (hxF B hB) hx - exact ⟨fun B hB ↦ (h B hB).1, fun B hB ↦ (h B hB).2⟩ + IsExtreme 𝕜 A (⋂₀ F) := by simpa [sInter_eq_biInter] using isExtreme_biInter hF hAF #align is_extreme_sInter isExtreme_sInter theorem mem_extremePoints : x ∈ A.extremePoints 𝕜 ↔ @@ -137,13 +132,15 @@ theorem mem_extremePoints : x ∈ A.extremePoints 𝕜 ↔ #align mem_extreme_points mem_extremePoints /-- x is an extreme point to A iff {x} is an extreme set of A. -/ -theorem mem_extremePoints_iff_extreme_singleton : x ∈ A.extremePoints 𝕜 ↔ IsExtreme 𝕜 A {x} := by - refine' ⟨_, fun hx ↦ ⟨singleton_subset_iff.1 hx.1, fun x₁ hx₁ x₂ hx₂ ↦ hx.2 hx₁ hx₂ rfl⟩⟩ +@[simp] lemma isExtreme_singleton : IsExtreme 𝕜 A {x} ↔ x ∈ A.extremePoints 𝕜 := by + refine ⟨fun hx ↦ ⟨singleton_subset_iff.1 hx.1, fun x₁ hx₁ x₂ hx₂ ↦ hx.2 hx₁ hx₂ rfl⟩, ?_⟩ rintro ⟨hxA, hAx⟩ use singleton_subset_iff.2 hxA rintro x₁ hx₁A x₂ hx₂A y (rfl : y = x) exact hAx hx₁A hx₂A -#align mem_extreme_points_iff_extreme_singleton mem_extremePoints_iff_extreme_singleton +#align mem_extreme_points_iff_extreme_singleton isExtreme_singleton + +alias ⟨IsExtreme.mem_extremePoints, _⟩ := isExtreme_singleton theorem extremePoints_subset : A.extremePoints 𝕜 ⊆ A := fun _ hx ↦ hx.1 @@ -167,8 +164,7 @@ theorem inter_extremePoints_subset_extremePoints_of_subset (hBA : B ⊆ A) : theorem IsExtreme.extremePoints_subset_extremePoints (hAB : IsExtreme 𝕜 A B) : B.extremePoints 𝕜 ⊆ A.extremePoints 𝕜 := - fun _ hx ↦ mem_extremePoints_iff_extreme_singleton.2 - (hAB.trans (mem_extremePoints_iff_extreme_singleton.1 hx)) + fun _ ↦ by simpa only [←isExtreme_singleton] using hAB.trans #align is_extreme.extreme_points_subset_extreme_points IsExtreme.extremePoints_subset_extremePoints theorem IsExtreme.extremePoints_eq (hAB : IsExtreme 𝕜 A B) : @@ -236,6 +232,21 @@ theorem extremePoints_pi (s : ∀ i, Set (π i)) : end OrderedSemiring +section OrderedRing +variable {L : Type*} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] + [LinearEquivClass L 𝕜 E F] + +lemma image_extremePoints (f : L) (s : Set E) : + f '' extremePoints 𝕜 s = extremePoints 𝕜 (f '' s) := by + ext b + obtain ⟨a, rfl⟩ := EquivLike.surjective f b + have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) := + image_openSegment _ (LinearMapClass.linearMap f).toAffineMap + simp only [mem_extremePoints, (EquivLike.surjective f).forall, + (EquivLike.injective f).mem_set_image, (EquivLike.injective f).eq_iff, ← this] + +end OrderedRing + section LinearOrderedRing variable [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] @@ -258,7 +269,7 @@ theorem mem_extremePoints_iff_forall_segment : x ∈ A.extremePoints 𝕜 ↔ theorem Convex.mem_extremePoints_iff_convex_diff (hA : Convex 𝕜 A) : x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ Convex 𝕜 (A \ {x}) := by - use fun hx ↦ ⟨hx.1, (mem_extremePoints_iff_extreme_singleton.1 hx).convex_diff hA⟩ + use fun hx ↦ ⟨hx.1, (isExtreme_singleton.2 hx).convex_diff hA⟩ rintro ⟨hxA, hAx⟩ refine' mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ _⟩ rw [convex_iff_segment_subset] at hAx diff --git a/Mathlib/Analysis/Convex/KreinMilman.lean b/Mathlib/Analysis/Convex/KreinMilman.lean index e8bb27ccdc62ee..1c880aa13fbfb6 100644 --- a/Mathlib/Analysis/Convex/KreinMilman.lean +++ b/Mathlib/Analysis/Convex/KreinMilman.lean @@ -5,6 +5,7 @@ Authors: Yaël Dillies -/ import Mathlib.Analysis.Convex.Exposed import Mathlib.Analysis.NormedSpace.HahnBanach.Separation +import Mathlib.Topology.Algebra.ContinuousAffineMap #align_import analysis.convex.krein_milman from "leanprover-community/mathlib"@"279297937dede7b1b3451b7b0f1786352ad011fa" @@ -51,20 +52,19 @@ See chapter 8 of [Barry Simon, *Convexity*][simon2011] -/ - open Set +open scoped Classical -open Classical - -variable {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] +variable {E F : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} + [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T1Space F] /-- **Krein-Milman lemma**: In a LCTVS, any nonempty compact set has an extreme point. -/ -theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty) : +theorem IsCompact.extremePoints_nonempty (hscomp : IsCompact s) (hsnemp : s.Nonempty) : (s.extremePoints ℝ).Nonempty := by let S : Set (Set E) := { t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t } rsuffices ⟨t, ⟨⟨x, hxt⟩, htclos, hst⟩, hBmin⟩ : ∃ t ∈ S, ∀ u ∈ S, u ⊆ t → u = t - · refine' ⟨x, mem_extremePoints_iff_extreme_singleton.2 _⟩ + · refine ⟨x, IsExtreme.mem_extremePoints ?_⟩ rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩] by_contra hyx obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx @@ -88,7 +88,7 @@ theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty) (hFS t.mem).2.1 obtain htu | hut := hF.total t.mem u.mem exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩] -#align is_compact.has_extreme_point IsCompact.has_extreme_point +#align is_compact.has_extreme_point IsCompact.extremePoints_nonempty /-- **Krein-Milman theorem**: In a LCTVS, any compact convex set is the closure of the convex hull of its extreme points. -/ @@ -101,7 +101,24 @@ theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩ obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn - obtain ⟨y, hy⟩ := (h.isCompact hscomp).has_extreme_point ⟨z, hzA, hz⟩ + obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩ linarith [hlr _ (subset_closure <| subset_convexHull _ _ <| h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA] #align closure_convex_hull_extreme_points closure_convexHull_extremePoints + +/-- A continuous affine map is surjective from the extreme points of a compact set to the extreme +points of the image of that set. This inclusion is in general strict. -/ +lemma surjOn_extremePoints_image (f : E →A[ℝ] F) (hs : IsCompact s) : + SurjOn f (extremePoints ℝ s) (extremePoints ℝ (f '' s)) := by + rintro w hw + -- The fiber of `w` is nonempty and compact + have ht : IsCompact {x ∈ s | f x = w} := hs.inter_right $ isClosed_singleton.preimage f.continuous + have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using extremePoints_subset hw + -- Hence by the Krein-Milman lemma it has an extreme point `x` + obtain ⟨x, ⟨hx, rfl⟩, hyt⟩ := ht.extremePoints_nonempty ht₀ + -- `f x = w` and `x` is an extreme point of `s`, so we're done + refine mem_image_of_mem _ ⟨hx, fun y hy z hz hxyz ↦ ?_⟩ + have := by simpa using image_openSegment _ f.toAffineMap y z + have := hw.2 (mem_image_of_mem _ hy) (mem_image_of_mem _ hz) $ by + rw [←this]; exact mem_image_of_mem _ hxyz + exact hyt ⟨hy, this.1⟩ ⟨hz, this.2⟩ hxyz diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index f2bb0a774471c7..09883f6bd7f202 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -919,31 +919,6 @@ theorem closedBall_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : exact closedBall_finset_sup_eq_iInter _ _ _ hr #align seminorm.closed_ball_finset_sup Seminorm.closedBall_finset_sup -theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) : - Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by - rw [Set.subset_def] - intro x hx - rw [Set.mem_smul] at hx - rcases hx with ⟨a, y, ha, hy, hx⟩ - rw [← hx, mem_ball_zero, map_smul_eq_mul] - gcongr - · exact mem_ball_zero_iff.mp ha - · exact p.mem_ball_zero.mp hy -#align seminorm.ball_smul_ball Seminorm.ball_smul_ball - -theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) : - Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) := by - rw [Set.subset_def] - intro x hx - rw [Set.mem_smul] at hx - rcases hx with ⟨a, y, ha, hy, hx⟩ - rw [← hx, mem_closedBall_zero, map_smul_eq_mul] - rw [mem_closedBall_zero_iff] at ha - gcongr - · exact (norm_nonneg a).trans ha - · exact p.mem_closedBall_zero.mp hy -#align seminorm.closed_ball_smul_closed_ball Seminorm.closedBall_smul_closedBall - @[simp] theorem ball_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r ≤ 0) : p.ball x r = ∅ := by ext @@ -959,6 +934,37 @@ theorem closedBall_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r < exact hr.trans_le (map_nonneg _ _) #align seminorm.closed_ball_eq_emptyset Seminorm.closedBall_eq_emptyset +theorem closedBall_smul_ball (p : Seminorm 𝕜 E) {r₁ : ℝ} (hr₁ : r₁ ≠ 0) (r₂ : ℝ) : + Metric.closedBall (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by + simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul] + refine fun a ha b hb ↦ mul_lt_mul' ha hb (map_nonneg _ _) ?_ + exact hr₁.lt_or_lt.resolve_left <| ((norm_nonneg a).trans ha).not_lt + +theorem ball_smul_closedBall (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ} (hr₂ : r₂ ≠ 0) : + Metric.ball (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by + simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff, + map_smul_eq_mul] + intro a ha b hb + rw [mul_comm, mul_comm r₁] + refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_lt.resolve_left ?_) + exact ((map_nonneg p b).trans hb).not_lt + +theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) : + Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by + rcases eq_or_ne r₂ 0 with rfl | hr₂ + · simp + · exact (smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans + (ball_smul_closedBall _ _ hr₂) +#align seminorm.ball_smul_ball Seminorm.ball_smul_ball + +theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) : + Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) := by + simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul] + intro a ha b hb + gcongr + exact (norm_nonneg _).trans ha +#align seminorm.closed_ball_smul_closed_ball Seminorm.closedBall_smul_closedBall + -- Porting note: TODO: make that an `iff` theorem neg_mem_ball_zero (r : ℝ) (hx : x ∈ ball p 0 r) : -x ∈ ball p 0 r := by simpa only [mem_ball_zero, map_neg_eq_map] using hx diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean index 66a5e489047c9e..fa98ff25ec3eaf 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean @@ -254,6 +254,11 @@ abbrev Sigma.desc {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) colimit.desc _ (Cofan.mk P p) #align category_theory.limits.sigma.desc CategoryTheory.Limits.Sigma.desc +instance {f : β → C} [HasCoproduct f] : IsIso (Sigma.desc (fun a ↦ Sigma.ι f a)) := by + convert IsIso.id _ + ext + simp + /-- A version of `Cocones.ext` for `Cofan`s. -/ @[simps!] def Cofan.ext {f : β → C} {c₁ c₂ : Cofan f} (e : c₁.pt ≅ c₂.pt) diff --git a/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean b/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean index c747b51ec38c4c..2908aaaaf725c1 100644 --- a/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean +++ b/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean @@ -6,6 +6,7 @@ Authors: Adam Topaz import Mathlib.CategoryTheory.Sites.Sieves import Mathlib.CategoryTheory.Limits.Shapes.KernelPair +import Mathlib.Tactic.ApplyFun /-! @@ -32,9 +33,10 @@ our notion of `EffectiveEpi` is often called "strict epi" in the literature. - [nlab: *Effective Epimorphism*](https://ncatlab.org/nlab/show/effective+epimorphism) and - [Stacks 00WP](https://stacks.math.columbia.edu/tag/00WP) for the standard definitions. --/ +## TODO +- Find sufficient conditions on functors to preserve/reflect effective epis. -set_option autoImplicit true +-/ namespace CategoryTheory @@ -303,12 +305,12 @@ attribute [nolint simpNF] EffectiveEpiFamily.fac_assoc /-- The effective epi family structure on the identity -/ -def effectiveEpiFamilyStructId : EffectiveEpiFamilyStruct (α : Unit → C) (fun _ => 𝟙 (α ())) where +def effectiveEpiFamilyStructId {α : Unit → C} : EffectiveEpiFamilyStruct α (fun _ => 𝟙 (α ())) where desc := fun e _ => e () fac := by aesop_cat uniq := by aesop_cat -instance : EffectiveEpiFamily (fun _ => X : Unit → C) (fun _ => 𝟙 X) := +instance {X : C} : EffectiveEpiFamily (fun _ => X : Unit → C) (fun _ => 𝟙 X) := ⟨⟨effectiveEpiFamilyStructId⟩⟩ example {B W : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) @@ -455,8 +457,9 @@ Given an `EffectiveEpiFamily X π` such that the coproduct of `X` exists, `Sigma `EffectiveEpi`. -/ noncomputable -def EffectiveEpiFamily_descStruct {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) - [HasCoproduct X] [EffectiveEpiFamily X π] : EffectiveEpiStruct (Sigma.desc π) where +def effectiveEpiStructDescOfEffectiveEpiFamily {B : C} {α : Type*} (X : α → C) + (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpiFamily X π] : + EffectiveEpiStruct (Sigma.desc π) where desc e h := EffectiveEpiFamily.desc X π (fun a ↦ Sigma.ι X a ≫ e) (fun a₁ a₂ g₁ g₂ hg ↦ by simp only [← Category.assoc] apply h (g₁ ≫ Sigma.ι X a₁) (g₂ ≫ Sigma.ι X a₂) @@ -478,26 +481,88 @@ def EffectiveEpiFamily_descStruct {B : C} {α : Type*} (X : α → C) (π : (a : instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpiFamily X π] : EffectiveEpi (Sigma.desc π) := - ⟨⟨EffectiveEpiFamily_descStruct X π⟩⟩ + ⟨⟨effectiveEpiStructDescOfEffectiveEpiFamily X π⟩⟩ + +/-- +This is an auxiliary lemma used twice in the definition of `EffectiveEpiFamilyOfEffectiveEpiDesc`. +It is the `h` hypothesis of `EffectiveEpi.desc` and `EffectiveEpi.fac`.  +-/ +theorem effectiveEpiFamilyStructOfEffectiveEpiDesc_aux {B : C} {α : Type*} {X : α → C} + {π : (a : α) → X a ⟶ B} [HasCoproduct X] + [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)] + [∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)] + [∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst (f := g) (g := (Sigma.ι X a)))] + {W : C} {e : (a : α) → X a ⟶ W} (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), + g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) {Z : C} + {g₁ g₂ : Z ⟶ ∐ fun b ↦ X b} (hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π) : + g₁ ≫ Sigma.desc e = g₂ ≫ Sigma.desc e := by + apply_fun ((Sigma.desc fun a ↦ pullback.fst (f := g₁) (g := (Sigma.ι X a))) ≫ ·) using + (fun a b ↦ (cancel_epi _).mp) + ext a + simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app] + rw [← Category.assoc, pullback.condition] + simp only [Category.assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app] + apply_fun ((Sigma.desc fun a ↦ pullback.fst (f := pullback.fst ≫ g₂) + (g := (Sigma.ι X a))) ≫ ·) using (fun a b ↦ (cancel_epi _).mp) + ext b + simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app] + simp only [← Category.assoc] + rw [(Category.assoc _ _ g₂), pullback.condition] + simp only [Category.assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app] + rw [← Category.assoc] + apply h + apply_fun (pullback.fst (f := g₁) (g := (Sigma.ι X a)) ≫ ·) at hg + rw [← Category.assoc, pullback.condition] at hg + simp only [Category.assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app] at hg + apply_fun ((Sigma.ι (fun a ↦ pullback _ _) b) ≫ (Sigma.desc fun a ↦ pullback.fst + (f := pullback.fst ≫ g₂) (g := (Sigma.ι X a))) ≫ ·) at hg + simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app] at hg + simp only [← Category.assoc] at hg + rw [(Category.assoc _ _ g₂), pullback.condition] at hg + simpa using hg + +/-- +If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of +the coproduct is effective epimorphic whenever `Sigma.desc` induces an effective epimorphism from +the coproduct itself. +-/ +noncomputable +def effectiveEpiFamilyStructOfEffectiveEpiDesc {B : C} {α : Type*} (X : α → C) + (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpi (Sigma.desc π)] + [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)] + [∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct (fun a ↦ pullback g (Sigma.ι X a))] + [∀ {Z : C} (g : Z ⟶ ∐ X), + Epi (Sigma.desc (fun a ↦ pullback.fst (f := g) (g := (Sigma.ι X a))))] : + EffectiveEpiFamilyStruct X π where + desc e h := EffectiveEpi.desc (Sigma.desc π) (Sigma.desc e) fun _ _ hg ↦ + effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg + fac e h a := by + rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e), + Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦ + effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)] + uniq _ _ _ hm := by + apply EffectiveEpi.uniq (Sigma.desc π) + ext + simpa using hm _ /-- An `EffectiveEpiFamily` consisting of a single `EffectiveEpi` -/ noncomputable -def EffectiveEpi_familyStruct {B X : C} (f : X ⟶ B) [EffectiveEpi f] : +def effectiveEpiFamilyStructSingletonOfEffectiveEpi {B X : C} (f : X ⟶ B) [EffectiveEpi f] : EffectiveEpiFamilyStruct (fun () ↦ X) (fun () ↦ f) where desc e h := EffectiveEpi.desc f (e ()) (fun g₁ g₂ hg ↦ h () () g₁ g₂ hg) fac e h := fun _ ↦ EffectiveEpi.fac f (e ()) (fun g₁ g₂ hg ↦ h () () g₁ g₂ hg) uniq e h m hm := by apply EffectiveEpi.uniq f (e ()) (h () ()); exact hm () instance {B X : C} (f : X ⟶ B) [EffectiveEpi f] : EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f) := - ⟨⟨EffectiveEpi_familyStruct f⟩⟩ + ⟨⟨effectiveEpiFamilyStructSingletonOfEffectiveEpi f⟩⟩ /-- A single element `EffectiveEpiFamily` constists of an `EffectiveEpi` -/ noncomputable -def EffectiveEpiStruct_ofFamily {B X : C} (f : X ⟶ B) +def effectiveEpiStructOfEffectiveEpiFamilySingleton {B X : C} (f : X ⟶ B) [EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f)] : EffectiveEpiStruct f where desc e h := EffectiveEpiFamily.desc @@ -509,9 +574,9 @@ def EffectiveEpiStruct_ofFamily {B X : C} (f : X ⟶ B) instance {B X : C} (f : X ⟶ B) [EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f)] : EffectiveEpi f := - ⟨⟨EffectiveEpiStruct_ofFamily f⟩⟩ + ⟨⟨effectiveEpiStructOfEffectiveEpiFamilySingleton f⟩⟩ -lemma effectiveEpi_iff_effectiveEpiFamily {B X : C} (f : X ⟶ B) : +theorem effectiveEpi_iff_effectiveEpiFamily {B X : C} (f : X ⟶ B) : EffectiveEpi f ↔ EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f) := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩ @@ -520,7 +585,7 @@ A family of morphisms with the same target inducing an isomorphism from the copr is an `EffectiveEpiFamily`. -/ noncomputable -def EffectiveEpiFamilyStruct_of_isIso_desc {B : C} {α : Type*} (X : α → C) +def effectiveEpiFamilyStructOfIsIsoDesc {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [IsIso (Sigma.desc π)] : EffectiveEpiFamilyStruct X π where desc e _ := (asIso (Sigma.desc π)).inv ≫ (Sigma.desc e) @@ -540,34 +605,51 @@ def EffectiveEpiFamilyStruct_of_isIso_desc {B : C} {α : Type*} (X : α → C) instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [IsIso (Sigma.desc π)] : EffectiveEpiFamily X π := - ⟨⟨EffectiveEpiFamilyStruct_of_isIso_desc X π⟩⟩ + ⟨⟨effectiveEpiFamilyStructOfIsIsoDesc X π⟩⟩ /-- The identity is an effective epi. -/ -def EffectiveEpiStructId {X : C} : EffectiveEpiStruct (𝟙 X) where - desc e _ := e - fac _ _ := by simp only [Category.id_comp] - uniq _ _ _ h := by simp only [Category.id_comp] at h; exact h - -instance {X : C} : EffectiveEpi (𝟙 X) := ⟨⟨EffectiveEpiStructId⟩⟩ - -end instances +noncomputable +def effectiveEpiStructOfIsIso {X Y : C} (f : X ⟶ Y) [IsIso f] : EffectiveEpiStruct f where + desc e _ := inv f ≫ e + fac _ _ := by simp + uniq _ _ _ h := by simpa using h -section Epi +instance {X Y : C} (f : X ⟶ Y) [IsIso f] : EffectiveEpi f := ⟨⟨effectiveEpiStructOfIsIso f⟩⟩ -variable [HasFiniteCoproducts C] (h : ∀ {α : Type} [Fintype α] {B : C} - (X : α → C) (π : (a : α) → (X a ⟶ B)), EffectiveEpiFamily X π ↔ Epi (Sigma.desc π )) +/-- +A split epi followed by an effective epi is an effective epi. This version takes an explicit section +to the split epi, and is mainly used to define `effectiveEpiStructCompOfEffectiveEpiSplitEpi`, +which takes a `IsSplitEpi` instance instead. +-/ +noncomputable +def effectiveEpiStructCompOfEffectiveEpiSplitEpi' {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) (i : X ⟶ Y) + (hi : i ≫ g = 𝟙 _) [EffectiveEpi f] : EffectiveEpiStruct (g ≫ f) where + desc e w := EffectiveEpi.desc f (i ≫ e) fun g₁ g₂ _ ↦ (by + simp only [← Category.assoc] + apply w (g₁ ≫ i) (g₂ ≫ i) + simpa [← Category.assoc, hi]) + fac e w := by + simp only [Category.assoc, EffectiveEpi.fac] + rw [← Category.id_comp e, ← Category.assoc, ← Category.assoc] + apply w + simp only [Category.comp_id, Category.id_comp, ← Category.assoc] + aesop + uniq _ _ _ hm := by + apply EffectiveEpi.uniq f + rw [← hm, ← Category.assoc, ← Category.assoc, hi, Category.id_comp] + +/-- A split epi followed by an effective epi is an effective epi. -/ +noncomputable +def effectiveEpiStructCompOfEffectiveEpiSplitEpi {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) [IsSplitEpi g] + [EffectiveEpi f] : EffectiveEpiStruct (g ≫ f) := + effectiveEpiStructCompOfEffectiveEpiSplitEpi' f g + (IsSplitEpi.exists_splitEpi (f := g)).some.section_ + (IsSplitEpi.exists_splitEpi (f := g)).some.id -lemma effectiveEpi_iff_epi {X Y : C} (f : X ⟶ Y) : EffectiveEpi f ↔ Epi f := by - rw [effectiveEpi_iff_effectiveEpiFamily, h] - have w : f = (Limits.Sigma.ι (fun () ↦ X) ()) ≫ (Limits.Sigma.desc (fun () ↦ f)) - · simp only [Limits.colimit.ι_desc, Limits.Cofan.mk_pt, Limits.Cofan.mk_ι_app] - refine ⟨?_, fun _ ↦ epi_of_epi_fac w.symm⟩ - intro - rw [w] - have : Epi (Limits.Sigma.ι (fun () ↦ X) ()) := ⟨fun _ _ h ↦ by ext; exact h⟩ - exact epi_comp _ _ +instance {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) [IsSplitEpi g] [EffectiveEpi f] : + EffectiveEpi (g ≫ f) := ⟨⟨effectiveEpiStructCompOfEffectiveEpiSplitEpi f g⟩⟩ -end Epi +end instances section Regular @@ -615,4 +697,21 @@ noncomputable instance regularEpiOfEffectiveEpi {B X : C} (f : X ⟶ B) [HasPull end Regular +section Epi + +variable [HasFiniteCoproducts C] (h : ∀ {α : Type} [Fintype α] {B : C} + (X : α → C) (π : (a : α) → (X a ⟶ B)), EffectiveEpiFamily X π ↔ Epi (Sigma.desc π )) + +lemma effectiveEpi_iff_epi {X Y : C} (f : X ⟶ Y) : EffectiveEpi f ↔ Epi f := by + rw [effectiveEpi_iff_effectiveEpiFamily, h] + have w : f = (Limits.Sigma.ι (fun () ↦ X) ()) ≫ (Limits.Sigma.desc (fun () ↦ f)) + · simp only [Limits.colimit.ι_desc, Limits.Cofan.mk_pt, Limits.Cofan.mk_ι_app] + refine ⟨?_, fun _ ↦ epi_of_epi_fac w.symm⟩ + intro + rw [w] + have : Epi (Limits.Sigma.ι (fun () ↦ X) ()) := ⟨fun _ _ h ↦ by ext; exact h⟩ + exact epi_comp _ _ + +end Epi + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Sites/RegularExtensive.lean b/Mathlib/CategoryTheory/Sites/RegularExtensive.lean index 62ab4fe4a8b6d7..615471555b5a23 100644 --- a/Mathlib/CategoryTheory/Sites/RegularExtensive.lean +++ b/Mathlib/CategoryTheory/Sites/RegularExtensive.lean @@ -27,6 +27,8 @@ disjoint. ## Main results +* `instance : Precoherent C` given `Preregular C` and `FinitaryPreExtensive C`. + * `extensive_union_regular_generates_coherent`: the union of the regular and extensive coverages generates the coherent topology on `C` if `C` is precoherent, preextensive and preregular. @@ -40,11 +42,6 @@ disjoint. * `isSheaf_iff_preservesFiniteProducts`: In a finitary extensive category, the sheaves for the extensive topology are precisely those preserving finite products. -TODO: figure out under what conditions `Preregular` and `Extensive` are implied by `Precoherent` and -vice versa. - -TODO: refactor the section `RegularSheaves` to use the new `Arrows` sheaf API. - -/ universe v u w @@ -77,6 +74,16 @@ class Preregular : Prop where exists_fac : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], (∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f) +instance [Precoherent C] [HasFiniteCoproducts C] : Preregular C where + exists_fac {X Y Z} f g _ := by + have hp := Precoherent.pullback f PUnit (fun () ↦ Z) (fun () ↦ g) + simp only [exists_const] at hp + rw [← effectiveEpi_iff_effectiveEpiFamily g] at hp + obtain ⟨β, _, X₂, π₂, h, ι, hι⟩ := hp inferInstance + refine ⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩ + ext b + simpa using hι b + /-- The regular coverage on a regular category `C`. -/ @@ -117,9 +124,32 @@ def extensiveCoverage [FinitaryPreExtensive C] : Coverage C where rw [hS] exact Presieve.ofArrows.mk a +theorem effectiveEpi_desc_iff_effectiveEpiFamily [FinitaryPreExtensive C] {α : Type} [Fintype α] + {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) : + EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π := by + exact ⟨fun h ↦ ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _ (fun g ↦ + (FinitaryPreExtensive.sigma_desc_iso (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩, + fun _ ↦ inferInstance⟩ + +instance [FinitaryPreExtensive C] [Preregular C] : Precoherent C where + pullback {B₁ B₂} f α _ X₁ π₁ h := by + refine ⟨α, inferInstance, ?_⟩ + obtain ⟨Y, g, _, g', hg⟩ := Preregular.exists_fac f (Sigma.desc π₁) + let X₂ := fun a ↦ pullback g' (Sigma.ι X₁ a) + let π₂ := fun a ↦ pullback.fst (f := g') (g := Sigma.ι X₁ a) ≫ g + let π' := fun a ↦ pullback.fst (f := g') (g := Sigma.ι X₁ a) + have _ := FinitaryPreExtensive.sigma_desc_iso (fun a ↦ Sigma.ι X₁ a) g' inferInstance + refine ⟨X₂, π₂, ?_, ?_⟩ + · have : (Sigma.desc π' ≫ g) = Sigma.desc π₂ := by ext; simp + rw [← effectiveEpi_desc_iff_effectiveEpiFamily, ← this] + infer_instance + · refine ⟨id, fun b ↦ pullback.snd, fun b ↦ ?_⟩ + simp only [id_eq, Category.assoc, ← hg] + rw [← Category.assoc, pullback.condition] + simp /-- The union of the extensive and regular coverages generates the coherent topology on `C`. -/ -lemma extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] [Precoherent C] : +lemma extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] : ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck = (coherentTopology C) := by ext B S diff --git a/Mathlib/Data/BitVec/Defs.lean b/Mathlib/Data/BitVec/Defs.lean index 050811911d6234..3f32799256e6cf 100644 --- a/Mathlib/Data/BitVec/Defs.lean +++ b/Mathlib/Data/BitVec/Defs.lean @@ -58,9 +58,11 @@ namespace Std.BitVec /-! ### Arithmetic operators -/ #align bitvec.neg Std.BitVec.neg -/-- Add with carry (no overflow) -/ -def adc {n} (x y : BitVec n) (c : Bool) : BitVec (n+1) := - ofFin (x.toNat + y.toNat + c.toNat) +/-- Add with carry (no overflow) + +See also `Std.BitVec.adc`, which stores the carry bit separately. -/ +def adc' {n} (x y : BitVec n) (c : Bool) : BitVec (n+1) := + let a := x.adc y c; .cons a.1 a.2 #align bitvec.adc Std.BitVec.adc #align bitvec.add Std.BitVec.add diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index ab9898dc426e4b..b35946fafdf14e 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -37,20 +37,10 @@ theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y := theorem toNat_lt_toNat {x y : BitVec w} : x.toNat < y.toNat ↔ x < y := Iff.rfl -@[simp] -lemma ofNat_eq_mod_two_pow (n : Nat) : (BitVec.ofNat w n).toNat = n % 2^w := rfl - -lemma toNat_ofNat {m} (h : m < 2^w) : (BitVec.ofNat w m).toNat = m := Fin.val_cast_of_lt h - -@[simp] -lemma toNat_ofFin (x : Fin (2^w)) : (ofFin x).toNat = x.val := rfl +attribute [simp] toNat_ofNat toNat_ofFin -theorem toNat_append (msbs : BitVec w) (lsbs : BitVec v) : - (msbs ++ lsbs).toNat = msbs.toNat <<< v ||| lsbs.toNat := by - rcases msbs with ⟨msbs, hm⟩ - rcases lsbs with ⟨lsbs, hl⟩ - simp only [HAppend.hAppend, append, toNat_ofFin] - rw [toNat_ofNat (Nat.add_comm w v ▸ append_lt hl hm)] +lemma toNat_ofNat_of_lt {m} (h : m < 2^w) : (BitVec.ofNat w m).toNat = m := by + simp only [toNat_ofNat, mod_eq_of_lt h] #noalign bitvec.bits_to_nat_to_bool @@ -66,14 +56,9 @@ lemma extractLsb_eq {w : ℕ} (hi lo : ℕ) (a : BitVec w) : theorem toNat_extractLsb' {i j} {x : BitVec w} : (extractLsb' i j x).toNat = x.toNat / 2 ^ i % (2 ^ j) := by - simp only [extractLsb', ofNat_eq_mod_two_pow, shiftRight_eq_div_pow] - -theorem getLsb_eq_testBit {i} {x : BitVec w} : getLsb x i = x.toNat.testBit i := by - simp only [getLsb, Nat.shiftLeft_eq, one_mul, Nat.and_two_pow] - cases' testBit (BitVec.toNat x) i - <;> simp [pos_iff_ne_zero.mp (two_pow_pos i)] + simp only [extractLsb', toNat_ofNat, shiftRight_eq_div_pow] -theorem ofFin_val {n : ℕ} (i : Fin <| 2 ^ n) : (ofFin i).toNat = i.val := by +theorem ofFin_val {n : ℕ} (i : Fin <| 2 ^ n) : (ofFin i).toNat = i.val := rfl #align bitvec.of_fin_val Std.BitVec.ofFin_val @@ -97,16 +82,12 @@ theorem decide_addLsb_mod_two {x b} : decide (addLsb x b % 2 = 1) = b := by simp [addLsb] #align bitvec.to_bool_add_lsb_mod_two Std.BitVec.decide_addLsb_mod_two -@[simp] -lemma ofNat_toNat (x : BitVec w) : BitVec.ofNat w x.toNat = x := by - rcases x with ⟨x⟩ - simp [BitVec.ofNat] - apply Fin.cast_val_eq_self x -#align bitvec.of_nat_to_nat Std.BitVec.ofNat_toNat +@[simp] lemma ofNat_toNat' (x : BitVec w) : (x.toNat)#w = x := by + rw [ofNat_toNat, truncate_eq] -lemma ofNat_toNat' (x : BitVec w) (h : w = v): +lemma ofNat_toNat_of_eq (x : BitVec w) (h : w = v): BitVec.ofNat v x.toNat = x.cast h := by - cases h; rw [ofNat_toNat, cast_eq] + cases h; rw [ofNat_toNat', cast_eq] theorem toFin_val {n : ℕ} (v : BitVec n) : (toFin v : ℕ) = v.toNat := by rfl diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean index 451b1f54700102..50bddc60ebbe1f 100644 --- a/Mathlib/Data/Bool/Basic.lean +++ b/Mathlib/Data/Bool/Basic.lean @@ -47,14 +47,7 @@ theorem of_decide_iff {p : Prop} [Decidable p] : decide p ↔ p := coe_decide p #align bool.of_to_bool_iff Bool.of_decide_iff -@[simp] -theorem true_eq_decide_iff {p : Prop} [Decidable p] : true = decide p ↔ p := - eq_comm.trans of_decide_iff #align bool.tt_eq_to_bool_iff Bool.true_eq_decide_iff - -@[simp] -theorem false_eq_decide_iff {p : Prop} [Decidable p] : false = decide p ↔ ¬p := - eq_comm.trans (decide_false_iff _) #align bool.ff_eq_to_bool_iff Bool.false_eq_decide_iff theorem decide_not (p : Prop) [Decidable p] : (decide ¬p) = !(decide p) := by @@ -308,22 +301,13 @@ theorem right_le_or : ∀ x y : Bool, y ≤ (x || y) := by decide theorem or_le : ∀ {x y z}, x ≤ z → y ≤ z → (x || y) ≤ z := by decide #align bool.bor_le Bool.or_le -/-- convert a `Bool` to a `ℕ`, `false -> 0`, `true -> 1` -/ -def toNat (b : Bool) : Nat := - cond b 1 0 #align bool.to_nat Bool.toNat -lemma toNat_le_one (b : Bool) : b.toNat ≤ 1 := by - cases b <;> decide - /-- convert a `ℕ` to a `Bool`, `0 -> false`, everything else -> `true` -/ def ofNat (n : Nat) : Bool := decide (n ≠ 0) #align bool.of_nat Bool.ofNat -@[simp] lemma toNat_true : toNat true = 1 := rfl -@[simp] lemma toNat_false : toNat false = 0 := rfl - @[simp] lemma toNat_beq_zero (b : Bool) : (b.toNat == 0) = !b := by cases b <;> rfl @[simp] lemma toNat_bne_zero (b : Bool) : (b.toNat != 0) = b := by simp [bne] @[simp] lemma toNat_beq_one (b : Bool) : (b.toNat == 1) = b := by cases b <;> rfl diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index f776c5598e1087..0808371b3a9319 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -407,15 +407,15 @@ attribute [local simp] Int.zero_div theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<< (n : ℤ)) <<< k | (m : ℕ), n, (k : ℕ) => - congr_arg ofNat (by simp [Nat.pow_add, mul_assoc]) + congr_arg ofNat (by simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc]) | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftLeft'_add _ _ _ _) | (m : ℕ), n, -[k+1] => subNatNat_elim n k.succ (fun n k i => (↑m) <<< i = (Nat.shiftLeft' false m n) >>> k) (fun (i n : ℕ) => - by dsimp; simp [- Nat.shiftLeft_eq, ← Nat.shiftLeft_sub _ , add_tsub_cancel_left]) + by dsimp; simp [← Nat.shiftLeft_sub _ , add_tsub_cancel_left]) fun i n => by dsimp - simp [- Nat.shiftLeft_eq, Nat.shiftLeft_zero, Nat.shiftRight_add, ← Nat.shiftLeft_sub] + simp [Nat.shiftLeft_zero, Nat.shiftRight_add, ← Nat.shiftLeft_sub] rfl | -[m+1], n, -[k+1] => subNatNat_elim n k.succ @@ -433,7 +433,7 @@ theorem shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (n - k) = (m <<< (n #align int.shiftl_sub Int.shiftLeft_sub theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2 ^ n : ℕ) - | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp) + | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq]) | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _) #align int.shiftl_eq_mul_pow Int.shiftLeft_eq_mul_pow @@ -445,7 +445,7 @@ theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / ( #align int.shiftr_eq_div_pow Int.shiftRight_eq_div_pow theorem one_shiftLeft (n : ℕ) : 1 <<< (n : ℤ) = (2 ^ n : ℕ) := - congr_arg ((↑) : ℕ → ℤ) (by simp) + congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq]) #align int.one_shiftl Int.one_shiftLeft @[simp] diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 5f999e12a50f9a..24a63bd7e349fd 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -838,11 +838,12 @@ theorem lt_mul_div_succ (m : ℕ) {n : ℕ} (n0 : 0 < n) : m < n * (m / n + 1) : exact lt_succ_self _ #align nat.lt_mul_div_succ Nat.lt_mul_div_succ -theorem mul_add_mod (a b c : ℕ) : (a * b + c) % b = c % b := by simp [Nat.add_mod] -#align nat.mul_add_mod Nat.mul_add_mod +-- TODO: Std4 claimed this name but flipped the order of multiplication +theorem mul_add_mod' (a b c : ℕ) : (a * b + c) % b = c % b := by rw [mul_comm, Nat.mul_add_mod] +#align nat.mul_add_mod Nat.mul_add_mod' theorem mul_add_mod_of_lt {a b c : ℕ} (h : c < b) : (a * b + c) % b = c := by - rw [Nat.mul_add_mod, Nat.mod_eq_of_lt h] + rw [Nat.mul_add_mod', Nat.mod_eq_of_lt h] #align nat.mul_add_mod_of_lt Nat.mul_add_mod_of_lt theorem pred_eq_self_iff {n : ℕ} : n.pred = n ↔ n = 0 := by diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index 7e63942b5660b1..cfa0f629fc037b 100644 --- a/Mathlib/Data/Nat/Bitwise.lean +++ b/Mathlib/Data/Nat/Bitwise.lean @@ -126,15 +126,7 @@ theorem xor_bit : ∀ a m b n, bit a m ^^^ bit b n = bit (bne a b) (m ^^^ n) := bitwise_bit #align nat.lxor_bit Nat.xor_bit -@[simp] -theorem testBit_bitwise {f : Bool → Bool → Bool} (h : f false false = false) (m n k) : - testBit (bitwise f m n) k = f (testBit m k) (testBit n k) := by - induction' k with k ih generalizing m n - <;> cases' m using bitCasesOn with a m - <;> cases' n using bitCasesOn with b n - <;> rw [bitwise_bit h] - · simp [testBit_zero] - · simp [testBit_succ, ih] +attribute [simp] Nat.testBit_bitwise #align nat.test_bit_bitwise Nat.testBit_bitwise @[simp] @@ -152,9 +144,7 @@ theorem testBit_ldiff : ∀ m n k, testBit (ldiff m n) k = (testBit m k && not ( testBit_bitwise rfl #align nat.test_bit_ldiff Nat.testBit_ldiff -@[simp] -theorem testBit_xor : ∀ m n k, testBit (m ^^^ n) k = bne (testBit m k) (testBit n k) := - testBit_bitwise rfl +attribute [simp] testBit_xor #align nat.test_bit_lxor Nat.testBit_xor end @@ -217,31 +207,19 @@ theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n theorem testBit_eq_false_of_lt {n i} (h : n < 2 ^ i) : n.testBit i = false := by simp [testBit, shiftRight_eq_div_pow, Nat.div_eq_of_lt h] -@[simp] -theorem zero_testBit (i : ℕ) : testBit 0 i = false := by - simp only [testBit, zero_shiftRight, bodd_zero] #align nat.zero_test_bit Nat.zero_testBit /-- The ith bit is the ith element of `n.bits`. -/ theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i := by induction' i with i ih generalizing n - · simp [testBit, bodd_eq_bits_head, List.getI_zero_eq_headI] + · simp only [testBit, zero_eq, shiftRight_zero, and_one_is_mod, mod_two_of_bodd, + bodd_eq_bits_head, List.getI_zero_eq_headI] + cases List.headI (bits n) <;> rfl conv_lhs => rw [← bit_decomp n] rw [testBit_succ, ih n.div2, div2_bits_eq_tail] cases n.bits <;> simp #align nat.test_bit_eq_inth Nat.testBit_eq_inth -/-- Bitwise extensionality: Two numbers agree if they agree at every bit position. -/ -theorem eq_of_testBit_eq {n m : ℕ} (h : ∀ i, testBit n i = testBit m i) : n = m := by - induction' n using Nat.binaryRec with b n hn generalizing m - · simp only [zero_testBit] at h - exact (zero_of_testBit_eq_false fun i => (h i).symm).symm - induction' m using Nat.binaryRec with b' m - · simp only [zero_testBit] at h - exact zero_of_testBit_eq_false h - suffices h' : n = m by - rw [h', show b = b' by simpa using h 0] - exact hn fun i => by convert h (i + 1) using 1 <;> rw [testBit_succ] #align nat.eq_of_test_bit_eq Nat.eq_of_testBit_eq theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) : @@ -295,20 +273,20 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes @[simp] theorem testBit_two_pow_self (n : ℕ) : testBit (2 ^ n) n = true := by - rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n), bodd_one] + rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n)] + simp #align nat.test_bit_two_pow_self Nat.testBit_two_pow_self theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = false := by rw [testBit, shiftRight_eq_div_pow] cases' hm.lt_or_lt with hm hm - · rw [Nat.div_eq_of_lt, bodd_zero] - exact Nat.pow_lt_pow_of_lt_right one_lt_two hm + · rw [Nat.div_eq_of_lt] + · simp + · exact Nat.pow_lt_pow_of_lt_right one_lt_two hm · rw [pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)] -- Porting note: XXX why does this make it work? rw [(rfl : succ 0 = 1)] - simp only [ge_iff_le, tsub_le_iff_right, pow_succ, bodd_mul, - Bool.and_eq_false_eq_eq_false_or_eq_false, or_true] - exact Or.inr rfl + simp [pow_succ, and_one_is_mod, mul_mod_left] #align nat.test_bit_two_pow_of_ne Nat.testBit_two_pow_of_ne theorem testBit_two_pow (n m : ℕ) : testBit (2 ^ n) m = (n = m) := by @@ -372,25 +350,10 @@ theorem zero_xor (n : ℕ) : 0 ^^^ n = n := by simp [HXor.hXor, Xor.xor, xor] theorem xor_zero (n : ℕ) : n ^^^ 0 = n := by simp [HXor.hXor, Xor.xor, xor] #align nat.lxor_zero Nat.xor_zero -@[simp] -theorem zero_land (n : ℕ) : 0 &&& n = 0 := by - simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_left, ite_false, Bool.and_true]; -#align nat.zero_land Nat.zero_land - -@[simp] -theorem land_zero (n : ℕ) : n &&& 0 = 0 := by - simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_right, ite_false, Bool.and_false] -#align nat.land_zero Nat.land_zero - -@[simp] -theorem zero_lor (n : ℕ) : 0 ||| n = n := by - simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_left, ite_true, Bool.or_true] -#align nat.zero_lor Nat.zero_lor - -@[simp] -theorem lor_zero (n : ℕ) : n ||| 0 = n := by - simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_right, ite_true, Bool.or_false] -#align nat.lor_zero Nat.lor_zero +#align nat.zero_land Nat.zero_and +#align nat.land_zero Nat.and_zero +#align nat.zero_lor Nat.zero_or +#align nat.lor_zero Nat.or_zero /-- Proving associativity of bitwise operations in general essentially boils down to a huge case @@ -488,11 +451,11 @@ theorem xor_trichotomy {a b c : ℕ} (h : a ≠ b ^^^ c) : all_goals exact lt_of_testBit i (by -- Porting note: this was originally `simp [h, hi]` - rw [Nat.testBit_xor, h, Bool.bne_eq_xor, Bool.true_xor,hi] + rw [Nat.testBit_xor, h, Bool.xor, Bool.true_xor, hi] rfl ) h fun j hj => by -- Porting note: this was originally `simp [hi' _ hj]` - rw [Nat.testBit_xor, hi' _ hj, Bool.bne_eq_xor, Bool.xor_false, eq_self_iff_true] + rw [Nat.testBit_xor, hi' _ hj, Bool.xor, Bool.xor_false, eq_self_iff_true] trivial #align nat.lxor_trichotomy Nat.xor_trichotomy diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean index 347d22795547b8..53533ef5aaddf2 100644 --- a/Mathlib/Data/Nat/Order/Lemmas.lean +++ b/Mathlib/Data/Nat/Order/Lemmas.lean @@ -223,11 +223,6 @@ theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b := exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _ #align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd -@[simp] -theorem mod_div_self (m n : ℕ) : m % n / n = 0 := by - cases n - · exact (m % 0).div_zero - · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos) #align nat.mod_div_self Nat.mod_div_self /-- `n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`. -/ diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean index 3a9c95879822ea..0feaee57900ea0 100644 --- a/Mathlib/Data/Nat/Size.lean +++ b/Mathlib/Data/Nat/Size.lean @@ -32,10 +32,7 @@ theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1) end #align nat.one_shiftl Nat.one_shiftLeft - -theorem zero_shiftLeft (n) : 0 <<< n = 0 := by simp #align nat.zero_shiftl Nat.zero_shiftLeft - #align nat.shiftr_eq_div_pow Nat.shiftRight_eq_div_pow theorem shiftLeft'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftLeft' b m n ≠ 0 := by @@ -118,7 +115,7 @@ theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by by_cases h : bit b n = 0 · apply this h rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul, ← bit0_val] - exact bit_lt_bit0 _ (by simpa [shiftRight_eq_div_pow] using IH) + exact bit_lt_bit0 _ (by simpa [shiftLeft_eq, shiftRight_eq_div_pow] using IH) #align nat.lt_size_self Nat.lt_size_self theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n := diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean index dc9ced5fbb7cfa..a4a8b74d9a2d5e 100644 --- a/Mathlib/Data/Num/Lemmas.lean +++ b/Mathlib/Data/Num/Lemmas.lean @@ -970,28 +970,40 @@ theorem castNum_shiftRight (m : Num) (n : Nat) : ↑(m >>> n) = (m : ℕ) >>> (n @[simp] theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by -- Porting note: `unfold` → `dsimp only` - cases m <;> dsimp only [testBit, Nat.testBit] + cases m <;> dsimp only [testBit] case zero => - change false = Nat.bodd (0 >>> n) - rw [Nat.zero_shiftRight] - rfl + rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit] case pos m => - induction' n with n IH generalizing m <;> cases' m with m m <;> dsimp only [PosNum.testBit] + rw [cast_pos] + induction' n with n IH generalizing m <;> cases' m with m m + <;> dsimp only [PosNum.testBit, Nat.zero_eq] · rfl - · exact (Nat.bodd_bit _ _).symm - · exact (Nat.bodd_bit _ _).symm - · change false = Nat.bodd (1 >>> (n + 1)) +<<<<<<< HEAD + · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_zero] + · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_zero] + · rw [PosNum.cast_one', ← bit1_zero, ← Nat.bit_true, Nat.testBit_succ, Nat.zero_testBit] + · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_succ, IH] + · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_succ, IH] +======= + · simp only [cast_pos, PosNum.cast_bit1, Nat.zero_eq, Nat.shiftRight_zero, Nat.and_one_is_mod] + rw [← Nat.bit_true, Nat.bit_mod_two] + rfl + · simp only [cast_pos, PosNum.cast_bit0, Nat.zero_eq, Nat.shiftRight_zero, Nat.and_one_is_mod] + rw[←Nat.bit_false, Nat.bit_mod_two] + rfl + · change _ = (Nat.bit true 0 >>> (n + 1) &&& 1 != 0) rw [add_comm, Nat.shiftRight_add] - change false = Nat.bodd (0 >>> n) - rw [Nat.zero_shiftRight]; rfl - · change PosNum.testBit m n = Nat.bodd ((Nat.bit true m) >>> (n + 1)) + simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit, + Nat.zero_shiftRight, Nat.and_one_is_mod, Nat.zero_mod, bne_self_eq_false] + · change _ = (Nat.bit true m >>> (n + 1) &&& 1 != 0) rw [add_comm, Nat.shiftRight_add] simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit] apply IH - · change PosNum.testBit m n = Nat.bodd ((Nat.bit false m) >>> (n + 1)) + · change _ = (Nat.bit false m >>> (n + 1) &&& 1 != 0) rw [add_comm, Nat.shiftRight_add] simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit] apply IH +>>>>>>> 7b6f1a3eb (Apply suggestions from code review) #align num.test_bit_to_nat Num.castNum_testBit end Num diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean index 5d8d5c74da67e8..cf70f850eda3f7 100644 --- a/Mathlib/Init/Data/Nat/Bitwise.lean +++ b/Mathlib/Init/Data/Nat/Bitwise.lean @@ -190,7 +190,7 @@ theorem shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n | n + 1 => by have : 2 * (m * 2^n) = 2^(n+1)*m := by rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp - simp [shiftLeft', bit_val, shiftLeft'_false, this] + simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this] /-- Std4 takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/ @[simp] @@ -199,14 +199,6 @@ lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl @[simp] lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl -theorem shiftLeft_zero (m) : m <<< 0 = m := rfl - -theorem shiftLeft_succ (m n) : m <<< (n + 1) = 2 * (m <<< n) := by - simp only [shiftLeft_eq, Nat.pow_add, Nat.pow_one, ← Nat.mul_assoc, Nat.mul_comm] - -/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/ -def testBit (m n : ℕ) : Bool := - bodd (m >>> n) #align nat.test_bit Nat.testBit lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by @@ -301,15 +293,28 @@ theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk] @[simp] -theorem testBit_zero (b n) : testBit (bit b n) 0 = b := - bodd_bit _ _ +theorem testBit_zero (b n) : testBit (bit b n) 0 = b := by + rw [testBit, bit] + cases b + · simp [bit0, ← Nat.mul_two] + · simp only [cond_true, bit1, bit0, shiftRight_zero, and_one_is_mod, bne_iff_ne] + simp only [← Nat.mul_two] + rw [Nat.add_mod] + simp + #align nat.test_bit_zero Nat.testBit_zero +theorem bodd_eq_and_one_ne_zero : ∀ n, bodd n = (n &&& 1 != 0) + | 0 => rfl + | 1 => rfl + | n + 2 => by simpa using bodd_eq_and_one_ne_zero n + theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by - dsimp [shiftRight] + simp only [shiftRight_eq_div_pow] simp [← div2_val, div2_bit] rw [← shiftRight_add, Nat.add_comm] at this + simp only [bodd_eq_and_one_ne_zero] at this exact this #align nat.test_bit_succ Nat.testBit_succ diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 207cef615f72c3..8f2210786a9f4f 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -585,16 +585,6 @@ theorem nontrivial_dual_iff : instance instNontrivialDual [Nontrivial V] : Nontrivial (Dual K V) := (nontrivial_dual_iff K).mpr inferInstance -theorem exists_dual_map_eq_bot_of_lt_top {p : Submodule K V} (hp : p < ⊤) (hp' : Free K (V ⧸ p)) : - ∃ f : Dual K V, f ≠ 0 ∧ p.map f = ⊥ := by - obtain ⟨f, g, h⟩ : Nontrivial (Dual K <| V ⧸ p) := - (nontrivial_dual_iff K).mpr <| Submodule.Quotient.nontrivial_of_lt_top p hp - refine ⟨(f - g).comp p.mkQ, ?_, by simp [Submodule.map_comp]⟩ - replace h : f - g ≠ 0 := sub_ne_zero.mpr h - contrapose! h - refine Submodule.quot_hom_ext (f := f - g) (g := 0) fun v ↦ (?_ : (f - g).comp p.mkQ v = _) - simp [h] - end theorem dual_rank_eq [Module.Finite K V] : @@ -703,6 +693,27 @@ end IsReflexive end Module +namespace Submodule + +open Module + +variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} + +theorem exists_dual_map_eq_bot_of_nmem {x : M} (hx : x ∉ p) (hp' : Free R (M ⧸ p)) : + ∃ f : Dual R M, f x ≠ 0 ∧ p.map f = ⊥ := by + suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by + obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩ + rwa [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply, + ← forall_dual_apply_eq_zero_iff (K := R), not_forall] at hx + +theorem exists_dual_map_eq_bot_of_lt_top (hp : p < ⊤) (hp' : Free R (M ⧸ p)) : + ∃ f : Dual R M, f ≠ 0 ∧ p.map f = ⊥ := by + obtain ⟨x, hx⟩ : ∃ x : M, x ∉ p := by rw [lt_top_iff_ne_top] at hp; contrapose! hp; ext; simp [hp] + obtain ⟨f, hf, hf'⟩ := p.exists_dual_map_eq_bot_of_nmem hx hp' + exact ⟨f, by aesop, hf'⟩ + +end Submodule + section DualBases open Module diff --git a/Mathlib/Topology/Category/Profinite/AsLimit.lean b/Mathlib/Topology/Category/Profinite/AsLimit.lean index 82df2d7476d439..c806893d68d393 100644 --- a/Mathlib/Topology/Category/Profinite/AsLimit.lean +++ b/Mathlib/Topology/Category/Profinite/AsLimit.lean @@ -64,12 +64,12 @@ def asLimitCone : CategoryTheory.Limits.Cone X.diagram := set_option linter.uppercaseLean3 false in #align Profinite.as_limit_cone Profinite.asLimitCone -instance isIso_asLimitCone_lift : IsIso ((limitConeIsLimit X.diagram).lift X.asLimitCone) := +instance isIso_asLimitCone_lift : IsIso ((limitConeIsLimit.{u, u} X.diagram).lift X.asLimitCone) := isIso_of_bijective _ (by refine' ⟨fun a b h => _, fun a => _⟩ · refine' DiscreteQuotient.eq_of_forall_proj_eq fun S => _ - apply_fun fun f : (limitCone X.diagram).pt => f.val S at h + apply_fun fun f : (limitCone.{u, u} X.diagram).pt => f.val S at h exact h · obtain ⟨b, hb⟩ := DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h) @@ -87,15 +87,15 @@ set_option linter.uppercaseLean3 false in /-- The isomorphism between `X` and the explicit limit of `X.diagram`, induced by lifting `X.asLimitCone`. -/ -def isoAsLimitConeLift : X ≅ (limitCone X.diagram).pt := - asIso <| (limitConeIsLimit _).lift X.asLimitCone +def isoAsLimitConeLift : X ≅ (limitCone.{u, u} X.diagram).pt := + asIso <| (limitConeIsLimit.{u, u} _).lift X.asLimitCone set_option linter.uppercaseLean3 false in #align Profinite.iso_as_limit_cone_lift Profinite.isoAsLimitConeLift /-- The isomorphism of cones `X.asLimitCone` and `Profinite.limitCone X.diagram`. The underlying isomorphism is defeq to `X.isoAsLimitConeLift`. -/ -def asLimitConeIso : X.asLimitCone ≅ limitCone _ := +def asLimitConeIso : X.asLimitCone ≅ limitCone.{u, u} _ := Limits.Cones.ext (isoAsLimitConeLift _) fun _ => rfl set_option linter.uppercaseLean3 false in #align Profinite.as_limit_cone_iso Profinite.asLimitConeIso diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index c45526e5e2799c..bf4a73b35c3b06 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/Mathlib/Topology/Category/Profinite/Basic.lean @@ -27,9 +27,7 @@ compact, Hausdorff and totally disconnected. ## TODO -0. Link to category of projective limits of finite discrete sets. -1. finite coproducts -2. Clausen/Scholze topology on the category `Profinite`. +* Define procategories and prove that `Profinite` is equivalent to `Pro (FintypeCat)`. ## Tags @@ -39,7 +37,7 @@ profinite set_option linter.uppercaseLean3 false -universe u +universe v u open CategoryTheory @@ -242,20 +240,31 @@ end DiscreteTopology end Profinite +/-- +Many definitions involving universe inequalities in Mathlib are expressed through use of `max u v`. +Unfortunately, this leads to unbound universes which cannot be solved for during unification, eg +`max u v =?= max v ?`. +The current solution is to wrap `Type max u v` in `TypeMax.{u,v}` +to expose both universe parameters directly. + +Similarly, for other concrete categories for which we need to refer to the maximum of two universes +(e.g. any category for which we are constructing limits), we need an analogous abbreviation. +-/ +@[nolint checkUnivs] +abbrev ProfiniteMax.{w, w'} := Profinite.{max w w'} + namespace Profinite --- TODO the following construction of limits could be generalised --- to allow diagrams in lower universes. /-- An explicit limit cone for a functor `F : J ⥤ Profinite`, defined in terms of `CompHaus.limitCone`, which is defined in terms of `TopCat.limitCone`. -/ -def limitCone {J : Type u} [SmallCategory J] (F : J ⥤ Profinite.{u}) : Limits.Cone F where +def limitCone {J : Type v} [SmallCategory J] (F : J ⥤ ProfiniteMax.{v, u}) : Limits.Cone F where pt := - { toCompHaus := (CompHaus.limitCone.{u, u} (F ⋙ profiniteToCompHaus)).pt + { toCompHaus := (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt isTotallyDisconnected := by change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _) exact Subtype.totallyDisconnectedSpace } π := - { app := (CompHaus.limitCone.{u, u} (F ⋙ profiniteToCompHaus)).π.app + { app := (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app -- Porting note: was `by tidy`: naturality := by intro j k f @@ -264,12 +273,12 @@ def limitCone {J : Type u} [SmallCategory J] (F : J ⥤ Profinite.{u}) : Limits. #align Profinite.limit_cone Profinite.limitCone /-- The limit cone `Profinite.limitCone F` is indeed a limit cone. -/ -def limitConeIsLimit {J : Type u} [SmallCategory J] (F : J ⥤ Profinite.{u}) : +def limitConeIsLimit {J : Type v} [SmallCategory J] (F : J ⥤ ProfiniteMax.{v, u}) : Limits.IsLimit (limitCone F) where lift S := - (CompHaus.limitConeIsLimit.{u, u} (F ⋙ profiniteToCompHaus)).lift + (CompHaus.limitConeIsLimit.{v, u} (F ⋙ profiniteToCompHaus)).lift (profiniteToCompHaus.mapCone S) - uniq S m h := (CompHaus.limitConeIsLimit.{u, u} _).uniq (profiniteToCompHaus.mapCone S) _ h + uniq S m h := (CompHaus.limitConeIsLimit.{v, u} _).uniq (profiniteToCompHaus.mapCone S) _ h #align Profinite.limit_cone_is_limit Profinite.limitConeIsLimit /-- The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus -/ diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean index 63035ff10b9bd1..495e15fcf3a485 100644 --- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean +++ b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean @@ -24,7 +24,6 @@ This file contains some theorems about cofiltered limits of profinite sets. of profinite sets factors through one of the components. -/ - namespace Profinite open scoped Classical @@ -33,9 +32,14 @@ open CategoryTheory open CategoryTheory.Limits -universe u +universe u v + +variable {J : Type v} [SmallCategory J] [IsCofiltered J] {F : J ⥤ ProfiniteMax.{u, v}} (C : Cone F) -variable {J : Type u} [SmallCategory J] [IsCofiltered J] {F : J ⥤ Profinite.{u}} (C : Cone F) +noncomputable +instance preserves_smaller_limits_toTopCat : + PreservesLimitsOfSize.{v, v} (toTopCat : ProfiniteMax.{v, u} ⥤ TopCatMax.{v, u}) := + Limits.preservesLimitsOfSizeShrink.{v, max u v, v, max u v} _ -- include hC -- Porting note: I just add `(hC : IsLimit C)` explicitly as a hypothesis to all the theorems @@ -45,9 +49,10 @@ a clopen set in one of the terms in the limit. -/ theorem exists_clopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) : ∃ (j : J) (V : Set (F.obj j)) (_ : IsClopen V), U = C.π.app j ⁻¹' V := by + have := preserves_smaller_limits_toTopCat.{u, v} -- First, we have the topological basis of the cofiltered limit obtained by pulling back -- clopen sets from the factors in the limit. By continuity, all such sets are again clopen. - have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, u} (F ⋙ Profinite.toTopCat) + have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, v} (F ⋙ Profinite.toTopCat) (Profinite.toTopCat.mapCone C) (isLimitOfPreserves _ hC) (fun j => {W | IsClopen W}) ?_ (fun i => isClopen_univ) (fun i U1 U2 hU1 hU2 => hU1.inter hU2) ?_ rotate_left @@ -214,6 +219,7 @@ set_option linter.uppercaseLean3 false in one of the components. -/ theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstant C.pt α) : ∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _) := by + have := preserves_smaller_limits_toTopCat.{u, v} let S := f.discreteQuotient let ff : S → α := f.lift cases isEmpty_or_nonempty S @@ -238,7 +244,7 @@ theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstan suffices : Nonempty C.pt; exact IsEmpty.false (S.proj this.some) let D := Profinite.toTopCat.mapCone C have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC - have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{u, u} _)).inv + have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv exact cond.map CD · let f' : LocallyConstant C.pt S := ⟨S.proj, S.proj_isLocallyConstant⟩ obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f' diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index acc37c3ac01779..a075acbf3e40c4 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -677,8 +677,8 @@ theorem fin_comap_jointlySurjective (hC : IsClosed C) (f : LocallyConstant C ℤ) : ∃ (s : Finset I) (g : LocallyConstant (π C (· ∈ s)) ℤ), f = g.comap (ProjRestrict C (· ∈ s)) := by - obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _ - (spanCone hC.isCompact) _ + obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant.{0, u, u} (Finset I)ᵒᵖ _ _ _ + (spanCone hC.isCompact) ℤ (spanCone_isLimit hC.isCompact) f exact ⟨(Opposite.unop J), g, h⟩ diff --git a/Mathlib/Topology/Category/Profinite/Product.lean b/Mathlib/Topology/Category/Profinite/Product.lean index 41cefdc8d8b5ea..f3a74831a94265 100644 --- a/Mathlib/Topology/Category/Profinite/Product.lean +++ b/Mathlib/Topology/Category/Profinite/Product.lean @@ -94,13 +94,13 @@ def indexCone : Cone (indexFunctor hC) where π := { app := fun J ↦ π_app C (· ∈ unop J) } instance isIso_indexCone_lift : - IsIso ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC)) := + IsIso ((limitConeIsLimit.{u, u} (indexFunctor hC)).lift (indexCone hC)) := haveI : CompactSpace C := by rwa [← isCompact_iff_compactSpace] isIso_of_bijective _ (by refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩ · refine eq_of_forall_π_app_eq a b (fun J ↦ ?_) - apply_fun fun f : (limitCone (indexFunctor hC)).pt => f.val (op J) at h + apply_fun fun f : (limitCone.{u, u} (indexFunctor hC)).pt => f.val (op J) at h exact h · suffices : ∃ (x : C), ∀ (J : Finset ι), π_app C (· ∈ J) x = a.val (op J) · obtain ⟨b, hb⟩ := this @@ -133,12 +133,12 @@ instance isIso_indexCone_lift : noncomputable def isoindexConeLift : @Profinite.of C _ (by rwa [← isCompact_iff_compactSpace]) _ _ ≅ - (Profinite.limitCone (indexFunctor hC)).pt := - asIso <| (Profinite.limitConeIsLimit _).lift (indexCone hC) + (Profinite.limitCone.{u, u} (indexFunctor hC)).pt := + asIso <| (Profinite.limitConeIsLimit.{u, u} _).lift (indexCone hC) /-- The isomorphism of cones induced by `isoindexConeLift`. -/ noncomputable -def asLimitindexConeIso : indexCone hC ≅ Profinite.limitCone _ := +def asLimitindexConeIso : indexCone hC ≅ Profinite.limitCone.{u, u} _ := Limits.Cones.ext (isoindexConeLift hC) fun _ => rfl /-- `indexCone` is a limit cone. -/ diff --git a/lake-manifest.json b/lake-manifest.json index 5e630d988708b4..c69509bb46bbd6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,11 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, +<<<<<<< HEAD + "rev": "a93d4aab761b7962a6aab845b24837e192eaabc5", +======= "rev": "415a6731db08f4d98935e5d80586d5a5499e02af", +>>>>>>> c43641ccb (chore: bump Std) "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main",