Merge branch 'master' into YK-cont-alternating

leanprover-community · Jul 2, 2023 · 991d1b5 · 991d1b5
2 parents 0d4a886 + d0b1936
commit 991d1b5
Show file tree

Hide file tree

Showing 187 changed files with 1,608 additions and 210 deletions.
diff --git 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/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/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/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
@@ -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/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/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/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
@@ -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/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/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/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
@@ -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/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/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/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
@@ -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/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/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/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
@@ -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/manifold.lean 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/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
@@ -9,18 +9,20 @@ 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
 
+> 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.
 -/
 
 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 +60,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/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`),