From 1b089e3bdc3ce6b39cd472543474a0a137128c6c Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Thu, 22 Jun 2023 05:03:22 +0000 Subject: [PATCH 01/16] chore(*): add mathlib4 synchronization comments (#19211) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Group.adjunctions` * `analysis.constant_speed` * `analysis.convolution` * `category_theory.category.PartialFun` * `control.bitraversable.instances` * `control.uliftable` * `data.nat.nth` * `field_theory.cardinality` * `field_theory.finite.galois_field` * `field_theory.finite.trace` * `number_theory.function_field` * `number_theory.number_field.basic` * `number_theory.number_field.norm` * `number_theory.prime_counting` * `number_theory.zeta_values` * `probability.ident_distrib` * `probability.kernel.cond_distrib` * `probability.kernel.condexp` * `probability.moments` * `probability.strong_law` * `probability.variance` * `representation_theory.Rep` * `ring_theory.complex` * `ring_theory.valuation.ramification_group` * `ring_theory.valuation.valuation_subring` * `set_theory.ordinal.notation` --- src/algebra/category/Group/adjunctions.lean | 3 +++ src/analysis/constant_speed.lean | 3 +++ src/analysis/convolution.lean | 3 +++ src/category_theory/category/PartialFun.lean | 3 +++ src/control/bitraversable/instances.lean | 3 +++ src/control/uliftable.lean | 3 +++ src/data/nat/nth.lean | 3 +++ src/field_theory/cardinality.lean | 3 +++ src/field_theory/finite/galois_field.lean | 3 +++ src/field_theory/finite/trace.lean | 3 +++ src/number_theory/function_field.lean | 3 +++ src/number_theory/number_field/basic.lean | 3 +++ src/number_theory/number_field/norm.lean | 3 +++ src/number_theory/prime_counting.lean | 3 +++ src/number_theory/zeta_values.lean | 3 +++ src/probability/ident_distrib.lean | 3 +++ src/probability/kernel/cond_distrib.lean | 3 +++ src/probability/kernel/condexp.lean | 3 +++ src/probability/moments.lean | 3 +++ src/probability/strong_law.lean | 3 +++ src/probability/variance.lean | 3 +++ src/representation_theory/Rep.lean | 3 +++ src/ring_theory/complex.lean | 5 ++++- src/ring_theory/valuation/ramification_group.lean | 3 +++ src/ring_theory/valuation/valuation_subring.lean | 3 +++ src/set_theory/ordinal/notation.lean | 3 +++ 26 files changed, 79 insertions(+), 1 deletion(-) diff --git a/src/algebra/category/Group/adjunctions.lean b/src/algebra/category/Group/adjunctions.lean index 64f2caf41d79c..8aa601a197357 100644 --- a/src/algebra/category/Group/adjunctions.lean +++ b/src/algebra/category/Group/adjunctions.lean @@ -9,6 +9,9 @@ import group_theory.free_abelian_group /-! # Adjunctions regarding the category of (abelian) groups +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains construction of basic adjunctions concerning the category of groups and the category of abelian groups. diff --git a/src/analysis/constant_speed.lean b/src/analysis/constant_speed.lean index c6ac9e016baf7..aa5b84190414f 100644 --- a/src/analysis/constant_speed.lean +++ b/src/analysis/constant_speed.lean @@ -9,6 +9,9 @@ import tactic.swap_var /-! # Constant speed +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the notion of constant (and unit) speed for a function `f : ℝ → E` with pseudo-emetric structure on `E` with respect to a set `s : set ℝ` and "speed" `l : ℝ≥0`, and shows that if `f` has locally bounded variation on `s`, it can be obtained (up to distance zero, on `s`), diff --git a/src/analysis/convolution.lean b/src/analysis/convolution.lean index edcbfe3a605bb..74b30a8db71c0 100644 --- a/src/analysis/convolution.lean +++ b/src/analysis/convolution.lean @@ -14,6 +14,9 @@ import measure_theory.integral.interval_integral /-! # Convolution of functions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the convolution on two functions, i.e. `x ↦ ∫ f(t)g(x - t) ∂t`. In the general case, these functions can be vector-valued, and have an arbitrary (additive) group as domain. We use a continuous bilinear operation `L` on these function values as diff --git a/src/category_theory/category/PartialFun.lean b/src/category_theory/category/PartialFun.lean index bef9af2a87470..46ffcb1b33c11 100644 --- a/src/category_theory/category/PartialFun.lean +++ b/src/category_theory/category/PartialFun.lean @@ -9,6 +9,9 @@ import data.pfun /-! # The category of types with partial functions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This defines `PartialFun`, the category of types equipped with partial functions. This category is classically equivalent to the category of pointed types. The reason it doesn't hold diff --git a/src/control/bitraversable/instances.lean b/src/control/bitraversable/instances.lean index 851bc71c60b8a..1b6bb4da9175d 100644 --- a/src/control/bitraversable/instances.lean +++ b/src/control/bitraversable/instances.lean @@ -9,6 +9,9 @@ import control.traversable.lemmas /-! # Bitraversable instances +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file provides `bitraversable` instances for concrete bifunctors: * `prod` * `sum` diff --git a/src/control/uliftable.lean b/src/control/uliftable.lean index 3cdadee22171d..104ed8c3b5399 100644 --- a/src/control/uliftable.lean +++ b/src/control/uliftable.lean @@ -12,6 +12,9 @@ import tactic.interactive /-! # Universe lifting for type families +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Some functors such as `option` and `list` are universe polymorphic. Unlike type polymorphism where `option α` is a function application and reasoning and generalizations that apply to functions can be used, `option.{u}` and `option.{v}` diff --git a/src/data/nat/nth.lean b/src/data/nat/nth.lean index c7802520e6ce0..42541ced019d3 100644 --- a/src/data/nat/nth.lean +++ b/src/data/nat/nth.lean @@ -10,6 +10,9 @@ import order.order_iso_nat /-! # The `n`th Number Satisfying a Predicate +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines a function for "what is the `n`th number that satisifies a given predicate `p`", and provides lemmas that deal with this function and its connection to `nat.count`. diff --git a/src/field_theory/cardinality.lean b/src/field_theory/cardinality.lean index 17a1c271f3e9b..e01d6b48ab64b 100644 --- a/src/field_theory/cardinality.lean +++ b/src/field_theory/cardinality.lean @@ -15,6 +15,9 @@ import set_theory.cardinal.divisibility /-! # Cardinality of Fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we show all the possible cardinalities of fields. All infinite cardinals can harbour a field structure, and so can all types with prime power cardinalities, and this is sharp. diff --git a/src/field_theory/finite/galois_field.lean b/src/field_theory/finite/galois_field.lean index 8737cefa46b92..d787c29c4b3c7 100644 --- a/src/field_theory/finite/galois_field.lean +++ b/src/field_theory/finite/galois_field.lean @@ -13,6 +13,9 @@ import field_theory.splitting_field.is_splitting_field /-! # Galois fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + If `p` is a prime number, and `n` a natural number, then `galois_field p n` is defined as the splitting field of `X^(p^n) - X` over `zmod p`. It is a finite field with `p ^ n` elements. diff --git a/src/field_theory/finite/trace.lean b/src/field_theory/finite/trace.lean index 42c334451a5f2..59dd268d8dc49 100644 --- a/src/field_theory/finite/trace.lean +++ b/src/field_theory/finite/trace.lean @@ -9,6 +9,9 @@ import field_theory.finite.galois_field /-! # The trace map for finite fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We state the fact that the trace map from a finite field of characteristic `p` to `zmod p` is nondegenerate. diff --git a/src/number_theory/function_field.lean b/src/number_theory/function_field.lean index 74b7f229c433a..491ce0bc15592 100644 --- a/src/number_theory/function_field.lean +++ b/src/number_theory/function_field.lean @@ -12,6 +12,9 @@ import topology.algebra.valued_field /-! # Function fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines a function field and the ring of integers corresponding to it. ## Main definitions diff --git a/src/number_theory/number_field/basic.lean b/src/number_theory/number_field/basic.lean index 537628af9ebf9..a426ce89fb1e7 100644 --- a/src/number_theory/number_field/basic.lean +++ b/src/number_theory/number_field/basic.lean @@ -8,6 +8,9 @@ import ring_theory.dedekind_domain.integral_closure /-! # Number fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. This file defines a number field and the ring of integers corresponding to it. ## Main definitions diff --git a/src/number_theory/number_field/norm.lean b/src/number_theory/number_field/norm.lean index 8476cfc5dff86..1699edeb6c4c3 100644 --- a/src/number_theory/number_field/norm.lean +++ b/src/number_theory/number_field/norm.lean @@ -9,6 +9,9 @@ import ring_theory.norm /-! # Norm in number fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. Given a finite extension of number fields, we define the norm morphism as a function between the rings of integers. diff --git a/src/number_theory/prime_counting.lean b/src/number_theory/prime_counting.lean index d811b98cd28f0..6a699a1ae127d 100644 --- a/src/number_theory/prime_counting.lean +++ b/src/number_theory/prime_counting.lean @@ -13,6 +13,9 @@ import data.nat.nth /-! # The Prime Counting Function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define the prime counting function: the function on natural numbers that returns the number of primes less than or equal to its input. diff --git a/src/number_theory/zeta_values.lean b/src/number_theory/zeta_values.lean index bb90b628f09d4..296f70123d559 100644 --- a/src/number_theory/zeta_values.lean +++ b/src/number_theory/zeta_values.lean @@ -12,6 +12,9 @@ import analysis.p_series /-! # Critical values of the Riemann zeta function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we prove formulae for the critical values of `ζ(s)`, and more generally of Hurwitz zeta functions, in terms of Bernoulli polynomials. diff --git a/src/probability/ident_distrib.lean b/src/probability/ident_distrib.lean index 75775ebd5c98a..022eafdb4b26b 100644 --- a/src/probability/ident_distrib.lean +++ b/src/probability/ident_distrib.lean @@ -9,6 +9,9 @@ import measure_theory.function.uniform_integrable /-! # Identically distributed random variables +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Two random variables defined on two (possibly different) probability spaces but taking value in the same space are *identically distributed* if their distributions (i.e., the image probability measures on the target space) coincide. We define this concept and establish its basic properties diff --git a/src/probability/kernel/cond_distrib.lean b/src/probability/kernel/cond_distrib.lean index 6da8554ccaf4b..d1a141b01b8e4 100644 --- a/src/probability/kernel/cond_distrib.lean +++ b/src/probability/kernel/cond_distrib.lean @@ -9,6 +9,9 @@ import probability.notation /-! # Regular conditional probability distribution +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the regular conditional probability distribution of `Y : α → Ω` given `X : α → β`, where `Ω` is a standard Borel space. This is a `kernel β Ω` such that for almost all `a`, `cond_distrib` evaluated at `X a` and a measurable set `s` is equal to the conditional expectation diff --git a/src/probability/kernel/condexp.lean b/src/probability/kernel/condexp.lean index d860a20e4c3ac..d63c7bb03b265 100644 --- a/src/probability/kernel/condexp.lean +++ b/src/probability/kernel/condexp.lean @@ -8,6 +8,9 @@ import probability.kernel.cond_distrib /-! # Kernel associated with a conditional expectation +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define `condexp_kernel μ m`, a kernel from `Ω` to `Ω` such that for all integrable functions `f`, `μ[f | m] =ᵐ[μ] λ ω, ∫ y, f y ∂(condexp_kernel μ m ω)`. diff --git a/src/probability/moments.lean b/src/probability/moments.lean index 392a55356ec10..64126645bbb0a 100644 --- a/src/probability/moments.lean +++ b/src/probability/moments.lean @@ -9,6 +9,9 @@ import probability.variance /-! # Moments and moment generating function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions * `probability_theory.moment X p μ`: `p`th moment of a real random variable `X` with respect to diff --git a/src/probability/strong_law.lean b/src/probability/strong_law.lean index e09fa4393ca78..53020a09142fa 100644 --- a/src/probability/strong_law.lean +++ b/src/probability/strong_law.lean @@ -13,6 +13,9 @@ import analysis.asymptotics.specific_asymptotics /-! # The strong law of large numbers +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We prove the strong law of large numbers, in `probability_theory.strong_law_ae`: If `X n` is a sequence of independent identically distributed integrable real-valued random variables, then `∑ i in range n, X i / n` converges almost surely to `𝔼[X 0]`. diff --git a/src/probability/variance.lean b/src/probability/variance.lean index a0b0c08c87d91..bf41ae83ad847 100644 --- a/src/probability/variance.lean +++ b/src/probability/variance.lean @@ -10,6 +10,9 @@ import measure_theory.function.l2_space /-! # Variance of random variables +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the variance of a real-valued random variable as `Var[X] = 𝔼[(X - 𝔼[X])^2]` (in the `probability_theory` locale). diff --git a/src/representation_theory/Rep.lean b/src/representation_theory/Rep.lean index 2f801e5652d25..cd4ef0178d7bd 100644 --- a/src/representation_theory/Rep.lean +++ b/src/representation_theory/Rep.lean @@ -14,6 +14,9 @@ import category_theory.closed.functor_category /-! # `Rep k G` is the category of `k`-linear representations of `G`. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + If `V : Rep k G`, there is a coercion that allows you to treat `V` as a type, and this type comes equipped with a `module k V` instance. Also `V.ρ` gives the homomorphism `G →* (V →ₗ[k] V)`. diff --git a/src/ring_theory/complex.lean b/src/ring_theory/complex.lean index 598d189f045c2..88b939cc3fb71 100644 --- a/src/ring_theory/complex.lean +++ b/src/ring_theory/complex.lean @@ -7,7 +7,10 @@ import data.complex.module import ring_theory.norm import ring_theory.trace -/-! # Lemmas about `algebra.trace` and `algebra.norm` on `ℂ` -/ +/-! # Lemmas about `algebra.trace` and `algebra.norm` on `ℂ` + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4.-/ open complex diff --git a/src/ring_theory/valuation/ramification_group.lean b/src/ring_theory/valuation/ramification_group.lean index 9276b19d54fb1..ed286cb001bc3 100644 --- a/src/ring_theory/valuation/ramification_group.lean +++ b/src/ring_theory/valuation/ramification_group.lean @@ -9,6 +9,9 @@ import ring_theory.valuation.valuation_subring /-! # Ramification groups +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The decomposition subgroup and inertia subgroups. TODO: Define higher ramification groups in lower numbering diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean index faf017aa2555c..156e1ae708a0e 100644 --- a/src/ring_theory/valuation/valuation_subring.lean +++ b/src/ring_theory/valuation/valuation_subring.lean @@ -12,6 +12,9 @@ import algebraic_geometry.prime_spectrum.basic # Valuation subrings of a field +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Projects The order structure on `valuation_subring K`. diff --git a/src/set_theory/ordinal/notation.lean b/src/set_theory/ordinal/notation.lean index cb4d422862155..606e136c196b7 100644 --- a/src/set_theory/ordinal/notation.lean +++ b/src/set_theory/ordinal/notation.lean @@ -9,6 +9,9 @@ import set_theory.ordinal.principal /-! # Ordinal notation +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Constructive ordinal arithmetic for ordinals below `ε₀`. We define a type `onote`, with constructors `0 : onote` and `onote.oadd e n a` representing From d30d31261cdb4d2f5e612eabc3c4bf45556350d5 Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Thu, 22 Jun 2023 12:28:45 +0000 Subject: [PATCH 02/16] feat(group_theory): simple lemmas for Wedderburn (#18862) These lemmas are a bit disparate, but they are all useful for Wedderburn's little theorem. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> --- src/group_theory/group_action/basic.lean | 3 +++ src/group_theory/group_action/conj_act.lean | 6 ++++++ src/group_theory/subgroup/basic.lean | 10 ++++++++++ 3 files changed, 19 insertions(+) diff --git a/src/group_theory/group_action/basic.lean b/src/group_theory/group_action/basic.lean index 767fc4042cae6..c9dfe90ea91b9 100644 --- a/src/group_theory/group_action/basic.lean +++ b/src/group_theory/group_action/basic.lean @@ -192,6 +192,9 @@ local attribute [instance] orbit_rel variables {α} {β} +@[to_additive] +lemma orbit_rel_apply {x y : β} : (orbit_rel α β).rel x y ↔ x ∈ orbit α y := iff.rfl + /-- When you take a set `U` in `β`, push it down to the quotient, and pull back, you get the union of the orbit of `U` under `α`. -/ @[to_additive "When you take a set `U` in `β`, push it down to the quotient, and pull back, you get diff --git a/src/group_theory/group_action/conj_act.lean b/src/group_theory/group_action/conj_act.lean index 94d3aa0d6bdf4..12809e56e22d4 100644 --- a/src/group_theory/group_action/conj_act.lean +++ b/src/group_theory/group_action/conj_act.lean @@ -187,6 +187,12 @@ begin simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul] end +@[simp] lemma mem_orbit_conj_act {g h : G} : g ∈ orbit (conj_act G) h ↔ is_conj g h := +by { rw [is_conj_comm, is_conj_iff, mem_orbit_iff], refl } + +lemma orbit_rel_conj_act : (orbit_rel (conj_act G) G).rel = is_conj := +funext₂ $ λ g h, by rw [orbit_rel_apply, mem_orbit_conj_act] + lemma stabilizer_eq_centralizer (g : G) : stabilizer (conj_act G) g = (zpowers g).centralizer := le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr (λ x, mul_inv_eq_iff_eq_mul.mp))) (λ x h, mul_inv_eq_of_eq_mul (h g (mem_zpowers g)).symm) diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index 42878c5673ac4..464a9504a5aaa 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -2676,6 +2676,16 @@ begin exact subset_normal_closure (set.mem_singleton _), end +variables {M : Type*} [monoid M] + +lemma eq_of_left_mem_center {g h : M} (H : is_conj g h) (Hg : g ∈ set.center M) : + g = h := +by { rcases H with ⟨u, hu⟩, rwa [← u.mul_left_inj, ← Hg u], } + +lemma eq_of_right_mem_center {g h : M} (H : is_conj g h) (Hh : h ∈ set.center M) : + g = h := +(H.symm.eq_of_left_mem_center Hh).symm + end is_conj assert_not_exists multiset From 57f9349f2fe19d2de7207e99b0341808d977cdcf Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 22 Jun 2023 23:00:27 +0000 Subject: [PATCH 03/16] chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds (#19212) Move some lemmas that use `mfderiv` or `mdifferentiable` to new files. --- .../complex/upper_half_plane/manifold.lean | 32 +++++++++++++++++++ .../complex/upper_half_plane/topology.lean | 17 +--------- src/number_theory/modular_forms/basic.lean | 3 +- .../basic.lean} | 10 ++---- .../modular_forms/jacobi_theta/manifold.lean | 23 +++++++++++++ src/number_theory/zeta_function.lean | 2 +- 6 files changed, 61 insertions(+), 26 deletions(-) create mode 100644 src/analysis/complex/upper_half_plane/manifold.lean rename src/number_theory/modular_forms/{jacobi_theta.lean => jacobi_theta/basic.lean} (95%) create mode 100644 src/number_theory/modular_forms/jacobi_theta/manifold.lean diff --git a/src/analysis/complex/upper_half_plane/manifold.lean b/src/analysis/complex/upper_half_plane/manifold.lean new file mode 100644 index 0000000000000..b5a8b7ec6de4b --- /dev/null +++ b/src/analysis/complex/upper_half_plane/manifold.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2022 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import analysis.complex.upper_half_plane.topology +import geometry.manifold.cont_mdiff_mfderiv +/-! +# Manifold structure on the upper half plane. + +In this file we define the complex manifold structure on the upper half-plane. +-/ + +open_locale upper_half_plane manifold + +namespace upper_half_plane + +noncomputable instance : charted_space ℂ ℍ := +upper_half_plane.open_embedding_coe.singleton_charted_space + +instance : smooth_manifold_with_corners 𝓘(ℂ) ℍ := +upper_half_plane.open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(ℂ) + +/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/ +lemma smooth_coe : smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := +λ x, cont_mdiff_at_ext_chart_at + +/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/ +lemma mdifferentiable_coe : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := +smooth_coe.mdifferentiable + +end upper_half_plane diff --git a/src/analysis/complex/upper_half_plane/topology.lean b/src/analysis/complex/upper_half_plane/topology.lean index c441e99fcfe93..418466831de71 100644 --- a/src/analysis/complex/upper_half_plane/topology.lean +++ b/src/analysis/complex/upper_half_plane/topology.lean @@ -9,7 +9,6 @@ import analysis.convex.normed import analysis.convex.complex import analysis.complex.re_im_topology import topology.homotopy.contractible -import geometry.manifold.cont_mdiff_mfderiv /-! # Topology on the upper half plane @@ -20,7 +19,7 @@ various instances. noncomputable theory open set filter function topological_space complex -open_locale filter topology upper_half_plane manifold +open_locale filter topology upper_half_plane namespace upper_half_plane @@ -58,18 +57,4 @@ end instance : locally_compact_space ℍ := open_embedding_coe.locally_compact_space -instance upper_half_plane.charted_space : charted_space ℂ ℍ := -upper_half_plane.open_embedding_coe.singleton_charted_space - -instance upper_half_plane.smooth_manifold_with_corners : smooth_manifold_with_corners 𝓘(ℂ) ℍ := -upper_half_plane.open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(ℂ) - -/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/ -lemma smooth_coe : smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := -λ x, cont_mdiff_at_ext_chart_at - -/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/ -lemma mdifferentiable_coe : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := -smooth_coe.mdifferentiable - end upper_half_plane diff --git a/src/number_theory/modular_forms/basic.lean b/src/number_theory/modular_forms/basic.lean index 693f1d5696ef8..1d1346c5dfee0 100644 --- a/src/number_theory/modular_forms/basic.lean +++ b/src/number_theory/modular_forms/basic.lean @@ -3,9 +3,8 @@ Copyright (c) 2022 Chris Birkbeck. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Birkbeck -/ - import analysis.complex.upper_half_plane.functions_bounded_at_infty -import analysis.complex.upper_half_plane.topology +import analysis.complex.upper_half_plane.manifold import number_theory.modular_forms.slash_invariant_forms /-! # Modular forms diff --git a/src/number_theory/modular_forms/jacobi_theta.lean b/src/number_theory/modular_forms/jacobi_theta/basic.lean similarity index 95% rename from src/number_theory/modular_forms/jacobi_theta.lean rename to src/number_theory/modular_forms/jacobi_theta/basic.lean index 1afe11de17ba4..5dfc5e66f6a90 100644 --- a/src/number_theory/modular_forms/jacobi_theta.lean +++ b/src/number_theory/modular_forms/jacobi_theta/basic.lean @@ -19,9 +19,8 @@ and proves the modular transformation properties `θ (τ + 2) = θ τ` and show that `θ` is differentiable on `ℍ`, and `θ(τ) - 1` has exponential decay as `im τ → ∞`. -/ -open complex real asymptotics - -open_locale real big_operators upper_half_plane manifold +open complex real asymptotics filter +open_locale real big_operators upper_half_plane /-- Jacobi's theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`. -/ noncomputable def jacobi_theta (z : ℂ) : ℂ := ∑' (n : ℤ), cexp (π * I * n ^ 2 * z) @@ -151,7 +150,7 @@ end /-- The norm of `jacobi_theta τ - 1` decays exponentially as `im τ → ∞`. -/ lemma is_O_at_im_infty_jacobi_theta_sub_one : - is_O (filter.comap im filter.at_top) (λ τ, jacobi_theta τ - 1) (λ τ, rexp (-π * τ.im)) := + (λ τ, jacobi_theta τ - 1) =O[comap im at_top] (λ τ, rexp (-π * τ.im)) := begin simp_rw [is_O, is_O_with, filter.eventually_comap, filter.eventually_at_top], refine ⟨2 / (1 - rexp (-π)), 1, λ y hy z hz, (norm_jacobi_theta_sub_one_le @@ -181,8 +180,5 @@ begin exact differentiable_on_tsum_of_summable_norm bd_s h1 h2 (λ i w hw, le_bd (le_of_lt hw) i), end -lemma mdifferentiable_jacobi_theta : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobi_theta ∘ coe : ℍ → ℂ) := -λ τ, (differentiable_at_jacobi_theta τ.2).mdifferentiable_at.comp τ τ.mdifferentiable_coe - lemma continuous_at_jacobi_theta {z : ℂ} (hz : 0 < im z) : continuous_at jacobi_theta z := (differentiable_at_jacobi_theta hz).continuous_at diff --git a/src/number_theory/modular_forms/jacobi_theta/manifold.lean b/src/number_theory/modular_forms/jacobi_theta/manifold.lean new file mode 100644 index 0000000000000..67094c9757bca --- /dev/null +++ b/src/number_theory/modular_forms/jacobi_theta/manifold.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2023 David Loeffler. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Loeffler +-/ +import number_theory.modular_forms.jacobi_theta.basic +import analysis.complex.upper_half_plane.manifold + +/-! +# Manifold differentiability of the Jacobi's theta function + +In this file we reformulate differentiability of the Jacobi's theta function in terms of manifold +differentiability. + +## TODO + +Prove smoothness (in terms of `smooth`). +-/ + +open_locale upper_half_plane manifold + +lemma mdifferentiable_jacobi_theta : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobi_theta ∘ coe : ℍ → ℂ) := +λ τ, (differentiable_at_jacobi_theta τ.2).mdifferentiable_at.comp τ τ.mdifferentiable_coe diff --git a/src/number_theory/zeta_function.lean b/src/number_theory/zeta_function.lean index 4254a814864f1..b3dc94155d253 100644 --- a/src/number_theory/zeta_function.lean +++ b/src/number_theory/zeta_function.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: David Loeffler -/ import analysis.special_functions.gamma.beta -import number_theory.modular_forms.jacobi_theta +import number_theory.modular_forms.jacobi_theta.basic import number_theory.zeta_values /-! From 5d0c76894ada7940957143163d7b921345474cbc Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Fri, 23 Jun 2023 06:33:52 +0000 Subject: [PATCH 04/16] chore(*): add mathlib4 synchronization comments (#19213) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebraic_geometry.Gamma_Spec_adjunction` * `algebraic_geometry.open_immersion.Scheme` * `analysis.calculus.implicit` * `analysis.matrix` * `analysis.normed_space.matrix_exponential` * `analysis.normed_space.star.matrix` * `data.matrix.invertible` * `linear_algebra.clifford_algebra.basic` * `linear_algebra.exterior_algebra.basic` * `number_theory.cyclotomic.basic` * `number_theory.cyclotomic.primitive_roots` * `number_theory.number_field.embeddings` * `number_theory.number_field.units` * `number_theory.zsqrtd.gaussian_int` * `ring_theory.dedekind_domain.S_integer` * `ring_theory.dedekind_domain.adic_valuation` * `ring_theory.dedekind_domain.finite_adele_ring` * `ring_theory.discriminant` * `ring_theory.ideal.norm` --- src/algebraic_geometry/Gamma_Spec_adjunction.lean | 3 +++ src/algebraic_geometry/open_immersion/Scheme.lean | 3 +++ src/analysis/calculus/implicit.lean | 3 +++ src/analysis/matrix.lean | 3 +++ src/analysis/normed_space/matrix_exponential.lean | 3 +++ src/analysis/normed_space/star/matrix.lean | 3 +++ src/data/matrix/invertible.lean | 3 +++ src/linear_algebra/clifford_algebra/basic.lean | 3 +++ src/linear_algebra/exterior_algebra/basic.lean | 3 +++ src/number_theory/cyclotomic/basic.lean | 3 +++ src/number_theory/cyclotomic/primitive_roots.lean | 3 +++ src/number_theory/number_field/embeddings.lean | 3 +++ src/number_theory/number_field/units.lean | 3 +++ src/number_theory/zsqrtd/gaussian_int.lean | 3 +++ src/ring_theory/dedekind_domain/S_integer.lean | 3 +++ src/ring_theory/dedekind_domain/adic_valuation.lean | 3 +++ src/ring_theory/dedekind_domain/finite_adele_ring.lean | 3 +++ src/ring_theory/discriminant.lean | 3 +++ src/ring_theory/ideal/norm.lean | 3 +++ 19 files changed, 57 insertions(+) diff --git a/src/algebraic_geometry/Gamma_Spec_adjunction.lean b/src/algebraic_geometry/Gamma_Spec_adjunction.lean index ebe6c4c29ea3f..566db61904700 100644 --- a/src/algebraic_geometry/Gamma_Spec_adjunction.lean +++ b/src/algebraic_geometry/Gamma_Spec_adjunction.lean @@ -10,6 +10,9 @@ import category_theory.adjunction.reflective /-! # Adjunction between `Γ` and `Spec` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the adjunction `Γ_Spec.adjunction : Γ ⊣ Spec` by defining the unit (`to_Γ_Spec`, in multiple steps in this file) and counit (done in Spec.lean) and checking that they satisfy the left and right triangle identities. The constructions and proofs make use of diff --git a/src/algebraic_geometry/open_immersion/Scheme.lean b/src/algebraic_geometry/open_immersion/Scheme.lean index 571f52b4d17c3..4b930e16e1994 100644 --- a/src/algebraic_geometry/open_immersion/Scheme.lean +++ b/src/algebraic_geometry/open_immersion/Scheme.lean @@ -10,6 +10,9 @@ import category_theory.limits.shapes.comm_sq /-! # Open immersions of schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + -/ noncomputable theory diff --git a/src/analysis/calculus/implicit.lean b/src/analysis/calculus/implicit.lean index 9e4b3ecc5dca0..21bbda6901e3a 100644 --- a/src/analysis/calculus/implicit.lean +++ b/src/analysis/calculus/implicit.lean @@ -9,6 +9,9 @@ import analysis.normed_space.complemented /-! # Implicit function theorem +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We prove three versions of the implicit function theorem. First we define a structure `implicit_function_data` that holds arguments for the most general version of the implicit function theorem, see `implicit_function_data.implicit_function` diff --git a/src/analysis/matrix.lean b/src/analysis/matrix.lean index aef241badd380..45b429a99d94e 100644 --- a/src/analysis/matrix.lean +++ b/src/analysis/matrix.lean @@ -10,6 +10,9 @@ import analysis.inner_product_space.pi_L2 /-! # Matrices as a normed space +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we provide the following non-instances for norms on matrices: * The elementwise norm: diff --git a/src/analysis/normed_space/matrix_exponential.lean b/src/analysis/normed_space/matrix_exponential.lean index 529ec5ab24174..678d4710a310b 100644 --- a/src/analysis/normed_space/matrix_exponential.lean +++ b/src/analysis/normed_space/matrix_exponential.lean @@ -14,6 +14,9 @@ import topology.uniform_space.matrix /-! # Lemmas about the matrix exponential +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we provide results about `exp` on `matrix`s over a topological or normed algebra. Note that generic results over all topological spaces such as `exp_zero` can be used on matrices without issue, so are not repeated here. The topological results specific to matrices are: diff --git a/src/analysis/normed_space/star/matrix.lean b/src/analysis/normed_space/star/matrix.lean index 035eb8318992f..0de74bb3ddbeb 100644 --- a/src/analysis/normed_space/star/matrix.lean +++ b/src/analysis/normed_space/star/matrix.lean @@ -11,6 +11,9 @@ import linear_algebra.unitary_group /-! # Unitary matrices +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or `ℂ`). -/ diff --git a/src/data/matrix/invertible.lean b/src/data/matrix/invertible.lean index 0ff393baefcf3..b7ab93f0e6d2f 100644 --- a/src/data/matrix/invertible.lean +++ b/src/data/matrix/invertible.lean @@ -8,6 +8,9 @@ import data.matrix.basic /-! # Extra lemmas about invertible matrices +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Many of the `invertible` lemmas are about `*`; this restates them to be about `⬝`. For lemmas about the matrix inverse in terms of the determinant and adjugate, see `matrix.has_inv` diff --git a/src/linear_algebra/clifford_algebra/basic.lean b/src/linear_algebra/clifford_algebra/basic.lean index f6828941f3658..45eada9e874ed 100644 --- a/src/linear_algebra/clifford_algebra/basic.lean +++ b/src/linear_algebra/clifford_algebra/basic.lean @@ -11,6 +11,9 @@ import linear_algebra.quadratic_form.isometry /-! # Clifford Algebras +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We construct the Clifford algebra of a module `M` over a commutative ring `R`, equipped with a quadratic_form `Q`. diff --git a/src/linear_algebra/exterior_algebra/basic.lean b/src/linear_algebra/exterior_algebra/basic.lean index a5bc276ee5af1..ddde814780643 100644 --- a/src/linear_algebra/exterior_algebra/basic.lean +++ b/src/linear_algebra/exterior_algebra/basic.lean @@ -10,6 +10,9 @@ import linear_algebra.alternating /-! # Exterior Algebras +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We construct the exterior algebra of a module `M` over a commutative semiring `R`. ## Notation diff --git a/src/number_theory/cyclotomic/basic.lean b/src/number_theory/cyclotomic/basic.lean index abb7208658c20..cc16b9b61dbfc 100644 --- a/src/number_theory/cyclotomic/basic.lean +++ b/src/number_theory/cyclotomic/basic.lean @@ -10,6 +10,9 @@ import field_theory.galois /-! # Cyclotomic extensions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Let `A` and `B` be commutative rings with `algebra A B`. For `S : set ℕ+`, we define a class `is_cyclotomic_extension S A B` expressing the fact that `B` is obtained from `A` by adding `n`-th primitive roots of unity, for all `n ∈ S`. diff --git a/src/number_theory/cyclotomic/primitive_roots.lean b/src/number_theory/cyclotomic/primitive_roots.lean index 971334e1bba6b..af57304165afc 100644 --- a/src/number_theory/cyclotomic/primitive_roots.lean +++ b/src/number_theory/cyclotomic/primitive_roots.lean @@ -14,6 +14,9 @@ import ring_theory.polynomial.cyclotomic.expand /-! # Primitive roots in cyclotomic fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. If `is_cyclotomic_extension {n} A B`, we define an element `zeta n A B : B` that is a primitive `n`th-root of unity in `B` and we study its properties. We also prove related theorems under the more general assumption of just being a primitive root, for reasons described in the implementation diff --git a/src/number_theory/number_field/embeddings.lean b/src/number_theory/number_field/embeddings.lean index 2e1883a6753cd..a42a2fc245ed5 100644 --- a/src/number_theory/number_field/embeddings.lean +++ b/src/number_theory/number_field/embeddings.lean @@ -13,6 +13,9 @@ import topology.instances.complex /-! # Embeddings of number fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. This file defines the embeddings of a number field into an algebraic closed field. ## Main Results diff --git a/src/number_theory/number_field/units.lean b/src/number_theory/number_field/units.lean index 106abb57e6437..26fae65f4afee 100644 --- a/src/number_theory/number_field/units.lean +++ b/src/number_theory/number_field/units.lean @@ -7,6 +7,9 @@ import number_theory.number_field.norm /-! # Units of a number field + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. We prove results about the group `(𝓞 K)ˣ` of units of the ring of integers `𝓞 K` of a number field `K`. diff --git a/src/number_theory/zsqrtd/gaussian_int.lean b/src/number_theory/zsqrtd/gaussian_int.lean index 4c121a2f9f4d5..dc145904b9aaa 100644 --- a/src/number_theory/zsqrtd/gaussian_int.lean +++ b/src/number_theory/zsqrtd/gaussian_int.lean @@ -11,6 +11,9 @@ import ring_theory.principal_ideal_domain /-! # Gaussian integers +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The Gaussian integers are complex integer, complex numbers whose real and imaginary parts are both integers. diff --git a/src/ring_theory/dedekind_domain/S_integer.lean b/src/ring_theory/dedekind_domain/S_integer.lean index ec1944af6e824..a3cdfe38b2547 100644 --- a/src/ring_theory/dedekind_domain/S_integer.lean +++ b/src/ring_theory/dedekind_domain/S_integer.lean @@ -9,6 +9,9 @@ import ring_theory.dedekind_domain.adic_valuation /-! # `S`-integers and `S`-units of fraction fields of Dedekind domains +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Let `K` be the field of fractions of a Dedekind domain `R`, and let `S` be a set of prime ideals in the height one spectrum of `R`. An `S`-integer of `K` is defined to have `v`-adic valuation at most one for all primes ideals `v` away from `S`, whereas an `S`-unit of `Kˣ` is defined to have `v`-adic diff --git a/src/ring_theory/dedekind_domain/adic_valuation.lean b/src/ring_theory/dedekind_domain/adic_valuation.lean index 86e0bac6f8b44..a5d737de91673 100644 --- a/src/ring_theory/dedekind_domain/adic_valuation.lean +++ b/src/ring_theory/dedekind_domain/adic_valuation.lean @@ -11,6 +11,9 @@ import algebra.order.group.type_tags /-! # Adic valuations on Dedekind domains + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. Given a Dedekind domain `R` of Krull dimension 1 and a maximal ideal `v` of `R`, we define the `v`-adic valuation on `R` and its extension to the field of fractions `K` of `R`. We prove several properties of this valuation, including the existence of uniformizers. diff --git a/src/ring_theory/dedekind_domain/finite_adele_ring.lean b/src/ring_theory/dedekind_domain/finite_adele_ring.lean index 8c599af57d482..78cf47915dd32 100644 --- a/src/ring_theory/dedekind_domain/finite_adele_ring.lean +++ b/src/ring_theory/dedekind_domain/finite_adele_ring.lean @@ -8,6 +8,9 @@ import ring_theory.dedekind_domain.adic_valuation /-! # The finite adèle ring of a Dedekind domain + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. We define the ring of finite adèles of a Dedekind domain `R`. ## Main definitions diff --git a/src/ring_theory/discriminant.lean b/src/ring_theory/discriminant.lean index 21a559720dab7..57849e8c1f982 100644 --- a/src/ring_theory/discriminant.lean +++ b/src/ring_theory/discriminant.lean @@ -11,6 +11,9 @@ import number_theory.number_field.basic /-! # Discriminant of a family of vectors +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define the *discriminant* of `b` as the determinant of the matrix whose `(i j)`-th element is the trace of `b i * b j`. diff --git a/src/ring_theory/ideal/norm.lean b/src/ring_theory/ideal/norm.lean index b0e0cdd6fcd75..ef4f65f73d77b 100644 --- a/src/ring_theory/ideal/norm.lean +++ b/src/ring_theory/ideal/norm.lean @@ -18,6 +18,9 @@ import ring_theory.localization.norm # Ideal norms +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the absolute ideal norm `ideal.abs_norm (I : ideal R) : ℕ` as the cardinality of the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite), and the relative ideal norm `ideal.span_norm R (I : ideal S) : ideal S` as the ideal spanned by From 93f880918cb51905fd51b76add8273cbc27718ab Mon Sep 17 00:00:00 2001 From: Hanting Zhang Date: Fri, 23 Jun 2023 19:10:46 +0000 Subject: [PATCH 05/16] feat(topology/metric_space/dilation): Dilations on metric spaces (#14315) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We define `dilation α β` as the type of maps that satisfy `edist (f x) (f y) = r * edist x y` for all `x y`. Here `r : ℝ≥0`, so we do not exclude the degenerate case of dilations which collapse into constant maps. After this I will extend to `{linear, affine}_dilation_{equiv}`s and `{linear, affine}_isometry_{equiv}`s. Co-authored-by: Yury G. Kudryashov Co-authored-by: JovanGerb --- docs/references.bib | 12 + src/topology/metric_space/dilation.lean | 393 ++++++++++++++++++++++++ 2 files changed, 405 insertions(+) create mode 100644 src/topology/metric_space/dilation.lean diff --git a/docs/references.bib b/docs/references.bib index 2569176a1a9f9..d97389ddd156d 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -159,6 +159,18 @@ @Book{ behrends1979 zbl = {0436.46013} } +@Book{ berger1987, + author = {Marcel Berger}, + title = {Geometry I}, + publisher = {Springer Berlin}, + year = 1987, + issn = {0172-5939}, + pages = {XIV, 432}, + series = {Universitext}, + address = {Heidelberg}, + edition = 1 +} + @Article{ bernstein1912, author = {Bernstein, S.}, year = {1912}, diff --git a/src/topology/metric_space/dilation.lean b/src/topology/metric_space/dilation.lean new file mode 100644 index 0000000000000..24195f12cdfcb --- /dev/null +++ b/src/topology/metric_space/dilation.lean @@ -0,0 +1,393 @@ +/- +Copyright (c) 2022 Hanting Zhang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Dilations of emetric and metric spaces +Authors: Hanting Zhang +-/ +import topology.metric_space.antilipschitz +import data.fun_like.basic + +/-! +# Dilations + +We define dilations, i.e., maps between emetric spaces that satisfy +`edist (f x) (f y) = r * edist x y` for some `r ∉ {0, ∞}`. + +The value `r = 0` is not allowed because we want dilations of (e)metric spaces to be automatically +injective. The value `r = ∞` is not allowed because this way we can define `dilation.ratio f : ℝ≥0`, +not `dilation.ratio f : ℝ≥0∞`. Also, we do not often need maps sending distinct points to points at +infinite distance. + +## Main defintions + +* `dilation.ratio f : ℝ≥0`: the value of `r` in the relation above, defaulting to 1 in the case + where it is not well-defined. + +## Implementation notes + +The type of dilations defined in this file are also referred to as "similarities" or "similitudes" +by other authors. The name `dilation` was choosen to match the Wikipedia name. + +Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the +theory for `pseudo_emetric_space` and we specialize to `pseudo_metric_space` and `metric_space` when +needed. + +## TODO + +- Introduce dilation equivs. +- Refactor the `isometry` API to match the `*_hom_class` API below. + +## References + +- https://en.wikipedia.org/wiki/Dilation_(metric_space) +- [Marcel Berger, *Geometry*][berger1987] +-/ + +noncomputable theory + +open function set +open_locale topology ennreal nnreal classical + +section defs + +variables (α : Type*) (β : Type*) [pseudo_emetric_space α] [pseudo_emetric_space β] + +/-- A dilation is a map that uniformly scales the edistance between any two points. -/ +structure dilation := +(to_fun : α → β) +(edist_eq' : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, edist (to_fun x) (to_fun y) = r * edist x y) + +/-- +`dilation_class F α β r` states that `F` is a type of `r`-dilations. +You should extend this typeclass when you extend `dilation`. +-/ +class dilation_class (F : Type*) (α β : out_param $ Type*) + [pseudo_emetric_space α] [pseudo_emetric_space β] extends fun_like F α (λ _, β) := +(edist_eq' : ∀ (f : F), ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = r * edist x y) + +end defs + +namespace dilation +variables {α : Type*} {β : Type*} {γ : Type*} {F : Type*} {G : Type*} + +section setup +variables [pseudo_emetric_space α] [pseudo_emetric_space β] + +instance to_dilation_class : + dilation_class (dilation α β) α β := +{ coe := to_fun, + coe_injective' := λ f g h, by { cases f; cases g; congr', }, + edist_eq' := λ f, edist_eq' f } + +instance : has_coe_to_fun (dilation α β) (λ _, α → β) := fun_like.has_coe_to_fun + +@[simp] lemma to_fun_eq_coe {f : dilation α β} : f.to_fun = (f : α → β) := rfl + +@[simp] lemma coe_mk (f : α → β) (h) : ⇑(⟨f, h⟩ : dilation α β) = f := rfl + +lemma congr_fun {f g : dilation α β} (h : f = g) (x : α) : f x = g x := fun_like.congr_fun h x +lemma congr_arg (f : dilation α β) {x y : α} (h : x = y) : f x = f y := fun_like.congr_arg f h + +@[ext] theorem ext {f g : dilation α β} (h : ∀ x, f x = g x) : f = g := +fun_like.ext f g h + +lemma ext_iff {f g : dilation α β} : f = g ↔ ∀ x, f x = g x := fun_like.ext_iff + +@[simp] lemma mk_coe (f : dilation α β) (h) : dilation.mk f h = f := ext $ λ _, rfl + +/-- Copy of a `dilation` with a new `to_fun` equal to the old one. Useful to fix definitional +equalities. -/ +@[simps { fully_applied := ff }] +protected def copy (f : dilation α β) (f' : α → β) (h : f' = ⇑f) : dilation α β := +{ to_fun := f', + edist_eq' := h.symm ▸ f.edist_eq' } + +lemma copy_eq_self (f : dilation α β) {f' : α → β} (h : f' = f) : f.copy f' h = f := +fun_like.ext' h + +/-- The ratio of a dilation `f`. If the ratio is undefined (i.e., the distance between any two +points in `α` is either zero or infinity), then we choose one as the ratio. -/ +def ratio [dilation_class F α β] (f : F) : ℝ≥0 := +if ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤ then 1 else (dilation_class.edist_eq' f).some + +lemma ratio_ne_zero [dilation_class F α β] (f : F) : ratio f ≠ 0 := +begin + rw ratio, split_ifs, + { exact one_ne_zero, }, + exact (dilation_class.edist_eq' f).some_spec.1, +end + +lemma ratio_pos [dilation_class F α β] (f : F) : 0 < ratio f := +(ratio_ne_zero f).bot_lt + +@[simp] lemma edist_eq [dilation_class F α β] (f : F) (x y : α) : + edist (f x) (f y) = ratio f * edist x y := +begin + rw ratio, split_ifs with key, + { rcases dilation_class.edist_eq' f with ⟨r, hne, hr⟩, + replace hr := hr x y, + cases key x y, + { simp only [hr, h, mul_zero] }, + { simp [hr, h, hne] } }, + exact (dilation_class.edist_eq' f).some_spec.2 x y, +end + +@[simp] lemma nndist_eq {α β F : Type*} [pseudo_metric_space α] [pseudo_metric_space β] + [dilation_class F α β] (f : F) (x y : α) : nndist (f x) (f y) = ratio f * nndist x y := +by simp only [← ennreal.coe_eq_coe, ← edist_nndist, ennreal.coe_mul, edist_eq] + +@[simp] lemma dist_eq {α β F : Type*} [pseudo_metric_space α] [pseudo_metric_space β] + [dilation_class F α β] (f : F) (x y : α) : dist (f x) (f y) = ratio f * dist x y := +by simp only [dist_nndist, nndist_eq, nnreal.coe_mul] + +/-- The `ratio` is equal to the distance ratio for any two points with nonzero finite distance. +`dist` and `nndist` versions below -/ +lemma ratio_unique [dilation_class F α β] {f : F} {x y : α} {r : ℝ≥0} + (h₀ : edist x y ≠ 0) (htop : edist x y ≠ ⊤) (hr : edist (f x) (f y) = r * edist x y) : + r = ratio f := +by simpa only [hr, ennreal.mul_eq_mul_right h₀ htop, ennreal.coe_eq_coe] using edist_eq f x y + +/-- The `ratio` is equal to the distance ratio for any two points +with nonzero finite distance; `nndist` version -/ +lemma ratio_unique_of_nndist_ne_zero {α β F : Type*} [pseudo_metric_space α] [pseudo_metric_space β] + [dilation_class F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : nndist x y ≠ 0) + (hr : nndist (f x) (f y) = r * nndist x y) : r = ratio f := +ratio_unique (by rwa [edist_nndist, ennreal.coe_ne_zero]) (edist_ne_top x y) + (by rw [edist_nndist, edist_nndist, hr, ennreal.coe_mul]) + +/-- The `ratio` is equal to the distance ratio for any two points +with nonzero finite distance; `dist` version -/ +lemma ratio_unique_of_dist_ne_zero {α β} {F : Type*} [pseudo_metric_space α] [pseudo_metric_space β] + [dilation_class F α β] {f : F} {x y : α} {r : ℝ≥0} + (hxy : dist x y ≠ 0) (hr : dist (f x) (f y) = r * dist x y) : + r = ratio f := +ratio_unique_of_nndist_ne_zero (nnreal.coe_ne_zero.1 hxy) $ nnreal.eq $ + by rw [coe_nndist, hr, nnreal.coe_mul, coe_nndist] + +/-- Alternative `dilation` constructor when the distance hypothesis is over `nndist` -/ +def mk_of_nndist_eq {α β} + [pseudo_metric_space α] [pseudo_metric_space β] + (f : α → β) (h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) : + dilation α β := +{ to_fun := f, + edist_eq' := + begin + rcases h with ⟨r, hne, h⟩, + refine ⟨r, hne, λ x y, _⟩, + rw [edist_nndist, edist_nndist, ← ennreal.coe_mul, h x y], + end } + +@[simp] lemma coe_mk_of_nndist_eq {α β} + [pseudo_metric_space α] [pseudo_metric_space β] + (f : α → β) (h) : ⇑(mk_of_nndist_eq f h : dilation α β) = f := rfl + +@[simp] lemma mk_coe_of_nndist_eq {α β} + [pseudo_metric_space α] [pseudo_metric_space β] + (f : dilation α β) (h) : dilation.mk_of_nndist_eq f h = f := +ext $ λ _, rfl + +/-- Alternative `dilation` constructor when the distance hypothesis is over `dist` -/ +def mk_of_dist_eq {α β} + [pseudo_metric_space α] [pseudo_metric_space β] + (f : α → β) (h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = r * dist x y) : + dilation α β := +mk_of_nndist_eq f $ h.imp $ λ r hr, + ⟨hr.1, λ x y, nnreal.eq $ by rw [coe_nndist, hr.2, nnreal.coe_mul, coe_nndist]⟩ + +@[simp] lemma coe_mk_of_dist_eq {α β} + [pseudo_metric_space α] [pseudo_metric_space β] + (f : α → β) (h) : ⇑(mk_of_dist_eq f h : dilation α β) = f := rfl + +@[simp] lemma mk_coe_of_dist_eq {α β} + [pseudo_metric_space α] [pseudo_metric_space β] + (f : dilation α β) (h) : dilation.mk_of_dist_eq f h = f := +ext $ λ _, rfl + +end setup + +section pseudo_emetric_dilation +variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] +variables [dilation_class F α β] [dilation_class G β γ] +variables (f : F) (g : G) {x y z : α} {s : set α} + +lemma lipschitz : lipschitz_with (ratio f) (f : α → β) := λ x y, (edist_eq f x y).le + +lemma antilipschitz : antilipschitz_with (ratio f)⁻¹ (f : α → β) := +λ x y, have hr : ratio f ≠ 0 := ratio_ne_zero f, by exact_mod_cast + (ennreal.mul_le_iff_le_inv (ennreal.coe_ne_zero.2 hr) ennreal.coe_ne_top).1 (edist_eq f x y).ge + +/-- A dilation from an emetric space is injective -/ +protected lemma injective {α : Type*} [emetric_space α] [dilation_class F α β] (f : F) : + injective f := (antilipschitz f).injective + +/-- The identity is a dilation -/ +protected def id (α) [pseudo_emetric_space α] : dilation α α := +{ to_fun := _root_.id, + edist_eq' := ⟨1, one_ne_zero, λ x y, by simp only [id.def, ennreal.coe_one, one_mul]⟩ } + +instance : inhabited (dilation α α) := ⟨dilation.id α⟩ + +@[simp, protected] lemma coe_id : ⇑(dilation.id α) = id := rfl + +lemma id_ratio : ratio (dilation.id α) = 1 := +begin + by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞, + { rw [ratio, if_pos h] }, + { push_neg at h, + rcases h with ⟨x, y, hne⟩, + refine (ratio_unique hne.1 hne.2 _).symm, + simp } +end + +/-- The composition of dilations is a dilation -/ +def comp (g : dilation β γ) (f : dilation α β) : dilation α γ := +{ to_fun := g ∘ f, + edist_eq' := ⟨ratio g * ratio f, + mul_ne_zero (ratio_ne_zero g) (ratio_ne_zero f), + λ x y, by { simp only [edist_eq, ennreal.coe_mul], ring, }⟩ } + +lemma comp_assoc {δ : Type*} [pseudo_emetric_space δ] + (f : dilation α β) (g : dilation β γ) (h : dilation γ δ) : + (h.comp g).comp f = h.comp (g.comp f) := rfl + +@[simp] lemma coe_comp (g : dilation β γ) (f : dilation α β) : + (g.comp f : α → γ) = g ∘ f := rfl + +lemma comp_apply (g : dilation β γ) (f : dilation α β) (x : α) : + (g.comp f : α → γ) x = (g (f x)) := rfl + +/-- Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume +that the domain `α` of `f` is nontrivial, otherwise `ratio f = ratio (g.comp f) = 1` but `ratio g` +may have any value. -/ +@[simp] lemma comp_ratio + {g : dilation β γ} {f : dilation α β} (hne : ∃ x y : α, edist x y ≠ 0 ∧ edist x y ≠ ⊤) : + ratio (g.comp f) = ratio g * ratio f := +begin + rcases hne with ⟨x, y, hα⟩, + have hgf := (edist_eq (g.comp f) x y).symm, + simp only [dist_eq, coe_comp, ← mul_assoc, mul_eq_mul_right_iff] at hgf, + rw [edist_eq, edist_eq, ← mul_assoc, ennreal.mul_eq_mul_right hα.1 hα.2] at hgf, + rwa [← ennreal.coe_eq_coe, ennreal.coe_mul], +end + +@[simp] lemma comp_id (f : dilation α β) : f.comp (dilation.id α) = f := ext $ λ x, rfl + +@[simp] lemma id_comp (f : dilation α β) : (dilation.id β).comp f = f := ext $ λ x, rfl + +instance : monoid (dilation α α) := +{ one := dilation.id α, + mul := comp, + mul_one := comp_id, + one_mul := id_comp, + mul_assoc := λ f g h, comp_assoc _ _ _ } + +lemma one_def : (1 : dilation α α) = dilation.id α := rfl +lemma mul_def (f g : dilation α α) : f * g = f.comp g := rfl + +@[simp] lemma coe_one : ⇑(1 : dilation α α) = _root_.id := rfl +@[simp] lemma coe_mul (f g : dilation α α) : ⇑(f * g) = f ∘ g := rfl + +lemma cancel_right {g₁ g₂ : dilation β γ} {f : dilation α β} (hf : surjective f) : + g₁.comp f = g₂.comp f ↔ g₁ = g₂ := +⟨λ h, dilation.ext $ hf.forall.2 (ext_iff.1 h), λ h, h ▸ rfl⟩ + +lemma cancel_left {g : dilation β γ} {f₁ f₂ : dilation α β} (hg : injective g) : + g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ := +⟨λ h, dilation.ext $ λ x, hg $ by rw [← comp_apply, h, comp_apply], λ h, h ▸ rfl⟩ + +/-- A dilation from a metric space is a uniform inducing map -/ +protected theorem uniform_inducing : uniform_inducing (f : α → β) := +(antilipschitz f).uniform_inducing (lipschitz f).uniform_continuous + +lemma tendsto_nhds_iff {ι : Type*} {g : ι → α} {a : filter ι} {b : α} : + filter.tendsto g a (𝓝 b) ↔ filter.tendsto ((f : α → β) ∘ g) a (𝓝 (f b)) := +(dilation.uniform_inducing f).inducing.tendsto_nhds_iff + +/-- A dilation is continuous. -/ +lemma to_continuous : continuous (f : α → β) := +(lipschitz f).continuous + +/-- Dilations scale the diameter by `ratio f` in pseudoemetric spaces. -/ +lemma ediam_image (s : set α) : + emetric.diam ((f : α → β) '' s) = ratio f * emetric.diam s := +begin + refine ((lipschitz f).ediam_image_le s).antisymm _, + apply ennreal.mul_le_of_le_div', + rw [div_eq_mul_inv, mul_comm, ← ennreal.coe_inv], + exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f], +end + +/-- A dilation scales the diameter of the range by `ratio f`. -/ +lemma ediam_range : + emetric.diam (range (f : α → β)) = ratio f * emetric.diam (univ : set α) := +by { rw ← image_univ, exact ediam_image f univ } + +/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/ +lemma maps_to_emetric_ball (x : α) (r : ℝ≥0∞) : + maps_to (f : α → β) (emetric.ball x r) (emetric.ball (f x) (ratio f * r)) := +λ y hy, (edist_eq f y x).trans_lt $ + (ennreal.mul_lt_mul_left (ennreal.coe_ne_zero.2 $ ratio_ne_zero f) ennreal.coe_ne_top).2 hy + +/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/ +lemma maps_to_emetric_closed_ball (x : α) (r' : ℝ≥0∞) : + maps_to (f : α → β) (emetric.closed_ball x r') (emetric.closed_ball (f x) (ratio f * r')) := +λ y hy, (edist_eq f y x).trans_le $ mul_le_mul_left' hy _ + +lemma comp_continuous_on_iff {γ} [topological_space γ] {g : γ → α} {s : set γ} : + continuous_on ((f : α → β) ∘ g) s ↔ continuous_on g s := +(dilation.uniform_inducing f).inducing.continuous_on_iff.symm + +lemma comp_continuous_iff {γ} [topological_space γ] {g : γ → α} : + continuous ((f : α → β) ∘ g) ↔ continuous g := +(dilation.uniform_inducing f).inducing.continuous_iff.symm + +end pseudo_emetric_dilation --section + +section emetric_dilation +variables [emetric_space α] + +/-- A dilation from a metric space is a uniform embedding -/ +protected theorem uniform_embedding [pseudo_emetric_space β] [dilation_class F α β] + (f : F) : uniform_embedding f := +(antilipschitz f).uniform_embedding (lipschitz f).uniform_continuous + +/-- A dilation from a metric space is an embedding -/ +protected theorem embedding [pseudo_emetric_space β] [dilation_class F α β] + (f : F) : embedding (f : α → β) := +(dilation.uniform_embedding f).embedding + +/-- A dilation from a complete emetric space is a closed embedding -/ +protected theorem closed_embedding [complete_space α] [emetric_space β] [dilation_class F α β] + (f : F) : closed_embedding f := +(antilipschitz f).closed_embedding (lipschitz f).uniform_continuous + +end emetric_dilation --section + +section pseudo_metric_dilation +variables [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) + +/-- A dilation scales the diameter by `ratio f` in pseudometric spaces. -/ +lemma diam_image (s : set α) : metric.diam ((f : α → β) '' s) = ratio f * metric.diam s := +by { simp [metric.diam, ediam_image, ennreal.to_real_mul], } + +lemma diam_range : metric.diam (range (f : α → β)) = ratio f * metric.diam (univ : set α) := +by rw [← image_univ, diam_image] + +/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/ +lemma maps_to_ball (x : α) (r' : ℝ) : + maps_to (f : α → β) (metric.ball x r') (metric.ball (f x) (ratio f * r')) := +λ y hy, (dist_eq f y x).trans_lt $ (mul_lt_mul_left $ nnreal.coe_pos.2 $ ratio_pos f).2 hy + +/-- A dilation maps spheres to spheres and scales the radius by `ratio f`. -/ +lemma maps_to_sphere (x : α) (r' : ℝ) : + maps_to (f : α → β) (metric.sphere x r') (metric.sphere (f x) (ratio f * r')) := +λ y hy, metric.mem_sphere.mp hy ▸ dist_eq f y x + +/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/ +lemma maps_to_closed_ball (x : α) (r' : ℝ) : + maps_to (f : α → β) (metric.closed_ball x r') (metric.closed_ball (f x) (ratio f * r')) := +λ y hy, (dist_eq f y x).trans_le $ mul_le_mul_of_nonneg_left hy (nnreal.coe_nonneg _) + +end pseudo_metric_dilation -- section + +end dilation From fdc286cc6967a012f41b87f76dcd2797b53152af Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Sat, 24 Jun 2023 06:34:52 +0000 Subject: [PATCH 06/16] chore(*): add mathlib4 synchronization comments (#19214) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebraic_geometry.presheafed_space.gluing` * `analysis.calculus.bump_function_findim` * `field_theory.polynomial_galois_group` * `geometry.manifold.sheaf.basic` * `linear_algebra.clifford_algebra.conjugation` * `linear_algebra.clifford_algebra.grading` * `linear_algebra.clifford_algebra.star` * `linear_algebra.free_module.norm` * `number_theory.cyclotomic.discriminant` * `number_theory.legendre_symbol.add_character` * `number_theory.number_field.canonical_embedding` --- src/algebraic_geometry/presheafed_space/gluing.lean | 3 +++ src/analysis/calculus/bump_function_findim.lean | 3 +++ src/field_theory/polynomial_galois_group.lean | 3 +++ src/geometry/manifold/sheaf/basic.lean | 3 +++ src/linear_algebra/clifford_algebra/conjugation.lean | 3 +++ src/linear_algebra/clifford_algebra/grading.lean | 3 +++ src/linear_algebra/clifford_algebra/star.lean | 3 +++ src/linear_algebra/free_module/norm.lean | 3 +++ src/number_theory/cyclotomic/discriminant.lean | 3 +++ src/number_theory/legendre_symbol/add_character.lean | 3 +++ src/number_theory/number_field/canonical_embedding.lean | 3 +++ 11 files changed, 33 insertions(+) diff --git a/src/algebraic_geometry/presheafed_space/gluing.lean b/src/algebraic_geometry/presheafed_space/gluing.lean index 8f214a1122052..c964bb9f338bf 100644 --- a/src/algebraic_geometry/presheafed_space/gluing.lean +++ b/src/algebraic_geometry/presheafed_space/gluing.lean @@ -10,6 +10,9 @@ import algebraic_geometry.locally_ringed_space.has_colimits /-! # Gluing Structured spaces +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Given a family of gluing data of structured spaces (presheafed spaces, sheafed spaces, or locally ringed spaces), we may glue them together. diff --git a/src/analysis/calculus/bump_function_findim.lean b/src/analysis/calculus/bump_function_findim.lean index 67a52967d0b5a..b46cf1c50c964 100644 --- a/src/analysis/calculus/bump_function_findim.lean +++ b/src/analysis/calculus/bump_function_findim.lean @@ -12,6 +12,9 @@ import data.set.pointwise.support /-! # Bump functions in finite-dimensional vector spaces +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Let `E` be a finite-dimensional real normed vector space. We show that any open set `s` in `E` is exactly the support of a smooth function taking values in `[0, 1]`, in `is_open.exists_smooth_support_eq`. diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean index d25a4855e0602..d522d1b6ba71f 100644 --- a/src/field_theory/polynomial_galois_group.lean +++ b/src/field_theory/polynomial_galois_group.lean @@ -10,6 +10,9 @@ import group_theory.perm.cycle.type /-! # Galois Groups of Polynomials +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we introduce the Galois group of a polynomial `p` over a field `F`, defined as the automorphism group of its splitting field. We also provide some results about some extension `E` above `p.splitting_field`, and some specific diff --git a/src/geometry/manifold/sheaf/basic.lean b/src/geometry/manifold/sheaf/basic.lean index 35fe4545d0d01..5c4722153c102 100644 --- a/src/geometry/manifold/sheaf/basic.lean +++ b/src/geometry/manifold/sheaf/basic.lean @@ -8,6 +8,9 @@ import topology.sheaves.local_predicate /-! # Generic construction of a sheaf from a `local_invariant_prop` on a manifold +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file constructs the sheaf-of-types of functions `f : M → M'` (for charted spaces `M`, `M'`) which satisfy the lifted property `lift_prop P` associated to some locally invariant (in the sense of `structure_groupoid.local_invariant_prop`) property `P` on the model spaces of `M` and `M'`. For diff --git a/src/linear_algebra/clifford_algebra/conjugation.lean b/src/linear_algebra/clifford_algebra/conjugation.lean index 07f8f5174fd87..f25611184e923 100644 --- a/src/linear_algebra/clifford_algebra/conjugation.lean +++ b/src/linear_algebra/clifford_algebra/conjugation.lean @@ -9,6 +9,9 @@ import algebra.module.opposites /-! # Conjugations +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the grade reversal and grade involution functions on multivectors, `reverse` and `involute`. Together, these operations compose to form the "Clifford conjugate", hence the name of this file. diff --git a/src/linear_algebra/clifford_algebra/grading.lean b/src/linear_algebra/clifford_algebra/grading.lean index d32e266c568e9..6e9f3a429a818 100644 --- a/src/linear_algebra/clifford_algebra/grading.lean +++ b/src/linear_algebra/clifford_algebra/grading.lean @@ -10,6 +10,9 @@ import ring_theory.graded_algebra.basic /-! # Results about the grading structure of the clifford algebra +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The main result is `clifford_algebra.graded_algebra`, which says that the clifford algebra is a ℤ₂-graded algebra (or "superalgebra"). -/ diff --git a/src/linear_algebra/clifford_algebra/star.lean b/src/linear_algebra/clifford_algebra/star.lean index 9c340fcbcb04f..697a4b2f4464d 100644 --- a/src/linear_algebra/clifford_algebra/star.lean +++ b/src/linear_algebra/clifford_algebra/star.lean @@ -8,6 +8,9 @@ import linear_algebra.clifford_algebra.conjugation /-! # Star structure on `clifford_algebra` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the "clifford conjugation", equal to `reverse (involute x)`, and assigns it the `star` notation. diff --git a/src/linear_algebra/free_module/norm.lean b/src/linear_algebra/free_module/norm.lean index 7f73836649fac..f9366158ef8a6 100644 --- a/src/linear_algebra/free_module/norm.lean +++ b/src/linear_algebra/free_module/norm.lean @@ -9,6 +9,9 @@ import ring_theory.norm /-! # Norms on free modules over principal ideal domains + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. -/ open ideal polynomial diff --git a/src/number_theory/cyclotomic/discriminant.lean b/src/number_theory/cyclotomic/discriminant.lean index f92f560b96935..1875990e97556 100644 --- a/src/number_theory/cyclotomic/discriminant.lean +++ b/src/number_theory/cyclotomic/discriminant.lean @@ -9,6 +9,9 @@ import ring_theory.discriminant /-! # Discriminant of cyclotomic fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. We compute the discriminant of a `p ^ n`-th cyclotomic extension. ## Main results diff --git a/src/number_theory/legendre_symbol/add_character.lean b/src/number_theory/legendre_symbol/add_character.lean index e35db8da04b63..47de7d6d7729b 100644 --- a/src/number_theory/legendre_symbol/add_character.lean +++ b/src/number_theory/legendre_symbol/add_character.lean @@ -9,6 +9,9 @@ import field_theory.finite.trace /-! # Additive characters of finite rings and fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Let `R` be a finite commutative ring. An *additive character* of `R` with values in another commutative ring `R'` is simply a morphism from the additive group of `R` into the multiplicative monoid of `R'`. diff --git a/src/number_theory/number_field/canonical_embedding.lean b/src/number_theory/number_field/canonical_embedding.lean index bdcc13bebd7ef..d3b0066683505 100644 --- a/src/number_theory/number_field/canonical_embedding.lean +++ b/src/number_theory/number_field/canonical_embedding.lean @@ -8,6 +8,9 @@ import number_theory.number_field.embeddings /-! # Canonical embedding of a number field +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The canonical embedding of a number field `K` of signature `(r₁, r₂)` is the ring homomorphism `K →+* ℝ^r₁ × ℂ^r₂` that sends `x ∈ K` to `(φ_₁(x),...,φ_r₁(x)) × (ψ_₁(x),..., ψ_r₂(x))` where `φ_₁,...,φ_r₁` are its real embeddings and `ψ_₁,..., ψ_r₂` are its complex embeddings (up to From 30faa0c3618ce1472bf6305ae0e3fa56affa3f95 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Mon, 26 Jun 2023 04:51:08 +0000 Subject: [PATCH 07/16] chore(*): add mathlib4 synchronization comments (#19215) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `field_theory.abel_ruffini` * `geometry.manifold.algebra.lie_group` * `geometry.manifold.algebra.monoid` * `geometry.manifold.algebra.structures` * `geometry.manifold.bump_function` * `geometry.manifold.cont_mdiff` * `geometry.manifold.cont_mdiff_map` * `geometry.manifold.vector_bundle.basic` * `geometry.manifold.vector_bundle.fiberwise_linear` * `geometry.manifold.vector_bundle.pullback` * `geometry.manifold.vector_bundle.tangent` * `linear_algebra.clifford_algebra.equivs` * `linear_algebra.clifford_algebra.fold` * `number_theory.class_number.finite` * `number_theory.class_number.function_field` * `number_theory.cyclotomic.gal` * `number_theory.cyclotomic.rat` * `number_theory.number_field.class_number` * `representation_theory.group_cohomology.resolution` * `topology.metric_space.dilation` --- src/field_theory/abel_ruffini.lean | 3 +++ src/geometry/manifold/algebra/lie_group.lean | 3 +++ src/geometry/manifold/algebra/monoid.lean | 3 +++ src/geometry/manifold/algebra/structures.lean | 3 +++ src/geometry/manifold/bump_function.lean | 3 +++ src/geometry/manifold/cont_mdiff.lean | 3 +++ src/geometry/manifold/cont_mdiff_map.lean | 3 +++ src/geometry/manifold/vector_bundle/basic.lean | 3 +++ src/geometry/manifold/vector_bundle/fiberwise_linear.lean | 3 +++ src/geometry/manifold/vector_bundle/pullback.lean | 3 +++ src/geometry/manifold/vector_bundle/tangent.lean | 3 +++ src/linear_algebra/clifford_algebra/equivs.lean | 3 +++ src/linear_algebra/clifford_algebra/fold.lean | 3 +++ src/number_theory/class_number/finite.lean | 3 +++ src/number_theory/class_number/function_field.lean | 3 +++ src/number_theory/cyclotomic/gal.lean | 3 +++ src/number_theory/cyclotomic/rat.lean | 3 +++ src/number_theory/number_field/class_number.lean | 3 +++ src/representation_theory/group_cohomology/resolution.lean | 3 +++ src/topology/metric_space/dilation.lean | 3 +++ 20 files changed, 60 insertions(+) diff --git a/src/field_theory/abel_ruffini.lean b/src/field_theory/abel_ruffini.lean index aa5760145959a..8c54b0d3de584 100644 --- a/src/field_theory/abel_ruffini.lean +++ b/src/field_theory/abel_ruffini.lean @@ -11,6 +11,9 @@ import ring_theory.roots_of_unity.basic /-! # The Abel-Ruffini Theorem +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file proves one direction of the Abel-Ruffini theorem, namely that if an element is solvable by radicals, then its minimal polynomial has solvable Galois group. diff --git a/src/geometry/manifold/algebra/lie_group.lean b/src/geometry/manifold/algebra/lie_group.lean index 32933bde56c91..90009628761f9 100644 --- a/src/geometry/manifold/algebra/lie_group.lean +++ b/src/geometry/manifold/algebra/lie_group.lean @@ -9,6 +9,9 @@ import geometry.manifold.algebra.monoid /-! # Lie groups +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + A Lie group is a group that is also a smooth manifold, in which the group operations of multiplication and inversion are smooth maps. Smoothness of the group multiplication means that multiplication is a smooth mapping of the product manifold `G` × `G` into `G`. diff --git a/src/geometry/manifold/algebra/monoid.lean b/src/geometry/manifold/algebra/monoid.lean index 79d38983c7054..3c2be5411253f 100644 --- a/src/geometry/manifold/algebra/monoid.lean +++ b/src/geometry/manifold/algebra/monoid.lean @@ -8,6 +8,9 @@ import geometry.manifold.cont_mdiff_map /-! # Smooth monoid + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. A smooth monoid is a monoid that is also a smooth manifold, in which multiplication is a smooth map of the product manifold `G` × `G` into `G`. diff --git a/src/geometry/manifold/algebra/structures.lean b/src/geometry/manifold/algebra/structures.lean index b8fad067971af..e90599f0c066d 100644 --- a/src/geometry/manifold/algebra/structures.lean +++ b/src/geometry/manifold/algebra/structures.lean @@ -8,6 +8,9 @@ import geometry.manifold.algebra.lie_group /-! # Smooth structures +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define smooth structures that build on Lie groups. We prefer using the term smooth instead of Lie mainly because Lie ring has currently another use in mathematics. -/ diff --git a/src/geometry/manifold/bump_function.lean b/src/geometry/manifold/bump_function.lean index 80262412fa133..c301d8103d3f4 100644 --- a/src/geometry/manifold/bump_function.lean +++ b/src/geometry/manifold/bump_function.lean @@ -9,6 +9,9 @@ import geometry.manifold.cont_mdiff /-! # Smooth bump functions on a smooth manifold +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define `smooth_bump_function I c` to be a bundled smooth "bump" function centered at `c`. It is a structure that consists of two real numbers `0 < r < R` with small enough `R`. We define a coercion to function for this type, and for `f : smooth_bump_function I c`, the function diff --git a/src/geometry/manifold/cont_mdiff.lean b/src/geometry/manifold/cont_mdiff.lean index e6205468df232..2ffd0e1c3c7d8 100644 --- a/src/geometry/manifold/cont_mdiff.lean +++ b/src/geometry/manifold/cont_mdiff.lean @@ -9,6 +9,9 @@ import geometry.manifold.local_invariant_properties /-! # Smooth functions between smooth manifolds +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define `Cⁿ` functions between smooth manifolds, as functions which are `Cⁿ` in charts, and prove basic properties of these notions. diff --git a/src/geometry/manifold/cont_mdiff_map.lean b/src/geometry/manifold/cont_mdiff_map.lean index 9b736749c8f52..e5c95ee2813fd 100644 --- a/src/geometry/manifold/cont_mdiff_map.lean +++ b/src/geometry/manifold/cont_mdiff_map.lean @@ -10,6 +10,9 @@ import topology.continuous_function.basic /-! # Smooth bundled map +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define the type `cont_mdiff_map` of `n` times continuously differentiable bundled maps. -/ diff --git a/src/geometry/manifold/vector_bundle/basic.lean b/src/geometry/manifold/vector_bundle/basic.lean index 5bef774d46b7f..49445ccc558dc 100644 --- a/src/geometry/manifold/vector_bundle/basic.lean +++ b/src/geometry/manifold/vector_bundle/basic.lean @@ -8,6 +8,9 @@ import topology.vector_bundle.constructions /-! # Smooth vector bundles +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines smooth vector bundles over a smooth manifold. Let `E` be a topological vector bundle, with model fiber `F` and base space `B`. We consider `E` as diff --git a/src/geometry/manifold/vector_bundle/fiberwise_linear.lean b/src/geometry/manifold/vector_bundle/fiberwise_linear.lean index cd9e5a761d63a..d2253f00b568d 100644 --- a/src/geometry/manifold/vector_bundle/fiberwise_linear.lean +++ b/src/geometry/manifold/vector_bundle/fiberwise_linear.lean @@ -7,6 +7,9 @@ import geometry.manifold.cont_mdiff /-! # The groupoid of smooth, fiberwise-linear maps +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains preliminaries for the definition of a smooth vector bundle: an associated `structure_groupoid`, the groupoid of `smooth_fiberwise_linear` functions. -/ diff --git a/src/geometry/manifold/vector_bundle/pullback.lean b/src/geometry/manifold/vector_bundle/pullback.lean index c65bc33987d01..44c3c92709f7c 100644 --- a/src/geometry/manifold/vector_bundle/pullback.lean +++ b/src/geometry/manifold/vector_bundle/pullback.lean @@ -8,6 +8,9 @@ import geometry.manifold.vector_bundle.basic /-! # Pullbacks of smooth vector bundles +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines pullbacks of smooth vector bundles over a smooth manifold. ## Main definitions diff --git a/src/geometry/manifold/vector_bundle/tangent.lean b/src/geometry/manifold/vector_bundle/tangent.lean index f5cd27d8429a8..55d597435cb96 100644 --- a/src/geometry/manifold/vector_bundle/tangent.lean +++ b/src/geometry/manifold/vector_bundle/tangent.lean @@ -8,6 +8,9 @@ import geometry.manifold.vector_bundle.basic /-! # Tangent bundles +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the tangent bundle as a smooth vector bundle. Let `M` be a smooth manifold with corners with model `I` on `(E, H)`. We define the tangent bundle diff --git a/src/linear_algebra/clifford_algebra/equivs.lean b/src/linear_algebra/clifford_algebra/equivs.lean index fbfc724ea7963..2c5bf524e78a8 100644 --- a/src/linear_algebra/clifford_algebra/equivs.lean +++ b/src/linear_algebra/clifford_algebra/equivs.lean @@ -13,6 +13,9 @@ import linear_algebra.quadratic_form.prod /-! # Other constructions isomorphic to Clifford Algebras +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains isomorphisms showing that other types are equivalent to some `clifford_algebra`. ## Rings diff --git a/src/linear_algebra/clifford_algebra/fold.lean b/src/linear_algebra/clifford_algebra/fold.lean index 625219a22945a..353aed894e0f3 100644 --- a/src/linear_algebra/clifford_algebra/fold.lean +++ b/src/linear_algebra/clifford_algebra/fold.lean @@ -8,6 +8,9 @@ import linear_algebra.clifford_algebra.conjugation /-! # Recursive computation rules for the Clifford algebra +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file provides API for a special case `clifford_algebra.foldr` of the universal property `clifford_algebra.lift` with `A = module.End R N` for some arbitrary module `N`. This specialization resembles the `list.foldr` operation, allowing a bilinear map to be "folded" along the generators. diff --git a/src/number_theory/class_number/finite.lean b/src/number_theory/class_number/finite.lean index 3e868fbb2d3b7..bae910d2a816e 100644 --- a/src/number_theory/class_number/finite.lean +++ b/src/number_theory/class_number/finite.lean @@ -14,6 +14,9 @@ import ring_theory.norm /-! # Class numbers of global fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. In this file, we use the notion of "admissible absolute value" to prove finiteness of the class group for number fields and function fields, and define `class_number` as the order of this group. diff --git a/src/number_theory/class_number/function_field.lean b/src/number_theory/class_number/function_field.lean index b56a75a38d58a..90b7241ccafc3 100644 --- a/src/number_theory/class_number/function_field.lean +++ b/src/number_theory/class_number/function_field.lean @@ -10,6 +10,9 @@ import number_theory.function_field /-! # Class numbers of function fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the class number of a function field as the (finite) cardinality of the class group of its ring of integers. It also proves some elementary results on the class number. diff --git a/src/number_theory/cyclotomic/gal.lean b/src/number_theory/cyclotomic/gal.lean index ee16e36e0619c..168f3db2ae45e 100644 --- a/src/number_theory/cyclotomic/gal.lean +++ b/src/number_theory/cyclotomic/gal.lean @@ -10,6 +10,9 @@ import field_theory.polynomial_galois_group /-! # Galois group of cyclotomic extensions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we show the relationship between the Galois group of `K(ζₙ)` and `(zmod n)ˣ`; it is always a subgroup, and if the `n`th cyclotomic polynomial is irreducible, they are isomorphic. diff --git a/src/number_theory/cyclotomic/rat.lean b/src/number_theory/cyclotomic/rat.lean index 6481a65641071..f285b2f60cf6d 100644 --- a/src/number_theory/cyclotomic/rat.lean +++ b/src/number_theory/cyclotomic/rat.lean @@ -9,6 +9,9 @@ import ring_theory.polynomial.eisenstein.is_integral /-! # Ring of integers of `p ^ n`-th cyclotomic fields + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. We gather results about cyclotomic extensions of `ℚ`. In particular, we compute the ring of integers of a `p ^ n`-th cyclotomic extension of `ℚ`. diff --git a/src/number_theory/number_field/class_number.lean b/src/number_theory/number_field/class_number.lean index 9b1bb64056c76..4958f37408dfe 100644 --- a/src/number_theory/number_field/class_number.lean +++ b/src/number_theory/number_field/class_number.lean @@ -10,6 +10,9 @@ import number_theory.number_field.basic /-! # Class numbers of number fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the class number of a number field as the (finite) cardinality of the class group of its ring of integers. It also proves some elementary results on the class number. diff --git a/src/representation_theory/group_cohomology/resolution.lean b/src/representation_theory/group_cohomology/resolution.lean index 434f70e9d0ab5..c31a3397b8fc2 100644 --- a/src/representation_theory/group_cohomology/resolution.lean +++ b/src/representation_theory/group_cohomology/resolution.lean @@ -12,6 +12,9 @@ import representation_theory.Rep /-! # The structure of the `k[G]`-module `k[Gⁿ]` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains facts about an important `k[G]`-module structure on `k[Gⁿ]`, where `k` is a commutative ring and `G` is a group. The module structure arises from the representation `G →* End(k[Gⁿ])` induced by the diagonal action of `G` on `Gⁿ.` diff --git a/src/topology/metric_space/dilation.lean b/src/topology/metric_space/dilation.lean index 24195f12cdfcb..d9b8ecdeb9dc6 100644 --- a/src/topology/metric_space/dilation.lean +++ b/src/topology/metric_space/dilation.lean @@ -10,6 +10,9 @@ import data.fun_like.basic /-! # Dilations +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define dilations, i.e., maps between emetric spaces that satisfy `edist (f x) (f y) = r * edist x y` for some `r ∉ {0, ∞}`. From 3ff3f2d6a3118b8711063de7111a0d77a53219a8 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Mon, 26 Jun 2023 11:35:20 +0000 Subject: [PATCH 08/16] feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card (#19198) Prove some lemmas that allow to handle part_enat.card of finite cardinals, analogous to those about nat.card Co-authored-by: Antoine Chambert-Loir --- src/data/finite/card.lean | 12 ++++ src/data/nat/part_enat.lean | 6 ++ src/set_theory/cardinal/basic.lean | 81 +++++++++++++++++++++++++- src/set_theory/cardinal/finite.lean | 88 +++++++++++++++++++++++++++++ 4 files changed, 186 insertions(+), 1 deletion(-) diff --git a/src/data/finite/card.lean b/src/data/finite/card.lean index 4191dc9366418..bda3efd6479ac 100644 --- a/src/data/finite/card.lean +++ b/src/data/finite/card.lean @@ -158,6 +158,18 @@ by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_lt hx } end finite +namespace part_enat + +lemma card_eq_coe_nat_card (α : Type*) [finite α] : card α = nat.card α := +begin + unfold part_enat.card, + apply symm, + rw cardinal.coe_nat_eq_to_part_enat_iff, + exact finite.cast_card_eq_mk , +end + +end part_enat + namespace set lemma card_union_le (s t : set α) : nat.card ↥(s ∪ t) ≤ nat.card s + nat.card t := diff --git a/src/data/nat/part_enat.lean b/src/data/nat/part_enat.lean index 7f03e53a943cf..599f44cb6f70e 100644 --- a/src/data/nat/part_enat.lean +++ b/src/data/nat/part_enat.lean @@ -380,6 +380,9 @@ begin apply_mod_cast nat.lt_of_succ_le, apply_mod_cast h end +lemma coe_succ_le_iff {n : ℕ} {e : part_enat} : ↑n.succ ≤ e ↔ ↑n < e:= +by rw [nat.succ_eq_add_one n, nat.cast_add, nat.cast_one, add_one_le_iff_lt (coe_ne_top n)] + lemma lt_add_one_iff_lt {x y : part_enat} (hx : x ≠ ⊤) : x < y + 1 ↔ x ≤ y := begin split, exact le_of_lt_add_one, @@ -388,6 +391,9 @@ begin apply_mod_cast nat.lt_succ_of_le, apply_mod_cast h end +lemma lt_coe_succ_iff_le {x : part_enat} {n : ℕ} (hx : x ≠ ⊤) : x < n.succ ↔ x ≤ n := +by rw [nat.succ_eq_add_one n, nat.cast_add, nat.cast_one, lt_add_one_iff_lt hx] + lemma add_eq_top_iff {a b : part_enat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := by apply part_enat.cases_on a; apply part_enat.cases_on b; simp; simp only [(nat.cast_add _ _).symm, part_enat.coe_ne_top]; simp diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index d3d08052171f7..c04b208884d0f 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -1215,6 +1215,10 @@ by rw [to_nat_apply_of_lt_aleph_0 h, ← classical.some_spec (lt_aleph_0.1 h)] lemma cast_to_nat_of_aleph_0_le {c : cardinal} (h : ℵ₀ ≤ c) : ↑c.to_nat = (0 : cardinal) := by rw [to_nat_apply_of_aleph_0_le h, nat.cast_zero] +lemma to_nat_eq_iff_eq_of_lt_aleph_0 {c d : cardinal} (hc : c < ℵ₀) (hd : d < ℵ₀) : + c.to_nat = d.to_nat ↔ c = d := +by rw [←nat_cast_inj, cast_to_nat_of_lt_aleph_0 hc, cast_to_nat_of_lt_aleph_0 hd] + lemma to_nat_le_iff_le_of_lt_aleph_0 {c d : cardinal} (hc : c < ℵ₀) (hd : d < ℵ₀) : c.to_nat ≤ d.to_nat ↔ c ≤ d := by rw [←nat_cast_le, cast_to_nat_of_lt_aleph_0 hc, cast_to_nat_of_lt_aleph_0 hd] @@ -1357,10 +1361,84 @@ to_part_enat_apply_of_aleph_0_le (infinite_iff.1 h) @[simp] theorem aleph_0_to_part_enat : to_part_enat ℵ₀ = ⊤ := to_part_enat_apply_of_aleph_0_le le_rfl +lemma to_part_enat_eq_top_iff_le_aleph_0 {c : cardinal} : + to_part_enat c = ⊤ ↔ aleph_0 ≤ c := +begin + cases lt_or_ge c aleph_0 with hc hc, + simp only [to_part_enat_apply_of_lt_aleph_0 hc, part_enat.coe_ne_top, false_iff, not_le, hc], + simp only [to_part_enat_apply_of_aleph_0_le hc, eq_self_iff_true, true_iff], + exact hc, +end + +lemma to_part_enat_le_iff_le_of_le_aleph_0 {c c' : cardinal} (h : c ≤ aleph_0) : + to_part_enat c ≤ to_part_enat c' ↔ c ≤ c' := +begin + cases lt_or_ge c aleph_0 with hc hc, + rw to_part_enat_apply_of_lt_aleph_0 hc, + cases lt_or_ge c' aleph_0 with hc' hc', + { rw to_part_enat_apply_of_lt_aleph_0 hc', + rw part_enat.coe_le_coe, + exact to_nat_le_iff_le_of_lt_aleph_0 hc hc', }, + { simp only [to_part_enat_apply_of_aleph_0_le hc', + le_top, true_iff], + exact le_trans h hc', }, + { rw to_part_enat_apply_of_aleph_0_le hc, + simp only [top_le_iff, to_part_enat_eq_top_iff_le_aleph_0, + le_antisymm h hc], }, +end + +lemma to_part_enat_le_iff_le_of_lt_aleph_0 {c c' : cardinal} (hc' : c' < aleph_0) : + to_part_enat c ≤ to_part_enat c' ↔ c ≤ c' := +begin + cases lt_or_ge c aleph_0 with hc hc, + { rw to_part_enat_apply_of_lt_aleph_0 hc, + rw to_part_enat_apply_of_lt_aleph_0 hc', + rw part_enat.coe_le_coe, + exact to_nat_le_iff_le_of_lt_aleph_0 hc hc', }, + { rw to_part_enat_apply_of_aleph_0_le hc, + simp only [top_le_iff, to_part_enat_eq_top_iff_le_aleph_0], + rw [← not_iff_not, not_le, not_le], + simp only [hc', lt_of_lt_of_le hc' hc], }, +end + +lemma to_part_enat_eq_iff_eq_of_le_aleph_0 {c c' : cardinal} + (hc : c ≤ aleph_0) (hc' : c' ≤ aleph_0) : + to_part_enat c = to_part_enat c' ↔ c = c' := by +rw [le_antisymm_iff, le_antisymm_iff, + to_part_enat_le_iff_le_of_le_aleph_0 hc, to_part_enat_le_iff_le_of_le_aleph_0 hc'] + +lemma to_part_enat_mono {c c' : cardinal} (h : c ≤ c') : + to_part_enat c ≤ to_part_enat c' := +begin + cases lt_or_ge c aleph_0 with hc hc, + rw to_part_enat_apply_of_lt_aleph_0 hc, + cases lt_or_ge c' aleph_0 with hc' hc', + rw to_part_enat_apply_of_lt_aleph_0 hc', + simp only [part_enat.coe_le_coe], + exact to_nat_le_of_le_of_lt_aleph_0 hc' h, + rw to_part_enat_apply_of_aleph_0_le hc', + exact le_top, + rw [to_part_enat_apply_of_aleph_0_le hc, + to_part_enat_apply_of_aleph_0_le (le_trans hc h)], +end + lemma to_part_enat_surjective : surjective to_part_enat := λ x, part_enat.cases_on x ⟨ℵ₀, to_part_enat_apply_of_aleph_0_le le_rfl⟩ $ λ n, ⟨n, to_part_enat_cast n⟩ +lemma to_part_enat_lift (c : cardinal.{v}) : (lift.{u v} c).to_part_enat = c.to_part_enat := +begin + cases lt_or_ge c ℵ₀ with hc hc, + { rw [to_part_enat_apply_of_lt_aleph_0 hc, cardinal.to_part_enat_apply_of_lt_aleph_0 _], + simp only [to_nat_lift], + rw [← lift_aleph_0, lift_lt], exact hc }, + { rw [to_part_enat_apply_of_aleph_0_le hc, cardinal.to_part_enat_apply_of_aleph_0_le _], + rw [← lift_aleph_0, lift_le], exact hc } +end + +lemma to_part_enat_congr {β : Type v} (e : α ≃ β) : (#α).to_part_enat = (#β).to_part_enat := +by rw [←to_part_enat_lift, lift_mk_eq.mpr ⟨e⟩, to_part_enat_lift] + lemma mk_to_part_enat_eq_coe_card [fintype α] : (#α).to_part_enat = fintype.card α := by simp @@ -1369,7 +1447,8 @@ lemma mk_int : #ℤ = ℵ₀ := mk_denumerable ℤ lemma mk_pnat : #ℕ+ = ℵ₀ := mk_denumerable ℕ+ /-- **König's theorem** -/ -theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g := +theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : +sum f < prod g := lt_of_not_ge $ λ ⟨F⟩, begin haveI : inhabited (Π (i : ι), (g i).out), { refine ⟨λ i, classical.choice $ mk_ne_zero_iff.1 _⟩, diff --git a/src/set_theory/cardinal/finite.lean b/src/set_theory/cardinal/finite.lean index 5495b095f9091..9e98d2bb67b27 100644 --- a/src/set_theory/cardinal/finite.lean +++ b/src/set_theory/cardinal/finite.lean @@ -120,4 +120,92 @@ lemma card_eq_coe_fintype_card [fintype α] : card α = fintype.card α := mk_to @[simp] lemma card_eq_top_of_infinite [infinite α] : card α = ⊤ := mk_to_part_enat_of_infinite +lemma card_congr {α : Type*} {β : Type*} (f : α ≃ β) : + part_enat.card α = part_enat.card β := +cardinal.to_part_enat_congr f + +lemma card_ulift (α : Type*) : card (ulift α) = card α := +card_congr equiv.ulift + +@[simp] lemma card_plift (α : Type*) : card (plift α) = card α := +card_congr equiv.plift + +lemma card_image_of_inj_on {α : Type*} {β : Type*} {f : α → β} {s : set α} (h : set.inj_on f s) : + card (f '' s) = card s := +card_congr (equiv.set.image_of_inj_on f s h).symm + +lemma card_image_of_injective {α : Type*} {β : Type*} + (f : α → β) (s : set α) (h : function.injective f) : + card (f '' s) = card s := +card_image_of_inj_on (set.inj_on_of_injective h s) + +-- Should I keep the 6 following lemmas ? +@[simp] +lemma _root_.cardinal.coe_nat_le_to_part_enat_iff {n : ℕ} {c : cardinal} : + ↑n ≤ to_part_enat c ↔ ↑n ≤ c := +by rw [← to_part_enat_cast n, to_part_enat_le_iff_le_of_le_aleph_0 (le_of_lt (nat_lt_aleph_0 n))] + +@[simp] +lemma _root_.cardinal.to_part_enat_le_coe_nat_iff {c : cardinal} {n : ℕ} : + to_part_enat c ≤ n ↔ c ≤ n := +by rw [← to_part_enat_cast n, + to_part_enat_le_iff_le_of_lt_aleph_0 (nat_lt_aleph_0 n)] + +@[simp] +lemma _root_.cardinal.coe_nat_eq_to_part_enat_iff {n : ℕ} {c : cardinal} : + ↑n = to_part_enat c ↔ ↑n = c := +by rw [le_antisymm_iff, le_antisymm_iff, + cardinal.coe_nat_le_to_part_enat_iff, cardinal.to_part_enat_le_coe_nat_iff] + +@[simp] +lemma _root_.cardinal.to_part_enat_eq_coe_nat_iff {c : cardinal} {n : ℕ} : + to_part_enat c = n ↔ c = n:= +by rw [eq_comm, cardinal.coe_nat_eq_to_part_enat_iff, eq_comm] + +@[simp] +lemma _root_.cardinal.coe_nat_lt_coe_iff_lt {n : ℕ} {c : cardinal} : + ↑n < to_part_enat c ↔ ↑n < c := +by simp only [← not_le, cardinal.to_part_enat_le_coe_nat_iff] + +@[simp] +lemma _root_.cardinal.lt_coe_nat_iff_lt {n : ℕ} {c : cardinal} : + to_part_enat c < n ↔ c < n := +by simp only [← not_le, cardinal.coe_nat_le_to_part_enat_iff] + +lemma card_eq_zero_iff_empty (α : Type*) : card α = 0 ↔ is_empty α := +begin + rw ← cardinal.mk_eq_zero_iff, + conv_rhs { rw ← nat.cast_zero }, + rw ← cardinal.to_part_enat_eq_coe_nat_iff, + simp only [part_enat.card, nat.cast_zero] +end + +lemma card_le_one_iff_subsingleton (α : Type*) : card α ≤ 1 ↔ subsingleton α := +begin + rw ← le_one_iff_subsingleton, + conv_rhs { rw ← nat.cast_one}, + rw ← cardinal.to_part_enat_le_coe_nat_iff, + simp only [part_enat.card, nat.cast_one] +end + +lemma one_lt_card_iff_nontrivial (α : Type*) : 1 < card α ↔ nontrivial α := +begin + rw ← one_lt_iff_nontrivial, + conv_rhs { rw ← nat.cast_one}, + rw ← cardinal.coe_nat_lt_coe_iff_lt, + simp only [part_enat.card, nat.cast_one] +end + +lemma is_finite_of_card {α : Type*} {n : ℕ} (hα : part_enat.card α = n) : + finite α := +begin + apply or.resolve_right (finite_or_infinite α), + intro h, resetI, + apply part_enat.coe_ne_top n, + rw ← hα, + exact part_enat.card_eq_top_of_infinite, +end + + + end part_enat From 8b981918a93bc45a8600de608cde7944a80d92b9 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Mon, 26 Jun 2023 15:07:59 +0000 Subject: [PATCH 09/16] feat(analysis/inner_product_space): the adjoint for unbounded operators (#18820) --- docs/overview.yaml | 1 + .../inner_product_space/linear_pmap.lean | 212 ++++++++++++++++++ src/linear_algebra/linear_pmap.lean | 2 + 3 files changed, 215 insertions(+) create mode 100644 src/analysis/inner_product_space/linear_pmap.lean diff --git a/docs/overview.yaml b/docs/overview.yaml index d1653f00c6261..ecc7271289e99 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -274,6 +274,7 @@ Analysis: Hilbert spaces: Inner product space, over $R$ or $C$: 'inner_product_space' Cauchy-Schwarz inequality: 'inner_mul_inner_self_le' + adjoint operator: 'linear_pmap.adjoint' self-adjoint operator: 'is_self_adjoint' orthogonal projection: 'orthogonal_projection' reflection: 'reflection' diff --git a/src/analysis/inner_product_space/linear_pmap.lean b/src/analysis/inner_product_space/linear_pmap.lean new file mode 100644 index 0000000000000..8d36210252e4c --- /dev/null +++ b/src/analysis/inner_product_space/linear_pmap.lean @@ -0,0 +1,212 @@ +/- +Copyright (c) 2022 Moritz Doll. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Moritz Doll +-/ + +import analysis.inner_product_space.adjoint +import topology.algebra.module.linear_pmap +import topology.algebra.module.basic + +/-! + +# Partially defined linear operators on Hilbert spaces + +We will develop the basics of the theory of unbounded operators on Hilbert spaces. + +## Main definitions + +* `linear_pmap.is_formal_adjoint`: An operator `T` is a formal adjoint of `S` if for all `x` in the + domain of `T` and `y` in the domain of `S`, we have that `⟪T x, y⟫ = ⟪x, S y⟫`. +* `linear_pmap.adjoint`: The adjoint of a map `E →ₗ.[𝕜] F` as a map `F →ₗ.[𝕜] E`. + +## Main statements + +* `linear_pmap.adjoint_is_formal_adjoint`: The adjoint is a formal adjoint +* `linear_pmap.is_formal_adjoint.le_adjoint`: Every formal adjoint is contained in the adjoint +* `continuous_linear_map.to_pmap_adjoint_eq_adjoint_to_pmap_of_dense`: The adjoint on + `continuous_linear_map` and `linear_pmap` coincide. + +## Notation + +* For `T : E →ₗ.[𝕜] F` the adjoint can be written as `T†`. + This notation is localized in `linear_pmap`. + +## Implementation notes + +We use the junk value pattern to define the adjoint for all `linear_pmap`s. In the case that +`T : E →ₗ.[𝕜] F` is not densely defined the adjoint `T†` is the zero map from `T.adjoint_domain` to +`E`. + +## References + +* [J. Weidmann, *Linear Operators in Hilbert Spaces*][weidmann_linear] + +## Tags + +Unbounded operators, closed operators +-/ + + +noncomputable theory + +open is_R_or_C +open_locale complex_conjugate classical + +variables {𝕜 E F G : Type*} [is_R_or_C 𝕜] +variables [normed_add_comm_group E] [inner_product_space 𝕜 E] +variables [normed_add_comm_group F] [inner_product_space 𝕜 F] + +local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y + +namespace linear_pmap + +/-- An operator `T` is a formal adjoint of `S` if for all `x` in the domain of `T` and `y` in the +domain of `S`, we have that `⟪T x, y⟫ = ⟪x, S y⟫`. -/ +def is_formal_adjoint (T : E →ₗ.[𝕜] F) (S : F →ₗ.[𝕜] E) : Prop := +∀ (x : T.domain) (y : S.domain), ⟪T x, y⟫ = ⟪(x : E), S y⟫ + +variables {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} + +@[protected] lemma is_formal_adjoint.symm (h : T.is_formal_adjoint S) : S.is_formal_adjoint T := +λ y _, by rw [←inner_conj_symm, ←inner_conj_symm (y : F), h] + +variables (T) + +/-- The domain of the adjoint operator. + +This definition is needed to construct the adjoint operator and the preferred version to use is +`T.adjoint.domain` instead of `T.adjoint_domain`. -/ +def adjoint_domain : submodule 𝕜 F := +{ carrier := {y | continuous ((innerₛₗ 𝕜 y).comp T.to_fun)}, + zero_mem' := by { rw [set.mem_set_of_eq, linear_map.map_zero, linear_map.zero_comp], + exact continuous_zero }, + add_mem' := λ x y hx hy, by { rw [set.mem_set_of_eq, linear_map.map_add] at *, exact hx.add hy }, + smul_mem' := λ a x hx, by { rw [set.mem_set_of_eq, linear_map.map_smulₛₗ] at *, + exact hx.const_smul (conj a) } } + +/-- The operator `λ x, ⟪y, T x⟫` considered as a continuous linear operator from `T.adjoint_domain` +to `𝕜`. -/ +def adjoint_domain_mk_clm (y : T.adjoint_domain) : T.domain →L[𝕜] 𝕜 := +⟨(innerₛₗ 𝕜 (y : F)).comp T.to_fun, y.prop⟩ + +lemma adjoint_domain_mk_clm_apply (y : T.adjoint_domain) (x : T.domain) : + adjoint_domain_mk_clm T y x = ⟪(y : F), T x⟫ := rfl + +variable {T} +variable (hT : dense (T.domain : set E)) + +include hT + +/-- The unique continuous extension of the operator `adjoint_domain_mk_clm` to `E`. -/ +def adjoint_domain_mk_clm_extend (y : T.adjoint_domain) : + E →L[𝕜] 𝕜 := +(T.adjoint_domain_mk_clm y).extend (submodule.subtypeL T.domain) + hT.dense_range_coe uniform_embedding_subtype_coe.to_uniform_inducing + +@[simp] lemma adjoint_domain_mk_clm_extend_apply (y : T.adjoint_domain) (x : T.domain) : + adjoint_domain_mk_clm_extend hT y (x : E) = ⟪(y : F), T x⟫ := +continuous_linear_map.extend_eq _ _ _ _ _ + +variables [complete_space E] + +/-- The adjoint as a linear map from its domain to `E`. + +This is an auxiliary definition needed to define the adjoint operator as a `linear_pmap` without +the assumption that `T.domain` is dense. -/ +def adjoint_aux : T.adjoint_domain →ₗ[𝕜] E := +{ to_fun := λ y, (inner_product_space.to_dual 𝕜 E).symm (adjoint_domain_mk_clm_extend hT y), + map_add' := λ x y, hT.eq_of_inner_left $ λ _, + by simp only [inner_add_left, submodule.coe_add, inner_product_space.to_dual_symm_apply, + adjoint_domain_mk_clm_extend_apply], + map_smul' := λ _ _, hT.eq_of_inner_left $ λ _, + by simp only [inner_smul_left, submodule.coe_smul_of_tower, ring_hom.id_apply, + inner_product_space.to_dual_symm_apply, adjoint_domain_mk_clm_extend_apply] } + +lemma adjoint_aux_inner (y : T.adjoint_domain) (x : T.domain) : + ⟪adjoint_aux hT y, x⟫ = ⟪(y : F), T x⟫ := +by simp only [adjoint_aux, linear_map.coe_mk, inner_product_space.to_dual_symm_apply, + adjoint_domain_mk_clm_extend_apply] + +lemma adjoint_aux_unique (y : T.adjoint_domain) {x₀ : E} + (hx₀ : ∀ x : T.domain, ⟪x₀, x⟫ = ⟪(y : F), T x⟫) : adjoint_aux hT y = x₀ := +hT.eq_of_inner_left (λ v, (adjoint_aux_inner hT _ _).trans (hx₀ v).symm) + +omit hT + +variable (T) + +/-- The adjoint operator as a partially defined linear operator. -/ +def adjoint : F →ₗ.[𝕜] E := +{ domain := T.adjoint_domain, + to_fun := if hT : dense (T.domain : set E) then adjoint_aux hT else 0 } + +localized "postfix (name := adjoint) `†`:1100 := linear_pmap.adjoint" in linear_pmap + +lemma mem_adjoint_domain_iff (y : F) : + y ∈ T†.domain ↔ continuous ((innerₛₗ 𝕜 y).comp T.to_fun) := iff.rfl + +variable {T} + +lemma mem_adjoint_domain_of_exists (y : F) (h : ∃ w : E, ∀ (x : T.domain), ⟪w, x⟫ = ⟪y, T x⟫) : + y ∈ T†.domain := +begin + cases h with w hw, + rw T.mem_adjoint_domain_iff, + have : continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by continuity, + convert this using 1, + exact funext (λ x, (hw x).symm), +end + +lemma adjoint_apply_of_not_dense (hT : ¬ dense (T.domain : set E)) (y : T†.domain) : T† y = 0 := +begin + change (if hT : dense (T.domain : set E) then adjoint_aux hT else 0) y = _, + simp only [hT, not_false_iff, dif_neg, linear_map.zero_apply], +end + +include hT + +lemma adjoint_apply_of_dense (y : T†.domain) : T† y = adjoint_aux hT y := +begin + change (if hT : dense (T.domain : set E) then adjoint_aux hT else 0) y = _, + simp only [hT, dif_pos, linear_map.coe_mk], +end + +lemma adjoint_apply_eq (y : T†.domain) {x₀ : E} + (hx₀ : ∀ x : T.domain, ⟪x₀, x⟫ = ⟪(y : F), T x⟫) : T† y = x₀ := +(adjoint_apply_of_dense hT y).symm ▸ adjoint_aux_unique hT _ hx₀ + +/-- The fundamental property of the adjoint. -/ +lemma adjoint_is_formal_adjoint : T†.is_formal_adjoint T := +λ x, (adjoint_apply_of_dense hT x).symm ▸ adjoint_aux_inner hT x + +/-- The adjoint is maximal in the sense that it contains every formal adjoint. -/ +lemma is_formal_adjoint.le_adjoint (h : T.is_formal_adjoint S) : S ≤ T† := +-- Trivially, every `x : S.domain` is in `T.adjoint.domain` +⟨λ x hx, mem_adjoint_domain_of_exists _ ⟨S ⟨x, hx⟩, h.symm ⟨x, hx⟩⟩, + -- Equality on `S.domain` follows from equality + -- `⟪v, S x⟫ = ⟪v, T.adjoint y⟫` for all `v : T.domain`: + λ _ _ hxy, (adjoint_apply_eq hT _ (λ _, by rw [h.symm, hxy])).symm⟩ + +end linear_pmap + +namespace continuous_linear_map + +variables [complete_space E] [complete_space F] +variables (A : E →L[𝕜] F) {p : submodule 𝕜 E} + +/-- Restricting `A` to a dense submodule and taking the `linear_pmap.adjoint` is the same +as taking the `continuous_linear_map.adjoint` interpreted as a `linear_pmap`. -/ +lemma to_pmap_adjoint_eq_adjoint_to_pmap_of_dense (hp : dense (p : set E)) : + (A.to_pmap p).adjoint = A.adjoint.to_pmap ⊤ := +begin + ext, + { simp only [to_linear_map_eq_coe, linear_map.to_pmap_domain, submodule.mem_top, iff_true, + linear_pmap.mem_adjoint_domain_iff, linear_map.coe_comp, innerₛₗ_apply_coe], + exact ((innerSL 𝕜 x).comp $ A.comp $ submodule.subtypeL _).cont }, + intros x y hxy, + refine linear_pmap.adjoint_apply_eq hp _ (λ v, _), + simp only [adjoint_inner_left, hxy, linear_map.to_pmap_apply, to_linear_map_eq_coe, coe_coe], +end + +end continuous_linear_map diff --git a/src/linear_algebra/linear_pmap.lean b/src/linear_algebra/linear_pmap.lean index 17569ffbfd37a..a20d1d6a41afb 100644 --- a/src/linear_algebra/linear_pmap.lean +++ b/src/linear_algebra/linear_pmap.lean @@ -470,6 +470,8 @@ def to_pmap (f : E →ₗ[R] F) (p : submodule R E) : E →ₗ.[R] F := @[simp] lemma to_pmap_apply (f : E →ₗ[R] F) (p : submodule R E) (x : p) : f.to_pmap p x = f x := rfl +@[simp] lemma to_pmap_domain (f : E →ₗ[R] F) (p : submodule R E) : (f.to_pmap p).domain = p := rfl + /-- Compose a linear map with a `linear_pmap` -/ def comp_pmap (g : F →ₗ[R] G) (f : E →ₗ.[R] F) : E →ₗ.[R] G := { domain := f.domain, From 15db1b4f26ba89c6eb0c78b0a44c7e779a788e29 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 27 Jun 2023 04:28:35 +0000 Subject: [PATCH 10/16] chore(category_theory/limits/construction/over): rename default to basic (#19217) This was a default file with content, so needs renaming. Afterwards it can just be ported as usual. Co-authored-by: Scott Morrison --- .../limits/constructions/over/{default.lean => basic.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/category_theory/limits/constructions/over/{default.lean => basic.lean} (100%) diff --git a/src/category_theory/limits/constructions/over/default.lean b/src/category_theory/limits/constructions/over/basic.lean similarity index 100% rename from src/category_theory/limits/constructions/over/default.lean rename to src/category_theory/limits/constructions/over/basic.lean From 08b63ab58a6ec1157ebeafcbbe6c7a3fb3c9f6d5 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Wed, 28 Jun 2023 06:08:04 +0000 Subject: [PATCH 11/16] chore(*): add mathlib4 synchronization comments (#19216) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Mon.colimits` * `algebra.category.fgModule.basic` * `analysis.complex.upper_half_plane.basic` * `analysis.inner_product_space.linear_pmap` * `analysis.special_functions.gamma.beta` * `analysis.special_functions.gamma.bohr_mollerup` * `analysis.special_functions.gaussian` * `category_theory.closed.ideal` * `category_theory.monoidal.Bimod` * `combinatorics.simple_graph.regularity.bound` * `combinatorics.simple_graph.regularity.chunk` * `combinatorics.simple_graph.regularity.increment` * `combinatorics.simple_graph.regularity.lemma` * `control.random` * `geometry.manifold.complex` * `geometry.manifold.mfderiv` * `geometry.manifold.partition_of_unity` * `linear_algebra.exterior_algebra.of_alternating` * `logic.equiv.array` * `number_theory.bertrand` * `number_theory.legendre_symbol.gauss_eisenstein_lemmas` * `number_theory.legendre_symbol.gauss_sum` * `number_theory.legendre_symbol.jacobi_symbol` * `number_theory.legendre_symbol.quadratic_char.gauss_sum` * `number_theory.legendre_symbol.quadratic_reciprocity` * `number_theory.sum_two_squares` * `number_theory.zsqrtd.quadratic_reciprocity` * `ring_theory.dedekind_domain.selmer_group` * `ring_theory.witt_vector.frobenius` * `ring_theory.witt_vector.identities` * `ring_theory.witt_vector.init_tail` * `ring_theory.witt_vector.verschiebung` * `set_theory.game.basic` * `set_theory.game.impartial` * `set_theory.game.ordinal` * `set_theory.surreal.basic` * `testing.slim_check.gen` * `testing.slim_check.sampleable` * `testing.slim_check.testable` --- src/algebra/category/Mon/colimits.lean | 3 +++ src/algebra/category/fgModule/basic.lean | 3 +++ src/analysis/special_functions/gamma/bohr_mollerup.lean | 3 +++ src/analysis/special_functions/gaussian.lean | 3 +++ src/category_theory/monoidal/Bimod.lean | 3 +++ src/combinatorics/simple_graph/regularity/bound.lean | 3 +++ src/combinatorics/simple_graph/regularity/chunk.lean | 3 +++ src/combinatorics/simple_graph/regularity/increment.lean | 3 +++ src/combinatorics/simple_graph/regularity/lemma.lean | 3 +++ src/geometry/manifold/mfderiv.lean | 3 +++ src/linear_algebra/exterior_algebra/of_alternating.lean | 3 +++ src/number_theory/bertrand.lean | 3 +++ src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean | 3 +++ src/number_theory/legendre_symbol/gauss_sum.lean | 3 +++ .../legendre_symbol/quadratic_char/gauss_sum.lean | 3 +++ src/number_theory/legendre_symbol/quadratic_reciprocity.lean | 3 +++ src/number_theory/sum_two_squares.lean | 3 +++ src/number_theory/zsqrtd/quadratic_reciprocity.lean | 3 +++ src/ring_theory/dedekind_domain/selmer_group.lean | 3 +++ src/set_theory/game/basic.lean | 3 +++ src/set_theory/game/ordinal.lean | 3 +++ 21 files changed, 63 insertions(+) diff --git a/src/algebra/category/Mon/colimits.lean b/src/algebra/category/Mon/colimits.lean index 9f12277c95cb3..b1bbcb32c2f8d 100644 --- a/src/algebra/category/Mon/colimits.lean +++ b/src/algebra/category/Mon/colimits.lean @@ -10,6 +10,9 @@ import category_theory.concrete_category.elementwise /-! # The category of monoids has all colimits. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We do this construction knowing nothing about monoids. In particular, I want to claim that this file could be produced by a python script that just looks at the output of `#print monoid`: diff --git a/src/algebra/category/fgModule/basic.lean b/src/algebra/category/fgModule/basic.lean index f70d4ec8e3ecb..118a4688f6a66 100644 --- a/src/algebra/category/fgModule/basic.lean +++ b/src/algebra/category/fgModule/basic.lean @@ -12,6 +12,9 @@ import algebra.category.Module.monoidal.closed /-! # The category of finitely generated modules over a ring +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This introduces `fgModule R`, the category of finitely generated modules over a ring `R`. It is implemented as a full subcategory on a subtype of `Module R`. diff --git a/src/analysis/special_functions/gamma/bohr_mollerup.lean b/src/analysis/special_functions/gamma/bohr_mollerup.lean index 9db12f986223c..3a6b66bd0659d 100644 --- a/src/analysis/special_functions/gamma/bohr_mollerup.lean +++ b/src/analysis/special_functions/gamma/bohr_mollerup.lean @@ -8,6 +8,9 @@ import analysis.special_functions.gaussian /-! # Convexity properties of the Gamma function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we prove that `Gamma` and `log ∘ Gamma` are convex functions on the positive real line. We then prove the Bohr-Mollerup theorem, which characterises `Gamma` as the *unique* positive-real-valued, log-convex function on the positive reals satisfying `f (x + 1) = x f x` and diff --git a/src/analysis/special_functions/gaussian.lean b/src/analysis/special_functions/gaussian.lean index b21f166f048e6..7705bdc538282 100644 --- a/src/analysis/special_functions/gaussian.lean +++ b/src/analysis/special_functions/gaussian.lean @@ -13,6 +13,9 @@ import analysis.fourier.poisson_summation /-! # Gaussian integral +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We prove various versions of the formula for the Gaussian integral: * `integral_gaussian`: for real `b` we have `∫ x:ℝ, exp (-b * x^2) = sqrt (π / b)`. * `integral_gaussian_complex`: for complex `b` with `0 < re b` we have diff --git a/src/category_theory/monoidal/Bimod.lean b/src/category_theory/monoidal/Bimod.lean index 7ff041dcfd99e..48b955f7b99b4 100644 --- a/src/category_theory/monoidal/Bimod.lean +++ b/src/category_theory/monoidal/Bimod.lean @@ -9,6 +9,9 @@ import category_theory.limits.preserves.shapes.equalizers /-! # The category of bimodule objects over a pair of monoid objects. + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. -/ universes v₁ v₂ u₁ u₂ diff --git a/src/combinatorics/simple_graph/regularity/bound.lean b/src/combinatorics/simple_graph/regularity/bound.lean index 2241cf244ebaf..6e2e8992eac1a 100644 --- a/src/combinatorics/simple_graph/regularity/bound.lean +++ b/src/combinatorics/simple_graph/regularity/bound.lean @@ -10,6 +10,9 @@ import order.partition.equipartition /-! # Numerical bounds for Szemerédi Regularity Lemma +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file gathers the numerical facts required by the proof of Szemerédi's regularity lemma. This entire file is internal to the proof of Szemerédi Regularity Lemma. diff --git a/src/combinatorics/simple_graph/regularity/chunk.lean b/src/combinatorics/simple_graph/regularity/chunk.lean index ab766c66b386c..a72af72eec1e4 100644 --- a/src/combinatorics/simple_graph/regularity/chunk.lean +++ b/src/combinatorics/simple_graph/regularity/chunk.lean @@ -10,6 +10,9 @@ import combinatorics.simple_graph.regularity.uniform /-! # Chunk of the increment partition for Szemerédi Regularity Lemma +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In the proof of Szemerédi Regularity Lemma, we need to partition each part of a starting partition to increase the energy. This file defines those partitions of parts and shows that they locally increase the energy. diff --git a/src/combinatorics/simple_graph/regularity/increment.lean b/src/combinatorics/simple_graph/regularity/increment.lean index 8f0c29a8e2a28..b19bae79f86d9 100644 --- a/src/combinatorics/simple_graph/regularity/increment.lean +++ b/src/combinatorics/simple_graph/regularity/increment.lean @@ -9,6 +9,9 @@ import combinatorics.simple_graph.regularity.energy /-! # Increment partition for Szemerédi Regularity Lemma +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In the proof of Szemerédi Regularity Lemma, we need to partition each part of a starting partition to increase the energy. This file defines the partition obtained by gluing the parts partitions together (the *increment partition*) and shows that the energy globally increases. diff --git a/src/combinatorics/simple_graph/regularity/lemma.lean b/src/combinatorics/simple_graph/regularity/lemma.lean index 0b271479520e1..88ae521886eaa 100644 --- a/src/combinatorics/simple_graph/regularity/lemma.lean +++ b/src/combinatorics/simple_graph/regularity/lemma.lean @@ -8,6 +8,9 @@ import combinatorics.simple_graph.regularity.increment /-! # Szemerédi's Regularity Lemma +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we prove Szemerédi's Regularity Lemma (aka SRL). This is a landmark result in combinatorics roughly stating that any sufficiently big graph behaves like a random graph. This is useful because random graphs are well-behaved in many aspects. diff --git a/src/geometry/manifold/mfderiv.lean b/src/geometry/manifold/mfderiv.lean index 67669519a2b97..30c9eb15fbf17 100644 --- a/src/geometry/manifold/mfderiv.lean +++ b/src/geometry/manifold/mfderiv.lean @@ -8,6 +8,9 @@ import geometry.manifold.vector_bundle.tangent /-! # The derivative of functions between smooth manifolds +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Let `M` and `M'` be two smooth manifolds with corners over a field `𝕜` (with respective models with corners `I` on `(E, H)` and `I'` on `(E', H')`), and let `f : M → M'`. We define the derivative of the function at a point, within a set or along the whole space, mimicking the API diff --git a/src/linear_algebra/exterior_algebra/of_alternating.lean b/src/linear_algebra/exterior_algebra/of_alternating.lean index 0aaeb47af7172..ad0ae0b28a5be 100644 --- a/src/linear_algebra/exterior_algebra/of_alternating.lean +++ b/src/linear_algebra/exterior_algebra/of_alternating.lean @@ -10,6 +10,9 @@ import linear_algebra.exterior_algebra.basic /-! # Extending an alternating map to the exterior algebra +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions * `exterior_algebra.lift_alternating`: construct a linear map out of the exterior algebra diff --git a/src/number_theory/bertrand.lean b/src/number_theory/bertrand.lean index 38e6d956438a7..73927a0e9b79c 100644 --- a/src/number_theory/bertrand.lean +++ b/src/number_theory/bertrand.lean @@ -12,6 +12,9 @@ import analysis.convex.specific_functions.deriv /-! # Bertrand's Postulate +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains a proof of Bertrand's postulate: That between any positive number and its double there is a prime. diff --git a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean index 75380ab52d02e..344697e529726 100644 --- a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean +++ b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean @@ -8,6 +8,9 @@ import number_theory.legendre_symbol.quadratic_reciprocity /-! # Lemmas of Gauss and Eisenstein +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains the Lemmas of Gauss and Eisenstein on the Legendre symbol. The main results are `zmod.gauss_lemma` and `zmod.eisenstein_lemma`. -/ diff --git a/src/number_theory/legendre_symbol/gauss_sum.lean b/src/number_theory/legendre_symbol/gauss_sum.lean index 43f375c18d498..d3eec3b506a90 100644 --- a/src/number_theory/legendre_symbol/gauss_sum.lean +++ b/src/number_theory/legendre_symbol/gauss_sum.lean @@ -10,6 +10,9 @@ import algebra.char_p.char_and_card /-! # Gauss sums +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the Gauss sum associated to a multiplicative and an additive character of a finite field and prove some results about them. diff --git a/src/number_theory/legendre_symbol/quadratic_char/gauss_sum.lean b/src/number_theory/legendre_symbol/quadratic_char/gauss_sum.lean index 6e220b86a5d81..ef6cb184b7bcd 100644 --- a/src/number_theory/legendre_symbol/quadratic_char/gauss_sum.lean +++ b/src/number_theory/legendre_symbol/quadratic_char/gauss_sum.lean @@ -9,6 +9,9 @@ import number_theory.legendre_symbol.gauss_sum /-! # Quadratic characters of finite fields +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Further facts relying on Gauss sums. -/ diff --git a/src/number_theory/legendre_symbol/quadratic_reciprocity.lean b/src/number_theory/legendre_symbol/quadratic_reciprocity.lean index 53cfb747b8efe..c8b13ea94189e 100644 --- a/src/number_theory/legendre_symbol/quadratic_reciprocity.lean +++ b/src/number_theory/legendre_symbol/quadratic_reciprocity.lean @@ -9,6 +9,9 @@ import number_theory.legendre_symbol.quadratic_char.gauss_sum /-! # Quadratic reciprocity. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main results We prove the law of quadratic reciprocity, see `legendre_sym.quadratic_reciprocity` and diff --git a/src/number_theory/sum_two_squares.lean b/src/number_theory/sum_two_squares.lean index fe7bbf6eae2f2..863876134230f 100644 --- a/src/number_theory/sum_two_squares.lean +++ b/src/number_theory/sum_two_squares.lean @@ -10,6 +10,9 @@ import tactic.linear_combination /-! # Sums of two squares +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Fermat's theorem on the sum of two squares. Every prime `p` congruent to 1 mod 4 is the sum of two squares; see `nat.prime.sq_add_sq` (which has the weaker assumption `p % 4 ≠ 3`). diff --git a/src/number_theory/zsqrtd/quadratic_reciprocity.lean b/src/number_theory/zsqrtd/quadratic_reciprocity.lean index 876937bec856e..bb4db5899c3c4 100644 --- a/src/number_theory/zsqrtd/quadratic_reciprocity.lean +++ b/src/number_theory/zsqrtd/quadratic_reciprocity.lean @@ -9,6 +9,9 @@ import number_theory.legendre_symbol.quadratic_reciprocity /-! # Facts about the gaussian integers relying on quadratic reciprocity. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main statements `prime_iff_mod_four_eq_three_of_nat_prime` diff --git a/src/ring_theory/dedekind_domain/selmer_group.lean b/src/ring_theory/dedekind_domain/selmer_group.lean index f729e75d1c898..adcbbfc9e1fb3 100644 --- a/src/ring_theory/dedekind_domain/selmer_group.lean +++ b/src/ring_theory/dedekind_domain/selmer_group.lean @@ -11,6 +11,9 @@ import ring_theory.norm /-! # Selmer groups of fraction fields of Dedekind domains +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Let $K$ be the field of fractions of a Dedekind domain $R$. For any set $S$ of prime ideals in the height one spectrum of $R$, and for any natural number $n$, the Selmer group $K(S, n)$ is defined to be the subgroup of the unit group $K^\times$ modulo $n$-th powers where each element has $v$-adic diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean index c440ab66e49f4..e98541fca9c39 100644 --- a/src/set_theory/game/basic.lean +++ b/src/set_theory/game/basic.lean @@ -9,6 +9,9 @@ import tactic.abel /-! # Combinatorial games. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define the quotient of pre-games by the equivalence relation `p ≈ q ↔ p ≤ q ∧ q ≤ p` (its `antisymmetrization`), and construct an instance `add_comm_group game`, as well as an instance `partial_order game`. diff --git a/src/set_theory/game/ordinal.lean b/src/set_theory/game/ordinal.lean index 34baa6c2abfb3..1fb9ef66b97e6 100644 --- a/src/set_theory/game/ordinal.lean +++ b/src/set_theory/game/ordinal.lean @@ -10,6 +10,9 @@ import set_theory.ordinal.natural_ops /-! # Ordinals as games +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the canonical map `ordinal → pgame`, where every ordinal is mapped to the game whose left set consists of all previous ordinals. From 147b294346843885f952c5171e9606616a8fd869 Mon Sep 17 00:00:00 2001 From: Apurva Date: Thu, 29 Jun 2023 07:01:52 +0000 Subject: [PATCH 12/16] feat(analysis/convex/cone/proper): add hyperplane_separation and comap (#19008) We add the theorem `hyperplane_separation` which is a relative version of [convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem](https://leanprover-community.github.io/mathlib_docs/analysis/convex/cone/dual.html#convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem). This is the most general form of Farkas' lemma (that I know of) for convex cones. We also add `proper_cone.comap` and a few theorems about it. Co-authored-by: Apurva Nakade --- src/analysis/convex/cone/proper.lean | 82 ++++++++++++++++++++++++++-- 1 file changed, 78 insertions(+), 4 deletions(-) diff --git a/src/analysis/convex/cone/proper.lean b/src/analysis/convex/cone/proper.lean index e85a633104328..9babbda4c6ef3 100644 --- a/src/analysis/convex/cone/proper.lean +++ b/src/analysis/convex/cone/proper.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Apurva Nakade -/ import analysis.convex.cone.dual +import analysis.inner_product_space.adjoint /-! # Proper cones @@ -17,8 +18,6 @@ linear programs, the results from this file can be used to prove duality theorem ## TODO The next steps are: -- Prove the cone version of Farkas' lemma (2.3.4 in the reference). -- Add comap, adjoint - Add convex_cone_class that extends set_like and replace the below instance - Define the positive cone as a proper cone. - Define primal and dual cone programs and prove weak duality. @@ -33,6 +32,8 @@ The next steps are: -/ +open continuous_linear_map filter set + namespace convex_cone variables {𝕜 : Type*} [ordered_semiring 𝕜] @@ -118,12 +119,13 @@ section inner_product_space variables {E : Type*} [normed_add_comm_group E] [inner_product_space ℝ E] variables {F : Type*} [normed_add_comm_group F] [inner_product_space ℝ F] +variables {G : Type*} [normed_add_comm_group G] [inner_product_space ℝ G] protected lemma pointed (K : proper_cone ℝ E) : (K : convex_cone ℝ E).pointed := (K : convex_cone ℝ E).pointed_of_nonempty_of_is_closed K.nonempty K.is_closed /-- The closure of image of a proper cone under a continuous `ℝ`-linear map is a proper cone. We -use continuous maps here so that the adjoint of f is also a map between proper cones. -/ +use continuous maps here so that the comap of f is also a map between proper cones. -/ noncomputable def map (f : E →L[ℝ] F) (K : proper_cone ℝ E) : proper_cone ℝ F := { to_convex_cone := convex_cone.closure (convex_cone.map (f : E →ₗ[ℝ] F) ↑K), nonempty' := ⟨ 0, subset_closure $ set_like.mem_coe.2 $ convex_cone.mem_map.2 @@ -152,18 +154,90 @@ lemma coe_dual (K : proper_cone ℝ E) : ↑(dual K) = (K : set E).inner_dual_co y ∈ dual K ↔ ∀ ⦃x⦄, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ := by {rw [← mem_coe, coe_dual, mem_inner_dual_cone _ _], refl} --- TODO: add comap, adjoint +/-- The preimage of a proper cone under a continuous `ℝ`-linear map is a proper cone. -/ +noncomputable def comap (f : E →L[ℝ] F) (S : proper_cone ℝ F) : proper_cone ℝ E := +{ to_convex_cone := convex_cone.comap (f : E →ₗ[ℝ] F) S, + nonempty' := ⟨ 0, + begin + simp only [convex_cone.comap, mem_preimage, map_zero, set_like.mem_coe, mem_coe], + apply proper_cone.pointed, + end ⟩, + is_closed' := + begin + simp only [convex_cone.comap, continuous_linear_map.coe_coe], + apply is_closed.preimage f.2 S.is_closed, + end } + +@[simp] lemma coe_comap (f : E →L[ℝ] F) (S : proper_cone ℝ F) : (S.comap f : set E) = f ⁻¹' S := +rfl + +@[simp] lemma comap_id (S : convex_cone ℝ E) : S.comap linear_map.id = S := +set_like.coe_injective preimage_id + +lemma comap_comap (g : F →L[ℝ] G) (f : E →L[ℝ] F) (S : proper_cone ℝ G) : + (S.comap g).comap f = S.comap (g.comp f) := +set_like.coe_injective $ preimage_comp.symm + +@[simp] lemma mem_comap {f : E →L[ℝ] F} {S : proper_cone ℝ F} {x : E} : x ∈ S.comap f ↔ f x ∈ S := +iff.rfl end inner_product_space section complete_space variables {E : Type*} [normed_add_comm_group E] [inner_product_space ℝ E] [complete_space E] +variables {F : Type*} [normed_add_comm_group F] [inner_product_space ℝ F] [complete_space F] /-- The dual of the dual of a proper cone is itself. -/ @[simp] theorem dual_dual (K : proper_cone ℝ E) : K.dual.dual = K := proper_cone.ext' $ (K : convex_cone ℝ E).inner_dual_cone_of_inner_dual_cone_eq_self K.nonempty K.is_closed +/-- This is a relative version of +`convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem`, which we recover by setting +`f` to be the identity map. This is a geometric interpretation of the Farkas' lemma +stated using proper cones. -/ +theorem hyperplane_separation (K : proper_cone ℝ E) {f : E →L[ℝ] F} {b : F} : + b ∈ K.map f ↔ ∀ y : F, (adjoint f y) ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ := iff.intro +begin + -- suppose `b ∈ K.map f` + simp only [proper_cone.mem_map, proper_cone.mem_dual, adjoint_inner_right, + convex_cone.mem_closure, mem_closure_iff_seq_limit], + + -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b` + rintros ⟨seq, hmem, htends⟩ y hinner, + + suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ, from ge_of_tendsto' (continuous.seq_continuous + (continuous.inner (@continuous_const _ _ _ _ y) continuous_id) htends) h, + + intro n, + obtain ⟨_, h, hseq⟩ := hmem n, + simpa only [← hseq, real_inner_comm] using (hinner h), +end +begin + -- proof by contradiction + -- suppose `b ∉ K.map f` + intro h, + contrapose! h, + + -- as `b ∉ K.map f`, there is a hyperplane `y` separating `b` from `K.map f` + obtain ⟨y, hxy, hyb⟩ := convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem _ + (K.map f).nonempty (K.map f).is_closed h, + + -- the rest of the proof is a straightforward algebraic manipulation + refine ⟨y, _, hyb⟩, + simp_rw [proper_cone.mem_dual, adjoint_inner_right], + intros x hxK, + apply hxy (f x), + rw [to_convex_cone_eq_coe, proper_cone.coe_map], + apply subset_closure, + rw [set_like.mem_coe, convex_cone.mem_map], + use ⟨x, hxK, rfl⟩, +end + +theorem hyperplane_separation_of_nmem (K : proper_cone ℝ E) {f : E →L[ℝ] F} {b : F} + (disj : b ∉ K.map f) : ∃ y : F, (adjoint f y) ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0 := +by { contrapose! disj, rwa K.hyperplane_separation } + end complete_space end proper_cone From 9240e8be927a0955b9a82c6c85ef499ee3a626b8 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Thu, 29 Jun 2023 14:58:24 +0000 Subject: [PATCH 13/16] chore(*): add mathlib4 synchronization comments (#19218) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebraic_geometry.elliptic_curve.weierstrass` * `analysis.complex.upper_half_plane.basic` * `analysis.complex.upper_half_plane.functions_bounded_at_infty` * `analysis.complex.upper_half_plane.metric` * `analysis.complex.upper_half_plane.topology` * `analysis.fourier.riemann_lebesgue_lemma` * `analysis.inner_product_space.linear_pmap` * `analysis.special_functions.gamma.beta` * `category_theory.closed.ideal` * `category_theory.monad.equiv_mon` * `control.random` * `geometry.euclidean.monge_point` * `geometry.manifold.complex` * `geometry.manifold.partition_of_unity` * `logic.equiv.array` * `number_theory.legendre_symbol.jacobi_symbol` * `number_theory.modular` * `number_theory.modular_forms.jacobi_theta.basic` * `number_theory.modular_forms.slash_actions` * `number_theory.modular_forms.slash_invariant_forms` * `ring_theory.witt_vector.compare` * `ring_theory.witt_vector.discrete_valuation_ring` * `ring_theory.witt_vector.domain` * `ring_theory.witt_vector.frobenius` * `ring_theory.witt_vector.identities` * `ring_theory.witt_vector.init_tail` * `ring_theory.witt_vector.mul_coeff` * `ring_theory.witt_vector.truncated` * `ring_theory.witt_vector.verschiebung` * `set_theory.game.birthday` * `set_theory.game.impartial` * `set_theory.surreal.basic` * `testing.slim_check.gen` * `testing.slim_check.sampleable` * `testing.slim_check.testable` --- src/algebraic_geometry/elliptic_curve/weierstrass.lean | 3 +++ src/analysis/complex/upper_half_plane/basic.lean | 3 +++ .../complex/upper_half_plane/functions_bounded_at_infty.lean | 3 +++ src/analysis/complex/upper_half_plane/metric.lean | 3 +++ src/analysis/complex/upper_half_plane/topology.lean | 3 +++ src/analysis/fourier/riemann_lebesgue_lemma.lean | 3 +++ src/analysis/inner_product_space/linear_pmap.lean | 3 +++ src/analysis/special_functions/gamma/beta.lean | 3 +++ src/category_theory/closed/ideal.lean | 3 +++ src/category_theory/monad/equiv_mon.lean | 3 +++ src/control/random.lean | 3 +++ src/geometry/euclidean/monge_point.lean | 3 +++ src/geometry/manifold/complex.lean | 3 +++ src/geometry/manifold/partition_of_unity.lean | 3 +++ src/logic/equiv/array.lean | 3 +++ src/number_theory/legendre_symbol/jacobi_symbol.lean | 3 +++ src/number_theory/modular.lean | 3 +++ src/number_theory/modular_forms/jacobi_theta/basic.lean | 3 +++ src/number_theory/modular_forms/slash_actions.lean | 3 +++ src/number_theory/modular_forms/slash_invariant_forms.lean | 3 +++ src/ring_theory/witt_vector/compare.lean | 3 +++ src/ring_theory/witt_vector/discrete_valuation_ring.lean | 3 +++ src/ring_theory/witt_vector/domain.lean | 3 +++ src/ring_theory/witt_vector/frobenius.lean | 3 +++ src/ring_theory/witt_vector/identities.lean | 3 +++ src/ring_theory/witt_vector/init_tail.lean | 3 +++ src/ring_theory/witt_vector/mul_coeff.lean | 3 +++ src/ring_theory/witt_vector/truncated.lean | 3 +++ src/ring_theory/witt_vector/verschiebung.lean | 3 +++ src/set_theory/game/birthday.lean | 3 +++ src/set_theory/game/impartial.lean | 3 +++ src/set_theory/surreal/basic.lean | 3 +++ src/testing/slim_check/gen.lean | 3 +++ src/testing/slim_check/sampleable.lean | 3 +++ src/testing/slim_check/testable.lean | 3 +++ 35 files changed, 105 insertions(+) diff --git a/src/algebraic_geometry/elliptic_curve/weierstrass.lean b/src/algebraic_geometry/elliptic_curve/weierstrass.lean index bd0c781db4fb0..ea856a6ac27ac 100644 --- a/src/algebraic_geometry/elliptic_curve/weierstrass.lean +++ b/src/algebraic_geometry/elliptic_curve/weierstrass.lean @@ -11,6 +11,9 @@ import tactic.linear_combination /-! # Weierstrass equations of elliptic curves +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the structure of an elliptic curve as a nonsingular Weierstrass curve given by a Weierstrass equation, which is mathematically accurate in many cases but also good for computation. diff --git a/src/analysis/complex/upper_half_plane/basic.lean b/src/analysis/complex/upper_half_plane/basic.lean index b92328ac57922..02d2506086cf0 100644 --- a/src/analysis/complex/upper_half_plane/basic.lean +++ b/src/analysis/complex/upper_half_plane/basic.lean @@ -13,6 +13,9 @@ import tactic.linear_combination /-! # The upper half plane and its automorphisms +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines `upper_half_plane` to be the upper half plane in `ℂ`. We furthermore equip it with the structure of an `GL_pos 2 ℝ` action by diff --git a/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean b/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean index 53538b4fa044d..26d6235065751 100644 --- a/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean +++ b/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean @@ -11,6 +11,9 @@ import order.filter.zero_and_bounded_at_filter /-! # Bounded at infinity +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + For complex valued functions on the upper half plane, this file defines the filter `at_im_infty` required for defining when functions are bounded at infinity and zero at infinity. Both of which are relevant for defining modular forms. diff --git a/src/analysis/complex/upper_half_plane/metric.lean b/src/analysis/complex/upper_half_plane/metric.lean index 39d5417caffa5..f240cfc3adbd2 100644 --- a/src/analysis/complex/upper_half_plane/metric.lean +++ b/src/analysis/complex/upper_half_plane/metric.lean @@ -10,6 +10,9 @@ import geometry.euclidean.inversion /-! # Metric on the upper half-plane +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define a `metric_space` structure on the `upper_half_plane`. We use hyperbolic (Poincaré) distance given by `dist z w = 2 * arsinh (dist (z : ℂ) w / (2 * real.sqrt (z.im * w.im)))` instead of the induced diff --git a/src/analysis/complex/upper_half_plane/topology.lean b/src/analysis/complex/upper_half_plane/topology.lean index 418466831de71..63eeb52de6c0e 100644 --- a/src/analysis/complex/upper_half_plane/topology.lean +++ b/src/analysis/complex/upper_half_plane/topology.lean @@ -13,6 +13,9 @@ import topology.homotopy.contractible /-! # Topology on the upper half plane +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we introduce a `topological_space` structure on the upper half plane and provide various instances. -/ diff --git a/src/analysis/fourier/riemann_lebesgue_lemma.lean b/src/analysis/fourier/riemann_lebesgue_lemma.lean index 31cd3a8acb7ce..d986b81e740a8 100644 --- a/src/analysis/fourier/riemann_lebesgue_lemma.lean +++ b/src/analysis/fourier/riemann_lebesgue_lemma.lean @@ -16,6 +16,9 @@ import topology.metric_space.emetric_paracompact /-! # The Riemann-Lebesgue Lemma +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we prove the Riemann-Lebesgue lemma, for functions on finite-dimensional real vector spaces `V`: if `f` is a function on `V` (valued in a complete normed space `E`), then the Fourier transform of `f`, viewed as a function on the dual space of `V`, tends to 0 along the diff --git a/src/analysis/inner_product_space/linear_pmap.lean b/src/analysis/inner_product_space/linear_pmap.lean index 8d36210252e4c..0613e2dfe34cd 100644 --- a/src/analysis/inner_product_space/linear_pmap.lean +++ b/src/analysis/inner_product_space/linear_pmap.lean @@ -12,6 +12,9 @@ import topology.algebra.module.basic # Partially defined linear operators on Hilbert spaces +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We will develop the basics of the theory of unbounded operators on Hilbert spaces. ## Main definitions diff --git a/src/analysis/special_functions/gamma/beta.lean b/src/analysis/special_functions/gamma/beta.lean index 42a05012901ec..9a115267c346a 100644 --- a/src/analysis/special_functions/gamma/beta.lean +++ b/src/analysis/special_functions/gamma/beta.lean @@ -11,6 +11,9 @@ import analysis.analytic.isolated_zeros /-! # The Beta function, and further properties of the Gamma function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define the Beta integral, relate Beta and Gamma functions, and prove some refined properties of the Gamma function using these relations. diff --git a/src/category_theory/closed/ideal.lean b/src/category_theory/closed/ideal.lean index 84959823ad8ec..47f10852c5734 100644 --- a/src/category_theory/closed/ideal.lean +++ b/src/category_theory/closed/ideal.lean @@ -14,6 +14,9 @@ import category_theory.subterminal /-! # Exponential ideals +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + An exponential ideal of a cartesian closed category `C` is a subcategory `D ⊆ C` such that for any `B : D` and `A : C`, the exponential `A ⟹ B` is in `D`: resembling ring theoretic ideals. We define the notion here for inclusion functors `i : D ⥤ C` rather than explicit subcategories to diff --git a/src/category_theory/monad/equiv_mon.lean b/src/category_theory/monad/equiv_mon.lean index 4c35b16c79667..7765dc2798ed7 100644 --- a/src/category_theory/monad/equiv_mon.lean +++ b/src/category_theory/monad/equiv_mon.lean @@ -11,6 +11,9 @@ import category_theory.monoidal.Mon_ # The equivalence between `Monad C` and `Mon_ (C ⥤ C)`. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + A monad "is just" a monoid in the category of endofunctors. # Definitions/Theorems diff --git a/src/control/random.lean b/src/control/random.lean index 0b6581b91df80..b6fffc4515b7d 100644 --- a/src/control/random.lean +++ b/src/control/random.lean @@ -13,6 +13,9 @@ import tactic.norm_num /-! # Rand Monad and Random Class +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This module provides tools for formulating computations guided by randomness and for defining objects that can be created randomly. diff --git a/src/geometry/euclidean/monge_point.lean b/src/geometry/euclidean/monge_point.lean index f6e741a38b287..250e4f686b38e 100644 --- a/src/geometry/euclidean/monge_point.lean +++ b/src/geometry/euclidean/monge_point.lean @@ -8,6 +8,9 @@ import geometry.euclidean.circumcenter /-! # Monge point and orthocenter +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the orthocenter of a triangle, via its n-dimensional generalization, the Monge point of a simplex. diff --git a/src/geometry/manifold/complex.lean b/src/geometry/manifold/complex.lean index 5e3d546fa2a71..bcd39594ce8bc 100644 --- a/src/geometry/manifold/complex.lean +++ b/src/geometry/manifold/complex.lean @@ -10,6 +10,9 @@ import topology.locally_constant.basic /-! # Holomorphic functions on complex manifolds +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Thanks to the rigidity of complex-differentiability compared to real-differentiability, there are many results about complex manifolds with no analogue for manifolds over a general normed field. For now, this file contains just two (closely related) such results: diff --git a/src/geometry/manifold/partition_of_unity.lean b/src/geometry/manifold/partition_of_unity.lean index 7598e00e1f479..e345b485faf25 100644 --- a/src/geometry/manifold/partition_of_unity.lean +++ b/src/geometry/manifold/partition_of_unity.lean @@ -11,6 +11,9 @@ import topology.shrinking_lemma /-! # Smooth partition of unity +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we define two structures, `smooth_bump_covering` and `smooth_partition_of_unity`. Both structures describe coverings of a set by a locally finite family of supports of smooth functions with some additional properties. The former structure is mostly useful as an intermediate step in diff --git a/src/logic/equiv/array.lean b/src/logic/equiv/array.lean index 5e1f98c7d71cf..cd709ecf95cbc 100644 --- a/src/logic/equiv/array.lean +++ b/src/logic/equiv/array.lean @@ -10,6 +10,9 @@ import control.traversable.equiv /-! # Equivalences involving `array` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We keep this separate from the file containing `list`-like equivalences as those have no future in mathlib4. -/ diff --git a/src/number_theory/legendre_symbol/jacobi_symbol.lean b/src/number_theory/legendre_symbol/jacobi_symbol.lean index 597367d2409f4..7cead399fc0db 100644 --- a/src/number_theory/legendre_symbol/jacobi_symbol.lean +++ b/src/number_theory/legendre_symbol/jacobi_symbol.lean @@ -8,6 +8,9 @@ import number_theory.legendre_symbol.quadratic_reciprocity /-! # The Jacobi Symbol +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the Jacobi symbol and prove its main properties. ## Main definitions diff --git a/src/number_theory/modular.lean b/src/number_theory/modular.lean index 901c51743781c..01ee6d1c547db 100644 --- a/src/number_theory/modular.lean +++ b/src/number_theory/modular.lean @@ -12,6 +12,9 @@ import linear_algebra.matrix.general_linear_group /-! # The action of the modular group SL(2, ℤ) on the upper half-plane +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the action of `SL(2,ℤ)` on `ℍ` (via restriction of the `SL(2,ℝ)` action in `analysis.complex.upper_half_plane`). We then define the standard fundamental domain (`modular_group.fd`, `𝒟`) for this action and show diff --git a/src/number_theory/modular_forms/jacobi_theta/basic.lean b/src/number_theory/modular_forms/jacobi_theta/basic.lean index 5dfc5e66f6a90..86c8bd4862385 100644 --- a/src/number_theory/modular_forms/jacobi_theta/basic.lean +++ b/src/number_theory/modular_forms/jacobi_theta/basic.lean @@ -10,6 +10,9 @@ import analysis.complex.upper_half_plane.topology /-! # Jacobi's theta function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines the Jacobi theta function $$\theta(\tau) = \sum_{n \in \mathbb{Z}} \exp (i \pi n ^ 2 \tau),$$ diff --git a/src/number_theory/modular_forms/slash_actions.lean b/src/number_theory/modular_forms/slash_actions.lean index 9c980afa75e78..591978ad458c7 100644 --- a/src/number_theory/modular_forms/slash_actions.lean +++ b/src/number_theory/modular_forms/slash_actions.lean @@ -9,6 +9,9 @@ import linear_algebra.matrix.special_linear_group /-! # Slash actions +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines a class of slash actions, which are families of right actions of a given group parametrized by some Type. This is modeled on the slash action of `GL_pos (fin 2) ℝ` on the space of modular forms. diff --git a/src/number_theory/modular_forms/slash_invariant_forms.lean b/src/number_theory/modular_forms/slash_invariant_forms.lean index 98b6074ce71ee..701fe0e66479a 100644 --- a/src/number_theory/modular_forms/slash_invariant_forms.lean +++ b/src/number_theory/modular_forms/slash_invariant_forms.lean @@ -8,6 +8,9 @@ import number_theory.modular_forms.slash_actions /-! # Slash invariant forms +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines functions that are invariant under a `slash_action` which forms the basis for defining `modular_form` and `cusp_form`. We prove several instances for such spaces, in particular that they form a module. diff --git a/src/ring_theory/witt_vector/compare.lean b/src/ring_theory/witt_vector/compare.lean index e6e4ad3ef3fca..8041ad4f5aecb 100644 --- a/src/ring_theory/witt_vector/compare.lean +++ b/src/ring_theory/witt_vector/compare.lean @@ -12,6 +12,9 @@ import number_theory.padics.ring_homs # Comparison isomorphism between `witt_vector p (zmod p)` and `ℤ_[p]` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We construct a ring isomorphism between `witt_vector p (zmod p)` and `ℤ_[p]`. This isomorphism follows from the fact that both satisfy the universal property of the inverse limit of `zmod (p^n)`. diff --git a/src/ring_theory/witt_vector/discrete_valuation_ring.lean b/src/ring_theory/witt_vector/discrete_valuation_ring.lean index abe97d3cecbc2..f44bfbc19e7a6 100644 --- a/src/ring_theory/witt_vector/discrete_valuation_ring.lean +++ b/src/ring_theory/witt_vector/discrete_valuation_ring.lean @@ -13,6 +13,9 @@ import tactic.linear_combination # Witt vectors over a perfect ring +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file establishes that Witt vectors over a perfect field are a discrete valuation ring. When `k` is a perfect ring, a nonzero `a : 𝕎 k` can be written as `p^m * b` for some `m : ℕ` and `b : 𝕎 k` with nonzero 0th coefficient. diff --git a/src/ring_theory/witt_vector/domain.lean b/src/ring_theory/witt_vector/domain.lean index 356d1f0532bd6..2e00ed1545195 100644 --- a/src/ring_theory/witt_vector/domain.lean +++ b/src/ring_theory/witt_vector/domain.lean @@ -10,6 +10,9 @@ import ring_theory.witt_vector.identities # Witt vectors over a domain +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file builds to the proof `witt_vector.is_domain`, an instance that says if `R` is an integral domain, then so is `𝕎 R`. It depends on the API around iterated applications diff --git a/src/ring_theory/witt_vector/frobenius.lean b/src/ring_theory/witt_vector/frobenius.lean index 912a4b5962c9a..2f9692e4afaa4 100644 --- a/src/ring_theory/witt_vector/frobenius.lean +++ b/src/ring_theory/witt_vector/frobenius.lean @@ -14,6 +14,9 @@ import field_theory.perfect_closure /-! ## The Frobenius operator +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + If `R` has characteristic `p`, then there is a ring endomorphism `frobenius R p` that raises `r : R` to the power `p`. By applying `witt_vector.map` to `frobenius R p`, we obtain a ring endomorphism `𝕎 R →+* 𝕎 R`. diff --git a/src/ring_theory/witt_vector/identities.lean b/src/ring_theory/witt_vector/identities.lean index 5f30cbae076ab..e64810ad66372 100644 --- a/src/ring_theory/witt_vector/identities.lean +++ b/src/ring_theory/witt_vector/identities.lean @@ -11,6 +11,9 @@ import ring_theory.witt_vector.mul_p /-! ## Identities between operations on the ring of Witt vectors +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we derive common identities between the Frobenius and Verschiebung operators. ## Main declarations diff --git a/src/ring_theory/witt_vector/init_tail.lean b/src/ring_theory/witt_vector/init_tail.lean index 1333a32ac7a30..2be11f7e6b5d1 100644 --- a/src/ring_theory/witt_vector/init_tail.lean +++ b/src/ring_theory/witt_vector/init_tail.lean @@ -11,6 +11,9 @@ import ring_theory.witt_vector.is_poly # `init` and `tail` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Given a Witt vector `x`, we are sometimes interested in its components before and after an index `n`. This file defines those operations, proves that `init` is polynomial, diff --git a/src/ring_theory/witt_vector/mul_coeff.lean b/src/ring_theory/witt_vector/mul_coeff.lean index 9903f792a5714..c5973058f8a56 100644 --- a/src/ring_theory/witt_vector/mul_coeff.lean +++ b/src/ring_theory/witt_vector/mul_coeff.lean @@ -10,6 +10,9 @@ import data.mv_polynomial.supported /-! # Leading terms of Witt vector multiplication +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The goal of this file is to study the leading terms of the formula for the `n+1`st coefficient of a product of Witt vectors `x` and `y` over a ring of characteristic `p`. We aim to isolate the `n+1`st coefficients of `x` and `y`, and express the rest of the product diff --git a/src/ring_theory/witt_vector/truncated.lean b/src/ring_theory/witt_vector/truncated.lean index 6bc9fee887a85..28a88b8f8070b 100644 --- a/src/ring_theory/witt_vector/truncated.lean +++ b/src/ring_theory/witt_vector/truncated.lean @@ -10,6 +10,9 @@ import ring_theory.witt_vector.init_tail # Truncated Witt vectors +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The ring of truncated Witt vectors (of length `n`) is a quotient of the ring of Witt vectors. It retains the first `n` coefficients of each Witt vector. In this file, we set up the basic quotient API for this ring. diff --git a/src/ring_theory/witt_vector/verschiebung.lean b/src/ring_theory/witt_vector/verschiebung.lean index f280e110e62cd..24286e1adef51 100644 --- a/src/ring_theory/witt_vector/verschiebung.lean +++ b/src/ring_theory/witt_vector/verschiebung.lean @@ -11,6 +11,9 @@ import ring_theory.witt_vector.is_poly /-! ## The Verschiebung operator +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## References * [Hazewinkel, *Witt Vectors*][Haze09] diff --git a/src/set_theory/game/birthday.lean b/src/set_theory/game/birthday.lean index c9b2642f8e8b8..163336f5f2243 100644 --- a/src/set_theory/game/birthday.lean +++ b/src/set_theory/game/birthday.lean @@ -10,6 +10,9 @@ import set_theory.ordinal.natural_ops /-! # Birthdays of games +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The birthday of a game is an ordinal that represents at which "step" the game was constructed. We define it recursively as the least ordinal larger than the birthdays of its left and right games. We prove the basic properties about these. diff --git a/src/set_theory/game/impartial.lean b/src/set_theory/game/impartial.lean index 94076d236cf67..c361208cf43b6 100644 --- a/src/set_theory/game/impartial.lean +++ b/src/set_theory/game/impartial.lean @@ -10,6 +10,9 @@ import tactic.nth_rewrite /-! # Basic definitions about impartial (pre-)games +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We will define an impartial game, one in which left and right can make exactly the same moves. Our definition differs slightly by saying that the game is always equivalent to its negative, no matter what moves are played. This allows for games such as poker-nim to be classifed as diff --git a/src/set_theory/surreal/basic.lean b/src/set_theory/surreal/basic.lean index 13d1fb908e27b..6a9d8bf27327a 100644 --- a/src/set_theory/surreal/basic.lean +++ b/src/set_theory/surreal/basic.lean @@ -10,6 +10,9 @@ import set_theory.game.ordinal /-! # Surreal numbers +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games. A pregame is `numeric` if all the Left options are strictly smaller than all the Right options, and diff --git a/src/testing/slim_check/gen.lean b/src/testing/slim_check/gen.lean index eff80477cdce2..d0e76abcadf90 100644 --- a/src/testing/slim_check/gen.lean +++ b/src/testing/slim_check/gen.lean @@ -11,6 +11,9 @@ import data.list.perm /-! # `gen` Monad +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This monad is used to formulate randomized computations with a parameter to specify the desired size of the result. diff --git a/src/testing/slim_check/sampleable.lean b/src/testing/slim_check/sampleable.lean index c14c317264fde..ac9b0ac097fe2 100644 --- a/src/testing/slim_check/sampleable.lean +++ b/src/testing/slim_check/sampleable.lean @@ -14,6 +14,9 @@ import tactic.linarith /-! # `sampleable` Class +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This class permits the creation samples of a given type controlling the size of those values using the `gen` monad`. It also helps minimize examples by creating smaller versions of given values. diff --git a/src/testing/slim_check/testable.lean b/src/testing/slim_check/testable.lean index 9888738ef57d3..b355cc40c8c98 100644 --- a/src/testing/slim_check/testable.lean +++ b/src/testing/slim_check/testable.lean @@ -9,6 +9,9 @@ import testing.slim_check.sampleable /-! # `testable` Class +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Testable propositions have a procedure that can generate counter-examples together with a proof that they invalidate the proposition. From 311ef8c4b4ae2804ea76b8a611bc5ea1d9c16872 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 30 Jun 2023 04:04:12 +0000 Subject: [PATCH 14/16] chore(category_theory/concrete_category): reorder universes (#19222) These will make life slightly easier dealing with our universe problems. Most of these changes have in fact already been made in mathlib4, and the remainder are in https://github.com/leanprover-community/mathlib4/pull/5605. Co-authored-by: Scott Morrison --- .../concrete_category/basic.lean | 54 ++++++++++--------- 1 file changed, 29 insertions(+), 25 deletions(-) diff --git a/src/category_theory/concrete_category/basic.lean b/src/category_theory/concrete_category/basic.lean index 2511901ec5bad..0029fae725175 100644 --- a/src/category_theory/concrete_category/basic.lean +++ b/src/category_theory/concrete_category/basic.lean @@ -38,7 +38,7 @@ See [Ahrens and Lumsdaine, *Displayed Categories*][ahrens2017] for related work. -/ -universes w v v' u +universes w v v' u u' namespace category_theory @@ -60,7 +60,7 @@ class concrete_category (C : Type u) [category.{v} C] := attribute [instance] concrete_category.forget_faithful /-- The forgetful functor from a concrete category to `Type u`. -/ -@[reducible] def forget (C : Type v) [category C] [concrete_category.{u} C] : C ⥤ Type u := +@[reducible] def forget (C : Type u) [category.{v} C] [concrete_category.{w} C] : C ⥤ Type w := concrete_category.forget C instance concrete_category.types : concrete_category (Type u) := @@ -75,14 +75,14 @@ You can use it on particular examples as: instance : has_coe_to_sort X := concrete_category.has_coe_to_sort X ``` -/ -def concrete_category.has_coe_to_sort (C : Type v) [category C] [concrete_category C] : - has_coe_to_sort C (Type u) := +def concrete_category.has_coe_to_sort (C : Type u) [category.{v} C] [concrete_category.{w} C] : + has_coe_to_sort C (Type w) := ⟨(concrete_category.forget C).obj⟩ section local attribute [instance] concrete_category.has_coe_to_sort -variables {C : Type v} [category C] [concrete_category C] +variables {C : Type u} [category.{v} C] [concrete_category.{w} C] @[simp] lemma forget_obj_eq_coe {X : C} : (forget C).obj X = X := rfl @@ -170,51 +170,54 @@ end `has_forget₂ C D`, where `C` and `D` are both concrete categories, provides a functor `forget₂ C D : C ⥤ D` and a proof that `forget₂ ⋙ (forget D) = forget C`. -/ -class has_forget₂ (C : Type v) (D : Type v') [category C] [concrete_category.{u} C] [category D] - [concrete_category.{u} D] := +class has_forget₂ (C : Type u) (D : Type u') [category.{v} C] [concrete_category.{w} C] + [category.{v'} D] [concrete_category.{w} D] := (forget₂ : C ⥤ D) (forget_comp : forget₂ ⋙ (forget D) = forget C . obviously) /-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance `has_forget₂ C `. -/ -@[reducible] def forget₂ (C : Type v) (D : Type v') [category C] [concrete_category C] [category D] - [concrete_category D] [has_forget₂ C D] : C ⥤ D := +@[reducible] def forget₂ (C : Type u) (D : Type u') [category.{v} C] [concrete_category.{w} C] + [category.{v'} D] [concrete_category.{w} D] [has_forget₂ C D] : C ⥤ D := has_forget₂.forget₂ -instance forget₂_faithful (C : Type v) (D : Type v') [category C] [concrete_category C] [category D] - [concrete_category D] [has_forget₂ C D] : faithful (forget₂ C D) := +instance forget₂_faithful (C : Type u) (D : Type u') [category.{v} C] [concrete_category.{w} C] + [category.{v'} D] [concrete_category.{w} D] [has_forget₂ C D] : faithful (forget₂ C D) := has_forget₂.forget_comp.faithful_of_comp -instance forget₂_preserves_monomorphisms (C : Type v) (D : Type v') [category C] - [concrete_category C] [category D] [concrete_category D] [has_forget₂ C D] +instance forget₂_preserves_monomorphisms (C : Type u) (D : Type u') + [category.{v} C] [concrete_category.{w} C] + [category.{v'} D] [concrete_category.{w} D] [has_forget₂ C D] [(forget C).preserves_monomorphisms] : (forget₂ C D).preserves_monomorphisms := have (forget₂ C D ⋙ forget D).preserves_monomorphisms, by { simp only [has_forget₂.forget_comp], apply_instance }, by exactI functor.preserves_monomorphisms_of_preserves_of_reflects _ (forget D) -instance forget₂_preserves_epimorphisms (C : Type v) (D : Type v') [category C] - [concrete_category C] [category D] [concrete_category D] [has_forget₂ C D] +instance forget₂_preserves_epimorphisms (C : Type u) (D : Type u') + [category.{v} C] [concrete_category.{w} C] + [category.{v'} D] [concrete_category.{w} D] [has_forget₂ C D] [(forget C).preserves_epimorphisms] : (forget₂ C D).preserves_epimorphisms := have (forget₂ C D ⋙ forget D).preserves_epimorphisms, by { simp only [has_forget₂.forget_comp], apply_instance }, by exactI functor.preserves_epimorphisms_of_preserves_of_reflects _ (forget D) -instance induced_category.concrete_category {C : Type v} {D : Type v'} [category D] - [concrete_category D] (f : C → D) : - concrete_category (induced_category D f) := +instance induced_category.concrete_category {C : Type u} {D : Type u'} [category.{v'} D] + [concrete_category.{w} D] (f : C → D) : + concrete_category.{w} (induced_category D f) := { forget := induced_functor f ⋙ forget D } -instance induced_category.has_forget₂ {C : Type v} {D : Type v'} [category D] [concrete_category D] +instance induced_category.has_forget₂ + {C : Type u} {D : Type u'} [category.{v'} D] [concrete_category.{w} D] (f : C → D) : has_forget₂ (induced_category D f) D := { forget₂ := induced_functor f, forget_comp := rfl } -instance full_subcategory.concrete_category {C : Type v} [category C] [concrete_category C] +instance full_subcategory.concrete_category {C : Type u} [category.{v} C] [concrete_category.{w} C] (Z : C → Prop) : concrete_category (full_subcategory Z) := { forget := full_subcategory_inclusion Z ⋙ forget C } -instance full_subcategory.has_forget₂ {C : Type v} [category C] [concrete_category C] +instance full_subcategory.has_forget₂ {C : Type u} [category.{v} C] [concrete_category.{w} C] (Z : C → Prop) : has_forget₂ (full_subcategory Z) C := { forget₂ := full_subcategory_inclusion Z, forget_comp := rfl } @@ -223,8 +226,9 @@ instance full_subcategory.has_forget₂ {C : Type v} [category C] [concrete_cate In order to construct a “partially forgetting” functor, we do not need to verify functor laws; it suffices to ensure that compositions agree with `forget₂ C D ⋙ forget D = forget C`. -/ -def has_forget₂.mk' {C : Type v} {D : Type v'} [category C] [concrete_category C] [category D] - [concrete_category D] (obj : C → D) (h_obj : ∀ X, (forget D).obj (obj X) = (forget C).obj X) +def has_forget₂.mk' {C : Type u} {D : Type u'} [category.{v} C] [concrete_category.{w} C] + [category.{v'} D] [concrete_category.{w} D] (obj : C → D) + (h_obj : ∀ X, (forget D).obj (obj X) = (forget C).obj X) (map : Π {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y} {f : X ⟶ Y}, (forget D).map (map f) == (forget C).map f) : has_forget₂ C D := @@ -233,8 +237,8 @@ has_forget₂ C D := /-- Every forgetful functor factors through the identity functor. This is not a global instance as it is prone to creating type class resolution loops. -/ -def has_forget_to_Type (C : Type v) [category C] [concrete_category C] : - has_forget₂ C (Type u) := +def has_forget_to_Type (C : Type u) [category.{v} C] [concrete_category.{w} C] : + has_forget₂ C (Type w) := { forget₂ := forget C, forget_comp := functor.comp_id _ } From 48fb5b5280e7c81672afc9524185ae994553ebf4 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 30 Jun 2023 11:29:36 +0000 Subject: [PATCH 15/16] refactor(*): move all `mk_simp_attribute` commands to 1 file (#19223) --- src/algebra/group/defs.lean | 4 - src/control/basic.lean | 5 +- src/control/monad/basic.lean | 4 - src/data/is_R_or_C/basic.lean | 2 - src/data/nat/parity.lean | 2 - src/data/prod/basic.lean | 4 +- src/data/set/basic.lean | 11 ++- src/data/set/image.lean | 16 +-- src/data/set/prod.lean | 10 +- src/data/subtype.lean | 2 +- src/data/typevec.lean | 5 - src/logic/basic.lean | 15 +-- src/logic/equiv/defs.lean | 17 ++-- src/logic/equiv/local_equiv.lean | 23 ----- src/logic/nontrivial.lean | 5 +- src/measure_theory/integral/bochner.lean | 11 ++- src/ring_theory/witt_vector/is_poly.lean | 3 - src/tactic/core.lean | 32 ------ src/tactic/equiv_rw.lean | 5 - src/tactic/mk_simp_attribute.lean | 119 +++++++++++++++++++++++ src/tactic/norm_cast.lean | 3 - src/tactic/split_ifs.lean | 5 - src/tactic/transport.lean | 17 ---- test/equiv_rw.lean | 6 +- 24 files changed, 173 insertions(+), 153 deletions(-) create mode 100644 src/tactic/mk_simp_attribute.lean diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean index 090c13ad34f05..a33049364eb5d 100644 --- a/src/algebra/group/defs.lean +++ b/src/algebra/group/defs.lean @@ -87,10 +87,6 @@ variables {G : Type*} to the additive one. -/ -mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to -reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are -division-free." - section has_mul variables [has_mul G] diff --git a/src/control/basic.lean b/src/control/basic.lean index ebb5951a04034..d5ee38648ff4e 100644 --- a/src/control/basic.lean +++ b/src/control/basic.lean @@ -5,6 +5,7 @@ Authors: Johannes Hölzl Extends the theory on functors, applicatives and monads. -/ +import tactic.mk_simp_attribute universes u v w variables {α β γ : Type u} @@ -14,9 +15,6 @@ notation a ` $< `:1 f:1 := f a section functor variables {f : Type u → Type v} [functor f] [is_lawful_functor f] -run_cmd mk_simp_attr `functor_norm -run_cmd tactic.add_doc_string `simp_attr.functor_norm "Simp set for functor_norm" - @[functor_norm] theorem functor.map_map (m : α → β) (g : β → γ) (x : f α) : g <$> (m <$> x) = (g ∘ m) <$> x := (comp_map _ _ _).symm @@ -85,6 +83,7 @@ lemma seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} : (f <$> x) >>= g show bind (f <$> x) g = bind x (g ∘ f), by rw [← bind_pure_comp_eq_map, bind_assoc]; simp [pure_bind] +@[monad_norm] lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x)) := (bind_map_eq_seq f x).symm diff --git a/src/control/monad/basic.lean b/src/control/monad/basic.lean index 916599b5d74d1..33cfffa056f56 100644 --- a/src/control/monad/basic.lean +++ b/src/control/monad/basic.lean @@ -38,11 +38,7 @@ functor, applicative, monad, simp -/ -mk_simp_attribute monad_norm none with functor_norm - attribute [ext] reader_t.ext state_t.ext except_t.ext option_t.ext -attribute [functor_norm] bind_assoc pure_bind bind_pure -attribute [monad_norm] seq_eq_bind_map universes u v @[monad_norm] diff --git a/src/data/is_R_or_C/basic.lean b/src/data/is_R_or_C/basic.lean index c2db17c4e3424..c747fef34bf60 100644 --- a/src/data/is_R_or_C/basic.lean +++ b/src/data/is_R_or_C/basic.lean @@ -70,8 +70,6 @@ class is_R_or_C (K : Type*) end -mk_simp_attribute is_R_or_C_simps "Simp attribute for lemmas about `is_R_or_C`" - variables {K E : Type*} [is_R_or_C K] namespace is_R_or_C diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean index 6a0cf0a24bcbc..5ec996b4dfb0b 100644 --- a/src/data/nat/parity.lean +++ b/src/data/nat/parity.lean @@ -91,8 +91,6 @@ mod_two_add_add_odd_mod_two m odd_one @[simp] theorem succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1 := by rw [add_comm, mod_two_add_succ_mod_two] -mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`" - @[simp] theorem not_even_one : ¬ even 1 := by rw even_iff; norm_num diff --git a/src/data/prod/basic.lean b/src/data/prod/basic.lean index 240beda2eb6e2..a2a159aced62e 100644 --- a/src/data/prod/basic.lean +++ b/src/data/prod/basic.lean @@ -37,7 +37,9 @@ prod.exists @[simp] lemma fst_comp_mk (x : α) : prod.fst ∘ (prod.mk x : β → α × β) = function.const β x := rfl -@[simp] lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) : map f g (a, b) = (f a, g b) := rfl +@[simp, mfld_simps] lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) : + map f g (a, b) = (f a, g b) := +rfl lemma map_fst (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).1 = f (p.1) := rfl diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean index 08af3259a3f2e..9ac1590fab649 100644 --- a/src/data/set/basic.lean +++ b/src/data/set/basic.lean @@ -409,7 +409,7 @@ Mathematically it is the same as `α` but it has a different type. @[simp] theorem set_of_true : {x : α | true} = univ := rfl -@[simp] theorem mem_univ (x : α) : x ∈ @univ α := trivial +@[simp, mfld_simps] theorem mem_univ (x : α) : x ∈ @univ α := trivial @[simp] lemma univ_eq_empty_iff : (univ : set α) = ∅ ↔ is_empty α := eq_empty_iff_forall_not_mem.trans ⟨λ H, ⟨λ x, H x trivial⟩, λ H x _, @is_empty.false α H x⟩ @@ -541,7 +541,8 @@ by simp only [← subset_empty_iff]; exact union_subset_iff theorem inter_def {s₁ s₂ : set α} : s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂} := rfl -@[simp] theorem mem_inter_iff (x : α) (a b : set α) : x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) := iff.rfl +@[simp, mfld_simps] +theorem mem_inter_iff (x : α) (a b : set α) : x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) := iff.rfl theorem mem_inter {x : α} {a b : set α} (ha : x ∈ a) (hb : x ∈ b) : x ∈ a ∩ b := ⟨ha, hb⟩ @@ -569,7 +570,7 @@ ext $ λ x, and.left_comm theorem inter_right_comm (s₁ s₂ s₃ : set α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ := ext $ λ x, and.right_comm -@[simp] theorem inter_subset_left (s t : set α) : s ∩ t ⊆ s := λ x, and.left +@[simp, mfld_simps] theorem inter_subset_left (s t : set α) : s ∩ t ⊆ s := λ x, and.left @[simp] theorem inter_subset_right (s t : set α) : s ∩ t ⊆ t := λ x, and.right @@ -596,9 +597,9 @@ lemma inter_congr_right (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t lemma inter_eq_inter_iff_left : s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u := inf_eq_inf_iff_left lemma inter_eq_inter_iff_right : s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t := inf_eq_inf_iff_right -@[simp] theorem inter_univ (a : set α) : a ∩ univ = a := inf_top_eq +@[simp, mfld_simps] theorem inter_univ (a : set α) : a ∩ univ = a := inf_top_eq -@[simp] theorem univ_inter (a : set α) : univ ∩ a = a := top_inf_eq +@[simp, mfld_simps] theorem univ_inter (a : set α) : univ ∩ a = a := top_inf_eq theorem inter_subset_inter {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∩ s₂ ⊆ t₁ ∩ t₂ := λ x, and.imp (@h₁ _) (@h₂ _) diff --git a/src/data/set/image.lean b/src/data/set/image.lean index fba4f00b8d959..4e942d43a7266 100644 --- a/src/data/set/image.lean +++ b/src/data/set/image.lean @@ -50,7 +50,7 @@ variables {f : α → β} {g : β → γ} @[simp] theorem preimage_empty : f ⁻¹' ∅ = ∅ := rfl -@[simp] theorem mem_preimage {s : set β} {a : α} : (a ∈ f ⁻¹' s) ↔ (f a ∈ s) := iff.rfl +@[simp, mfld_simps] theorem mem_preimage {s : set β} {a : α} : (a ∈ f ⁻¹' s) ↔ (f a ∈ s) := iff.rfl lemma preimage_congr {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) : f ⁻¹' s = g ⁻¹' s := by { congr' with x, apply_assumption } @@ -58,11 +58,11 @@ by { congr' with x, apply_assumption } theorem preimage_mono {s t : set β} (h : s ⊆ t) : f ⁻¹' s ⊆ f ⁻¹' t := assume x hx, h hx -@[simp] theorem preimage_univ : f ⁻¹' univ = univ := rfl +@[simp, mfld_simps] theorem preimage_univ : f ⁻¹' univ = univ := rfl theorem subset_preimage_univ {s : set α} : s ⊆ f ⁻¹' univ := subset_univ _ -@[simp] theorem preimage_inter {s t : set β} : f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t := rfl +@[simp, mfld_simps] theorem preimage_inter {s t : set β} : f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t := rfl @[simp] theorem preimage_union {s t : set β} : f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t := rfl @@ -80,7 +80,7 @@ rfl @[simp] lemma preimage_id_eq : preimage (id : α → α) = id := rfl -theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl +@[mfld_simps] theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl @[simp] theorem preimage_id' {s : set α} : (λ x, x) ⁻¹' s = s := rfl @@ -152,6 +152,7 @@ theorem mem_image_iff_bex {f : α → β} {s : set α} {y : β} : lemma image_eta (f : α → β) : f '' s = (λ x, f x) '' s := rfl +@[mfld_simps] theorem mem_image_of_mem (f : α → β) {x : α} {a : set α} (h : x ∈ a) : f x ∈ f '' a := ⟨_, h, rfl⟩ @@ -252,7 +253,8 @@ by { ext, simp [image, eq_comm] } ext $ λ x, ⟨λ ⟨y, _, h⟩, h ▸ mem_singleton _, λ h, (eq_of_mem_singleton h).symm ▸ hs.imp (λ y hy, ⟨hy, rfl⟩)⟩ -@[simp] lemma image_eq_empty {α β} {f : α → β} {s : set α} : f '' s = ∅ ↔ s = ∅ := +@[simp, mfld_simps] +lemma image_eq_empty {α β} {f : α → β} {s : set α} : f '' s = ∅ ↔ s = ∅ := by { simp only [eq_empty_iff_forall_not_mem], exact ⟨λ H a ha, H _ ⟨_, ha, rfl⟩, λ H b ⟨_, ha, _⟩, H _ ha⟩ } @@ -506,7 +508,7 @@ def range (f : ι → α) : set α := {x | ∃y, f y = x} @[simp] theorem mem_range {x : α} : x ∈ range f ↔ ∃ y, f y = x := iff.rfl -@[simp] theorem mem_range_self (i : ι) : f i ∈ range f := ⟨i, rfl⟩ +@[simp, mfld_simps] theorem mem_range_self (i : ι) : f i ∈ range f := ⟨i, rfl⟩ theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i, p (f i)) := by simp @@ -649,7 +651,7 @@ theorem preimage_image_preimage {f : α → β} {s : set β} : f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s := by rw [image_preimage_eq_inter_range, preimage_inter_range] -@[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id +@[simp, mfld_simps] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id @[simp] theorem range_id' : range (λ (x : α), x) = univ := range_id diff --git a/src/data/set/prod.lean b/src/data/set/prod.lean index e6f35bb6ad86c..90f2736c294bc 100644 --- a/src/data/set/prod.lean +++ b/src/data/set/prod.lean @@ -42,9 +42,9 @@ lemma prod_eq (s : set α) (t : set β) : s ×ˢ t = prod.fst ⁻¹' s ∩ prod. lemma mem_prod_eq {p : α × β} : p ∈ s ×ˢ t = (p.1 ∈ s ∧ p.2 ∈ t) := rfl -@[simp] lemma mem_prod {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := iff.rfl +@[simp, mfld_simps] lemma mem_prod {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := iff.rfl -@[simp] lemma prod_mk_mem_set_prod_eq : (a, b) ∈ s ×ˢ t = (a ∈ s ∧ b ∈ t) := rfl +@[simp, mfld_simps] lemma prod_mk_mem_set_prod_eq : (a, b) ∈ s ×ˢ t = (a ∈ s ∧ b ∈ t) := rfl lemma mk_mem_prod (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t := ⟨ha, hb⟩ @@ -77,7 +77,7 @@ by simp [and_assoc] @[simp] lemma empty_prod : (∅ : set α) ×ˢ t = ∅ := by { ext, exact false_and _ } -@[simp] lemma univ_prod_univ : @univ α ×ˢ @univ β = univ := by { ext, exact true_and _ } +@[simp, mfld_simps] lemma univ_prod_univ : @univ α ×ˢ @univ β = univ := by { ext, exact true_and _ } lemma univ_prod {t : set β} : (univ : set α) ×ˢ t = prod.snd ⁻¹' t := by simp [prod_eq] @@ -103,6 +103,7 @@ by { ext ⟨x, y⟩, simp only [←and_and_distrib_right, mem_inter_iff, mem_pro lemma prod_inter : s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂ := by { ext ⟨x, y⟩, simp only [←and_and_distrib_left, mem_inter_iff, mem_prod] } +@[mfld_simps] lemma prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) := by { ext ⟨x, y⟩, simp [and_assoc, and.left_comm] } @@ -186,7 +187,7 @@ lemma prod_range_range_eq {m₁ : α → γ} {m₂ : β → δ} : (range m₁) ×ˢ (range m₂) = range (λ p : α × β, (m₁ p.1, m₂ p.2)) := ext $ by simp [range] -@[simp] lemma range_prod_map {m₁ : α → γ} {m₂ : β → δ} : +@[simp, mfld_simps] lemma range_prod_map {m₁ : α → γ} {m₂ : β → δ} : range (prod.map m₁ m₂) = (range m₁) ×ˢ (range m₂) := prod_range_range_eq.symm @@ -219,7 +220,6 @@ lemma prod_sub_preimage_iff {W : set γ} {f : α × β → γ} : s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W := by simp [subset_def] - lemma image_prod_mk_subset_prod {f : α → β} {g : α → γ} {s : set α} : (λ x, (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s) := by { rintros _ ⟨x, hx, rfl⟩, exact mk_mem_prod (mem_image_of_mem f hx) (mem_image_of_mem g hx) } diff --git a/src/data/subtype.lean b/src/data/subtype.lean index 5dd326422b4cb..10dc89a45d6f0 100644 --- a/src/data/subtype.lean +++ b/src/data/subtype.lean @@ -84,7 +84,7 @@ ext_iff @[simp] theorem coe_eta (a : {a // p a}) (h : p a) : mk ↑a h = a := subtype.ext rfl -@[simp] theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl +@[simp, mfld_simps] theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl @[simp, nolint simp_nf] -- built-in reduction doesn't always work theorem mk_eq_mk {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' := diff --git a/src/data/typevec.lean b/src/data/typevec.lean index 60416b60ebafb..55224d6e7ef0b 100644 --- a/src/data/typevec.lean +++ b/src/data/typevec.lean @@ -235,11 +235,6 @@ eq_of_drop_last_eq rfl rfl instance subsingleton0 : subsingleton (typevec 0) := ⟨ λ a b, funext $ λ a, fin2.elim0 a ⟩ -run_cmd do - mk_simp_attr `typevec, - tactic.add_doc_string `simp_attr.typevec -"simp set for the manipulation of typevec and arrow expressions" - local prefix `♯`:0 := cast (by try { simp }; congr' 1; try { simp }) /-- cases distinction for 0-length type vector -/ diff --git a/src/logic/basic.lean b/src/logic/basic.lean index e4b5d9cb3afe4..71baa00527e9d 100644 --- a/src/logic/basic.lean +++ b/src/logic/basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura -/ -import tactic.doc_commands +import tactic.mk_simp_attribute import tactic.reserved_notation /-! @@ -63,7 +63,7 @@ instance psum.inhabited_right {α β} [inhabited β] : inhabited (psum α β) := {α} [subsingleton α] : decidable_eq α | a b := is_true (subsingleton.elim a b) -@[simp] lemma eq_iff_true_of_subsingleton {α : Sort*} [subsingleton α] (x y : α) : +@[simp, nontriviality] lemma eq_iff_true_of_subsingleton {α : Sort*} [subsingleton α] (x y : α) : x = y ↔ true := by cc @@ -274,7 +274,7 @@ theorem imp_and_distrib {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) := ⟨λ h, ⟨λ ha, (h ha).left, λ ha, (h ha).right⟩, λ h ha, ⟨h.left ha, h.right ha⟩⟩ -@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := +@[simp, mfld_simps] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := iff.intro (λ h ha hb, h ⟨ha, hb⟩) (λ h ⟨ha, hb⟩, h ha hb) theorem iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a) := @@ -842,7 +842,7 @@ end mem section equality variables {α : Sort*} {a b : α} -@[simp] theorem heq_iff_eq : a == b ↔ a = b := +@[simp, mfld_simps] theorem heq_iff_eq : a == b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩ theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : hp == hq := @@ -865,12 +865,12 @@ theorem eq_equivalence : equivalence (@eq α) := ⟨eq.refl, @eq.symm _, @eq.trans _⟩ /-- Transport through trivial families is the identity. -/ -@[simp] +@[simp, transport_simps] lemma eq_rec_constant {α : Sort*} {a a' : α} {β : Sort*} (y : β) (h : a = a') : (@eq.rec α a (λ a, β) y a' h) = y := by { cases h, refl, } -@[simp] +@[simp, transport_simps] lemma eq_mp_eq_cast {α β : Sort*} (h : α = β) : eq.mp h = cast h := rfl @[simp] @@ -1096,6 +1096,7 @@ let ⟨a⟩ := ha in (λ hb, hb $ h $ λ x, (not_imp.1 (h' x)).1), λ ⟨x, hx⟩ h, hx (h x)⟩ -- TODO: duplicate of a lemma in core +@[mfld_simps] theorem forall_true_iff : (α → true) ↔ true := implies_true_iff α @@ -1118,7 +1119,7 @@ exists.elim h (λ x hx, ⟨x, and.left hx⟩) (∃! x, p x) ↔ ∃ x, p x := ⟨λ h, h.exists, Exists.imp $ λ x hx, ⟨hx, λ y _, subsingleton.elim y x⟩⟩ -@[simp] theorem forall_const (α : Sort*) [i : nonempty α] : (α → b) ↔ b := +@[simp, mfld_simps] theorem forall_const (α : Sort*) [i : nonempty α] : (α → b) ↔ b := ⟨i.elim, λ hb x, hb⟩ /-- For some reason simp doesn't use `forall_const` to simplify in this case. -/ diff --git a/src/logic/equiv/defs.lean b/src/logic/equiv/defs.lean index abb46c6753b6c..490c633c499db 100644 --- a/src/logic/equiv/defs.lean +++ b/src/logic/equiv/defs.lean @@ -120,10 +120,10 @@ initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply) @[trans] protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm, e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩ -@[simp] +@[simp, transport_simps, mfld_simps] lemma to_fun_as_coe (e : α ≃ β) : e.to_fun = e := rfl -@[simp] +@[simp, mfld_simps] lemma inv_fun_as_coe (e : α ≃ β) : e.inv_fun = e.symm := rfl protected theorem injective (e : α ≃ β) : injective e := equiv_like.injective e @@ -189,10 +189,11 @@ theorem refl_apply (x : α) : equiv.refl α x = x := rfl theorem trans_apply (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a) := rfl -@[simp] theorem apply_symm_apply (e : α ≃ β) (x : β) : e (e.symm x) = x := +@[simp, equiv_rw_simp] theorem apply_symm_apply (e : α ≃ β) (x : β) : e (e.symm x) = x := e.right_inv x -@[simp] theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x := +@[simp, equiv_rw_simp, transport_simps] +theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x := e.left_inv x @[simp] theorem symm_comp_self (e : α ≃ β) : e.symm ∘ e = id := funext e.symm_apply_apply @@ -208,6 +209,7 @@ e.left_inv x theorem apply_eq_iff_eq (f : α ≃ β) {x y : α} : f x = f y ↔ x = y := equiv_like.apply_eq_iff_eq f +@[transport_simps] theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) {x : α} {y : β} : f x = y ↔ x = f.symm y := begin @@ -234,7 +236,7 @@ lemma symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y := lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x := (eq_comm.trans e.symm_apply_eq).trans eq_comm -@[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl } +@[simp, equiv_rw_simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl } @[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by { cases e, refl } @@ -411,7 +413,7 @@ A version of `equiv.arrow_congr` in `Type`, rather than `Sort`. The `equiv_rw` tactic is not able to use the default `Sort` level `equiv.arrow_congr`, because Lean's universe rules will not unify `?l_1` with `imax (1 ?m_1)`. -/ -@[congr, simps apply] +@[congr, simps apply { attrs := [`simp, `transport_simps] }] def arrow_congr' {α₁ β₁ α₂ β₂ : Type*} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) := equiv.arrow_congr hα hβ @@ -638,7 +640,8 @@ def sigma_congr {α₁ α₂} {β₁ : α₁ → Sort*} {β₂ : α₂ → Sort* (sigma_congr_right F).trans (sigma_congr_left f) /-- `sigma` type with a constant fiber is equivalent to the product. -/ -@[simps apply symm_apply] def sigma_equiv_prod (α β : Type*) : (Σ_:α, β) ≃ α × β := +@[simps apply symm_apply { attrs := [`simp, `mfld_simps] }] +def sigma_equiv_prod (α β : Type*) : (Σ_:α, β) ≃ α × β := ⟨λ a, ⟨a.1, a.2⟩, λ a, ⟨a.1, a.2⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩ /-- If each fiber of a `sigma` type is equivalent to a fixed type, then the sigma type diff --git a/src/logic/equiv/local_equiv.lean b/src/logic/equiv/local_equiv.lean index 7b1c693559b8f..d86e01abfeddc 100644 --- a/src/logic/equiv/local_equiv.lean +++ b/src/logic/equiv/local_equiv.lean @@ -68,29 +68,6 @@ then it should use `e.source ∩ s` or `e.target ∩ t`, not `s ∩ e.source` or -/ -mk_simp_attribute mfld_simps "The simpset `mfld_simps` records several simp lemmas that are -especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it -possible to have quicker proofs (when used with `squeeze_simp` or `simp only`) while retaining -readability. - -The typical use case is the following, in a file on manifolds: -If `simp [foo, bar]` is slow, replace it with `squeeze_simp [foo, bar] with mfld_simps` and paste -its output. The list of lemmas should be reasonable (contrary to the output of -`squeeze_simp [foo, bar]` which might contain tens of lemmas), and the outcome should be quick -enough. -" - --- register in the simpset `mfld_simps` several lemmas that are often useful when dealing --- with manifolds -attribute [mfld_simps] id.def function.comp.left_id set.mem_set_of_eq set.image_eq_empty -set.univ_inter set.preimage_univ set.prod_mk_mem_set_prod_eq and_true set.mem_univ -set.mem_image_of_mem true_and set.mem_inter_iff set.mem_preimage function.comp_app -set.inter_subset_left set.mem_prod set.range_id set.range_prod_map and_self set.mem_range_self -eq_self_iff_true forall_const forall_true_iff set.inter_univ set.preimage_id function.comp.right_id -not_false_iff and_imp set.prod_inter_prod set.univ_prod_univ true_or or_true prod.map_mk -set.preimage_inter heq_iff_eq equiv.sigma_equiv_prod_apply equiv.sigma_equiv_prod_symm_apply -subtype.coe_mk equiv.to_fun_as_coe equiv.inv_fun_as_coe - /-- Common `@[simps]` configuration options used for manifold-related declarations. -/ def mfld_cfg : simps_cfg := {attrs := [`simp, `mfld_simps], fully_applied := ff} diff --git a/src/logic/nontrivial.lean b/src/logic/nontrivial.lean index 99388b9a6b5a1..14ad9c3c2116d 100644 --- a/src/logic/nontrivial.lean +++ b/src/logic/nontrivial.lean @@ -178,13 +178,10 @@ end pi instance function.nontrivial [h : nonempty α] [nontrivial β] : nontrivial (α → β) := h.elim $ λ a, pi.nontrivial_at a -mk_simp_attribute nontriviality "Simp lemmas for `nontriviality` tactic" - +@[nontriviality] protected lemma subsingleton.le [preorder α] [subsingleton α] (x y : α) : x ≤ y := le_of_eq (subsingleton.elim x y) -attribute [nontriviality] eq_iff_true_of_subsingleton subsingleton.le - namespace bool instance : nontrivial bool := ⟨⟨tt,ff, tt_eq_ff_eq_false⟩⟩ diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean index c594e1e066aed..84076d698e9b8 100644 --- a/src/measure_theory/integral/bochner.lean +++ b/src/measure_theory/integral/bochner.lean @@ -638,24 +638,28 @@ end variables {α E} +@[integral_simps] lemma integral_add (f g : α →₁[μ] E) : integral (f + g) = integral f + integral g := begin simp only [integral], exact map_add integral_clm f g end +@[integral_simps] lemma integral_neg (f : α →₁[μ] E) : integral (-f) = - integral f := begin simp only [integral], exact map_neg integral_clm f end +@[integral_simps] lemma integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - integral g := begin simp only [integral], exact map_sub integral_clm f g end +@[integral_simps] lemma integral_smul (c : 𝕜) (f : α →₁[μ] E) : integral (c • f) = c • integral f := begin simp only [integral], @@ -797,6 +801,7 @@ begin exact set_to_fun_finset_sum (dominated_fin_meas_additive_weighted_smul _) s hf end +@[integral_simps] lemma integral_neg (f : α → E) : ∫ a, -f a ∂μ = - ∫ a, f a ∂μ := begin simp only [integral, L1.integral], @@ -817,6 +822,7 @@ lemma integral_sub' (hf : integrable f μ) (hg : integrable g μ) : ∫ a, (f - g) a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ := integral_sub hf hg +@[integral_simps] lemma integral_smul (c : 𝕜) (f : α → E) : ∫ a, c • (f a) ∂μ = c • ∫ a, f a ∂μ := begin @@ -1664,11 +1670,6 @@ end end properties -mk_simp_attribute integral_simps "Simp set for integral rules." - -attribute [integral_simps] integral_neg integral_smul L1.integral_add L1.integral_sub - L1.integral_smul L1.integral_neg - section integral_trim variables {H β γ : Type*} [normed_add_comm_group H] diff --git a/src/ring_theory/witt_vector/is_poly.lean b/src/ring_theory/witt_vector/is_poly.lean index 5be39c921c856..f967401b8e131 100644 --- a/src/ring_theory/witt_vector/is_poly.lean +++ b/src/ring_theory/witt_vector/is_poly.lean @@ -100,9 +100,6 @@ end We define it here so it is a shared import. -/ -mk_simp_attribute ghost_simps -"Simplification rules for ghost equations" - namespace tactic namespace interactive setup_tactic_parser diff --git a/src/tactic/core.lean b/src/tactic/core.lean index 845f0254d8fc3..2364d7bd99a08 100644 --- a/src/tactic/core.lean +++ b/src/tactic/core.lean @@ -2409,38 +2409,6 @@ add_tactic_doc decl_names := [`tactic.import_private_cmd], tags := ["renaming"] } -/-- -The command `mk_simp_attribute simp_name "description"` creates a simp set with name `simp_name`. -Lemmas tagged with `@[simp_name]` will be included when `simp with simp_name` is called. -`mk_simp_attribute simp_name none` will use a default description. - -Appending the command with `with attr1 attr2 ...` will include all declarations tagged with -`attr1`, `attr2`, ... in the new simp set. - -This command is preferred to using ``run_cmd mk_simp_attr `simp_name`` since it adds a doc string -to the attribute that is defined. If you need to create a simp set in a file where this command is -not available, you should use -```lean -run_cmd mk_simp_attr `simp_name -run_cmd add_doc_string `simp_attr.simp_name "Description of the simp set here" -``` --/ -@[user_command] -meta def mk_simp_attribute_cmd (_ : parse $ tk "mk_simp_attribute") : lean.parser unit := -do n ← ident, - d ← parser.pexpr, - d ← to_expr ``(%%d : option string), - descr ← eval_expr (option string) d, - with_list ← (tk "with" *> many ident) <|> return [], - mk_simp_attr n with_list, - add_doc_string (name.append `simp_attr n) $ descr.get_or_else $ "simp set for " ++ to_string n - -add_tactic_doc -{ name := "mk_simp_attribute", - category := doc_category.cmd, - decl_names := [`tactic.mk_simp_attribute_cmd], - tags := ["simplification"] } - /-- Given a user attribute name `attr_name`, `get_user_attribute_name attr_name` returns the name of the declaration that defines this attribute. diff --git a/src/tactic/equiv_rw.lean b/src/tactic/equiv_rw.lean index 766703bf8924f..ca74919c3eecc 100644 --- a/src/tactic/equiv_rw.lean +++ b/src/tactic/equiv_rw.lean @@ -187,11 +187,6 @@ do -- to compress away some `map_equiv equiv.refl` subexpressions. prod.fst <$> new_eqv.simp {fail_if_unchanged := ff} -mk_simp_attribute equiv_rw_simp "The simpset `equiv_rw_simp` is used by the tactic `equiv_rw` to -simplify applications of equivalences and their inverses." - -attribute [equiv_rw_simp] equiv.symm_symm equiv.apply_symm_apply equiv.symm_apply_apply - /-- Attempt to replace the hypothesis with name `x` by transporting it along the equivalence in `e : α ≃ β`. diff --git a/src/tactic/mk_simp_attribute.lean b/src/tactic/mk_simp_attribute.lean new file mode 100644 index 0000000000000..2422f9675391a --- /dev/null +++ b/src/tactic/mk_simp_attribute.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2019 Rob Lewis All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rob Lewis +-/ +import tactic.doc_commands +/-! +# User command to register `simp` attributes + +In this file we define a command `mk_simp_attribute` that can be used to register `simp` sets. We +also define all `simp` attributes that are used in the library and tag lemmas from Lean core with +these attributes. +-/ + +/-! +### User command +-/ + +section cmd + +open interactive lean lean.parser + +namespace tactic + +/-- +The command `mk_simp_attribute simp_name "description"` creates a simp set with name `simp_name`. +Lemmas tagged with `@[simp_name]` will be included when `simp with simp_name` is called. +`mk_simp_attribute simp_name none` will use a default description. + +Appending the command with `with attr1 attr2 ...` will include all declarations tagged with +`attr1`, `attr2`, ... in the new simp set. + +This command is preferred to using ``run_cmd mk_simp_attr `simp_name`` since it adds a doc string +to the attribute that is defined. If you need to create a simp set in a file where this command is +not available, you should use +```lean +run_cmd mk_simp_attr `simp_name +run_cmd add_doc_string `simp_attr.simp_name "Description of the simp set here" +``` +-/ +@[user_command] +meta def mk_simp_attribute_cmd (_ : parse $ tk "mk_simp_attribute") : lean.parser unit := +do n ← ident, + d ← parser.pexpr, + d ← to_expr ``(%%d : option string), + descr ← eval_expr (option string) d, + with_list ← (tk "with" *> many ident) <|> return [], + mk_simp_attr n with_list, + add_doc_string (name.append `simp_attr n) $ descr.get_or_else $ "simp set for " ++ to_string n + +add_tactic_doc +{ name := "mk_simp_attribute", + category := doc_category.cmd, + decl_names := [`tactic.mk_simp_attribute_cmd], + tags := ["simplification"] } + +end tactic + +end cmd + +/-! +### Attributes +-/ + +mk_simp_attribute equiv_rw_simp "The simpset `equiv_rw_simp` is used by the tactic `equiv_rw` to +simplify applications of equivalences and their inverses." + +mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to +reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are +division-free." + +mk_simp_attribute functor_norm "Simp set for functor_norm" + +attribute [functor_norm] bind_assoc pure_bind bind_pure + +mk_simp_attribute ghost_simps "Simplification rules for ghost equations" + +mk_simp_attribute integral_simps "Simp set for integral rules." + +mk_simp_attribute is_R_or_C_simps "Simp attribute for lemmas about `is_R_or_C`" + +mk_simp_attribute mfld_simps "The simpset `mfld_simps` records several simp lemmas that are +especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it +possible to have quicker proofs (when used with `squeeze_simp` or `simp only`) while retaining +readability. + +The typical use case is the following, in a file on manifolds: +If `simp [foo, bar]` is slow, replace it with `squeeze_simp [foo, bar] with mfld_simps` and paste +its output. The list of lemmas should be reasonable (contrary to the output of +`squeeze_simp [foo, bar]` which might contain tens of lemmas), and the outcome should be quick +enough. +" + +attribute [mfld_simps] id.def function.comp.left_id set.mem_set_of_eq and_true true_and + function.comp_app and_self eq_self_iff_true function.comp.right_id not_false_iff true_or or_true + +mk_simp_attribute monad_norm none with functor_norm + +mk_simp_attribute nontriviality "Simp lemmas for `nontriviality` tactic" + +mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`" + +mk_simp_attribute push_cast "The `push_cast` simp attribute uses `norm_cast` lemmas +to move casts toward the leaf nodes of the expression." + +mk_simp_attribute split_if_reduction + "Simp set for if-then-else statements, used in the `split_ifs` tactic" + +attribute [split_if_reduction] if_pos if_neg dif_pos dif_neg if_congr + +mk_simp_attribute transport_simps +"The simpset `transport_simps` is used by the tactic `transport` +to simplify certain expressions involving application of equivalences, +and trivial `eq.rec` or `ep.mpr` conversions. +It's probably best not to adjust it without understanding the algorithm used by `transport`." + +attribute [transport_simps] cast_eq + +mk_simp_attribute typevec "simp set for the manipulation of typevec and arrow expressions" diff --git a/src/tactic/norm_cast.lean b/src/tactic/norm_cast.lean index dd64e04597622..b0c4fdc0f9409 100644 --- a/src/tactic/norm_cast.lean +++ b/src/tactic/norm_cast.lean @@ -61,9 +61,6 @@ when_tracing `norm_cast $ do a ← pp a, trace ("[norm_cast] " ++ msg ++ a : format) -mk_simp_attribute push_cast "The `push_cast` simp attribute uses `norm_cast` lemmas -to move casts toward the leaf nodes of the expression." - /-- `label` is a type used to classify `norm_cast` lemmas. * elim lemma: LHS has 0 head coes and ≥ 1 internal coe diff --git a/src/tactic/split_ifs.lean b/src/tactic/split_ifs.lean index dd06561183e13..e96604ceea6a0 100644 --- a/src/tactic/split_ifs.lean +++ b/src/tactic/split_ifs.lean @@ -27,11 +27,6 @@ lctx ← at_.get_locals, lctx ← lctx.mmap infer_type, tgt ← target, let es := if at_.include_goal then tgt::lctx else lctx, return $ find_if_cond $ es.foldr app default -run_cmd mk_simp_attr `split_if_reduction -run_cmd add_doc_string `simp_attr.split_if_reduction "Simp set for if-then-else statements" - -attribute [split_if_reduction] if_pos if_neg dif_pos dif_neg if_congr - meta def reduce_ifs_at (at_ : loc) : tactic unit := do sls ← get_user_simp_lemmas `split_if_reduction, let cfg : simp_config := { fail_if_unchanged := ff }, diff --git a/src/tactic/transport.lean b/src/tactic/transport.lean index 2e7ec3dc4a02d..53bdde01db08e 100644 --- a/src/tactic/transport.lean +++ b/src/tactic/transport.lean @@ -19,23 +19,6 @@ to a `monoid β`, the new multiplication is definitionally `λ x y, e (e.symm a namespace tactic open tactic.interactive -mk_simp_attribute transport_simps -"The simpset `transport_simps` is used by the tactic `transport` -to simplify certain expressions involving application of equivalences, -and trivial `eq.rec` or `ep.mpr` conversions. -It's probably best not to adjust it without understanding the algorithm used by `transport`." - -attribute [transport_simps] - eq_rec_constant - eq_mp_eq_cast - cast_eq - equiv.to_fun_as_coe - equiv.arrow_congr'_apply - equiv.symm_apply_apply - -- we use `apply_eq_iff_eq_symm_apply` rather than `apply_eq_iff_eq`, - -- as many axioms have a constant on the right-hand-side - equiv.apply_eq_iff_eq_symm_apply - /-- Given `s : S α` for some structure `S` depending on a type `α`, and an equivalence `e : α ≃ β`, diff --git a/test/equiv_rw.lean b/test/equiv_rw.lean index a39015992dc92..ae548862f1509 100644 --- a/test/equiv_rw.lean +++ b/test/equiv_rw.lean @@ -276,9 +276,9 @@ end -- The constructions and proofs here are written as uniformly as possible. -- This example is the blueprint for the `transport` tactic. -mk_simp_attribute transport_simps "simps useful inside `transport`" +mk_simp_attribute transport_simps' "simps useful inside `transport`" -attribute [transport_simps] +attribute [transport_simps'] eq_rec_constant cast_eq equiv.to_fun_as_coe @@ -291,7 +291,7 @@ begin refine_struct { .. }, { have mul := S.mul, equiv_rw e at mul, exact mul, }, { try { unfold_projs }, - simp only with transport_simps, + simp only with transport_simps', have mul_assoc := S.mul_assoc, equiv_rw e at mul_assoc, solve_by_elim, }, From d0b1936853671209a866fa35b9e54949c81116e2 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Fri, 30 Jun 2023 15:09:19 +0000 Subject: [PATCH 16/16] chore(*): add mathlib4 synchronization comments (#19220) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.fgModule.limits` * `algebra.homology.differential_object` * `algebraic_geometry.AffineScheme` * `algebraic_geometry.gluing` * `algebraic_geometry.limits` * `algebraic_geometry.properties` * `algebraic_geometry.pullbacks` * `linear_algebra.clifford_algebra.even` * `number_theory.legendre_symbol.norm_num` * `number_theory.zeta_function` * `order.category.omega_complete_partial_order` * `ring_theory.witt_vector.frobenius_fraction_field` * `set_theory.game.nim` * `set_theory.surreal.dyadic` * `topology.sheaves.skyscraper` --- src/algebra/category/fgModule/limits.lean | 3 +++ src/algebra/homology/differential_object.lean | 3 +++ src/algebraic_geometry/AffineScheme.lean | 3 +++ src/algebraic_geometry/gluing.lean | 3 +++ src/algebraic_geometry/limits.lean | 3 +++ src/algebraic_geometry/properties.lean | 3 +++ src/algebraic_geometry/pullbacks.lean | 3 +++ src/linear_algebra/clifford_algebra/even.lean | 3 +++ src/number_theory/legendre_symbol/norm_num.lean | 3 +++ src/number_theory/zeta_function.lean | 3 +++ src/order/category/omega_complete_partial_order.lean | 3 +++ src/ring_theory/witt_vector/frobenius_fraction_field.lean | 3 +++ src/set_theory/game/nim.lean | 3 +++ src/set_theory/surreal/dyadic.lean | 3 +++ src/topology/sheaves/skyscraper.lean | 3 +++ 15 files changed, 45 insertions(+) diff --git a/src/algebra/category/fgModule/limits.lean b/src/algebra/category/fgModule/limits.lean index f4c114b7dccdb..6c02caa86c100 100644 --- a/src/algebra/category/fgModule/limits.lean +++ b/src/algebra/category/fgModule/limits.lean @@ -14,6 +14,9 @@ import category_theory.limits.constructions.limits_of_products_and_equalizers /-! # `forget₂ (fgModule K) (Module K)` creates all finite limits. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + And hence `fgModule K` has all finite limits. ## Future work diff --git a/src/algebra/homology/differential_object.lean b/src/algebra/homology/differential_object.lean index 12a6920cb0ba9..03f8f3839d349 100644 --- a/src/algebra/homology/differential_object.lean +++ b/src/algebra/homology/differential_object.lean @@ -9,6 +9,9 @@ import category_theory.differential_object /-! # Homological complexes are differential graded objects. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We verify that a `homological_complex` indexed by an `add_comm_group` is essentially the same thing as a differential graded object. diff --git a/src/algebraic_geometry/AffineScheme.lean b/src/algebraic_geometry/AffineScheme.lean index 4def63a940a0a..827f2d0f8852b 100644 --- a/src/algebraic_geometry/AffineScheme.lean +++ b/src/algebraic_geometry/AffineScheme.lean @@ -11,6 +11,9 @@ import ring_theory.localization.inv_submonoid /-! # Affine schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the category of `AffineScheme`s as the essential image of `Spec`. We also define predicates about affine schemes and affine open sets. diff --git a/src/algebraic_geometry/gluing.lean b/src/algebraic_geometry/gluing.lean index 2a5345bbf6a65..15c3b25257934 100644 --- a/src/algebraic_geometry/gluing.lean +++ b/src/algebraic_geometry/gluing.lean @@ -9,6 +9,9 @@ import algebraic_geometry.open_immersion.Scheme /-! # Gluing Schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Given a family of gluing data of schemes, we may glue them together. ## Main definitions diff --git a/src/algebraic_geometry/limits.lean b/src/algebraic_geometry/limits.lean index 6268fba92246e..22c9fbc92cf7f 100644 --- a/src/algebraic_geometry/limits.lean +++ b/src/algebraic_geometry/limits.lean @@ -9,6 +9,9 @@ import algebraic_geometry.AffineScheme /-! # (Co)Limits of Schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We construct various limits and colimits in the category of schemes. * The existence of fibred products was shown in `algebraic_geometry/pullbacks.lean`. diff --git a/src/algebraic_geometry/properties.lean b/src/algebraic_geometry/properties.lean index 62429e066242e..7dbae1c65bc70 100644 --- a/src/algebraic_geometry/properties.lean +++ b/src/algebraic_geometry/properties.lean @@ -12,6 +12,9 @@ import ring_theory.local_properties /-! # Basic properties of schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We provide some basic properties of schemes ## Main definition diff --git a/src/algebraic_geometry/pullbacks.lean b/src/algebraic_geometry/pullbacks.lean index 726ffd94eed13..5173a80bbca4d 100644 --- a/src/algebraic_geometry/pullbacks.lean +++ b/src/algebraic_geometry/pullbacks.lean @@ -11,6 +11,9 @@ import category_theory.limits.shapes.diagonal /-! # Fibred products of schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we construct the fibred product of schemes via gluing. We roughly follow [har77] Theorem 3.3. diff --git a/src/linear_algebra/clifford_algebra/even.lean b/src/linear_algebra/clifford_algebra/even.lean index e977571460879..a374a0ead8693 100644 --- a/src/linear_algebra/clifford_algebra/even.lean +++ b/src/linear_algebra/clifford_algebra/even.lean @@ -9,6 +9,9 @@ import linear_algebra.clifford_algebra.grading /-! # The universal property of the even subalgebra +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions * `clifford_algebra.even Q`: The even subalgebra of `clifford_algebra Q`. diff --git a/src/number_theory/legendre_symbol/norm_num.lean b/src/number_theory/legendre_symbol/norm_num.lean index 00cfe5eb881ff..a47ded8453ec7 100644 --- a/src/number_theory/legendre_symbol/norm_num.lean +++ b/src/number_theory/legendre_symbol/norm_num.lean @@ -8,6 +8,9 @@ import number_theory.legendre_symbol.jacobi_symbol /-! # A `norm_num` extension for Jacobi and Legendre symbols +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We extend the `tactic.interactive.norm_num` tactic so that it can be used to provably compute the value of the Jacobi symbol `J(a | b)` or the Legendre symbol `legendre_sym p a` when the arguments are numerals. diff --git a/src/number_theory/zeta_function.lean b/src/number_theory/zeta_function.lean index b3dc94155d253..cda925a279f9f 100644 --- a/src/number_theory/zeta_function.lean +++ b/src/number_theory/zeta_function.lean @@ -10,6 +10,9 @@ import number_theory.zeta_values /-! # Definition of the Riemann zeta function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions: * `riemann_zeta`: the Riemann zeta function `ζ : ℂ → ℂ`. diff --git a/src/order/category/omega_complete_partial_order.lean b/src/order/category/omega_complete_partial_order.lean index 65d74186c9172..15b627c09c367 100644 --- a/src/order/category/omega_complete_partial_order.lean +++ b/src/order/category/omega_complete_partial_order.lean @@ -13,6 +13,9 @@ import category_theory.concrete_category.bundled_hom /-! # Category of types with a omega complete partial order +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we bundle the class `omega_complete_partial_order` into a concrete category and prove that continuous functions also form a `omega_complete_partial_order`. diff --git a/src/ring_theory/witt_vector/frobenius_fraction_field.lean b/src/ring_theory/witt_vector/frobenius_fraction_field.lean index d251d81d5ad0b..e9cd65c73af4f 100644 --- a/src/ring_theory/witt_vector/frobenius_fraction_field.lean +++ b/src/ring_theory/witt_vector/frobenius_fraction_field.lean @@ -10,6 +10,9 @@ import ring_theory.witt_vector.discrete_valuation_ring /-! # Solving equations about the Frobenius map on the field of fractions of `𝕎 k` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The goal of this file is to prove `witt_vector.exists_frobenius_solution_fraction_ring`, which says that for an algebraically closed field `k` of characteristic `p` and `a, b` in the field of fractions of Witt vectors over `k`, diff --git a/src/set_theory/game/nim.lean b/src/set_theory/game/nim.lean index fbbbb91d3abbd..93d6b3f894ccd 100644 --- a/src/set_theory/game/nim.lean +++ b/src/set_theory/game/nim.lean @@ -10,6 +10,9 @@ import set_theory.game.impartial /-! # Nim and the Sprague-Grundy theorem +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains the definition for nim for any ordinal `o`. In the game of `nim o₁` both players may move to `nim o₂` for any `o₂ < o₁`. We also define a Grundy value for an impartial game `G` and prove the Sprague-Grundy theorem, that diff --git a/src/set_theory/surreal/dyadic.lean b/src/set_theory/surreal/dyadic.lean index e663ebaecd75e..0f666a31e2705 100644 --- a/src/set_theory/surreal/dyadic.lean +++ b/src/set_theory/surreal/dyadic.lean @@ -10,6 +10,9 @@ import ring_theory.localization.basic /-! # Dyadic numbers + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category of rings with no 2-torsion. diff --git a/src/topology/sheaves/skyscraper.lean b/src/topology/sheaves/skyscraper.lean index c02f854b23030..08b19fe467af6 100644 --- a/src/topology/sheaves/skyscraper.lean +++ b/src/topology/sheaves/skyscraper.lean @@ -10,6 +10,9 @@ import topology.sheaves.functors /-! # Skyscraper (pre)sheaves +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + A skyscraper (pre)sheaf `𝓕 : (pre)sheaf C X` is the (pre)sheaf with value `A` at point `p₀` that is supported only at open sets contain `p₀`, i.e. `𝓕(U) = A` if `p₀ ∈ U` and `𝓕(U) = *` if `p₀ ∉ U` where `*` is a terminal object of `C`. In terms of stalks, `𝓕` is supported at all specializations