Merge master into nightly-testing

Mathlib/Algebra/Algebra/Pi.lean

@@ -79,6 +79,16 @@ def evalAlgHom {_ : CommSemiring R} [∀ i, Semiring (f i)] [∀ i, Algebra R (f
     toFun := fun f => f i
     commutes' := fun _ => rfl }
 
+@[simp]
+theorem algHom_evalAlgHom [CommSemiring R] [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] :
+    algHom R f (evalAlgHom R f) = AlgHom.id R (Π i, f i) := rfl
+
+/-- `Pi.algHom` commutes with composition. -/
+theorem algHom_comp [CommSemiring R] [∀ i, Semiring (f i)] [∀ i, Algebra R (f i)]
+    {A B : Type*} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
+    (g : ∀ i, B →ₐ[R] f i) (h : A →ₐ[R] B) :
+    (algHom R f g).comp h = algHom R f (fun i ↦ (g i).comp h) := rfl
+
 variable (A B : Type*) [CommSemiring R] [Semiring B] [Algebra R B]
 
 /-- `Function.const` as an `AlgHom`. The name matches `Pi.constRingHom`, `Pi.constMonoidHom`,

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
 import Mathlib.Algebra.Algebra.Pi
+import Mathlib.Algebra.Algebra.Prod
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.MonoidAlgebra.Basic
@@ -368,6 +369,38 @@ theorem aeval_algebraMap_apply_eq_algebraMap_eval (x : R) (p : R[X]) :
     aeval (algebraMap R A x) p = algebraMap R A (p.eval x) :=
   aeval_algHom_apply (Algebra.ofId R A) x p
 
+/-- Polynomial evaluation on a pair is a product of the evaluations on the components. -/
+theorem aeval_prod (x : A × B) : aeval (R := R) x = (aeval x.1).prod (aeval x.2) :=
+  aeval_algHom (.fst R A B) x ▸ aeval_algHom (.snd R A B) x ▸
+    (aeval x).prod_comp (.fst R A B) (.snd R A B)
+
+/-- Polynomial evaluation on a pair is a pair of evaluations. -/
+theorem aeval_prod_apply (x : A × B) (p : Polynomial R) :
+    p.aeval x = (p.aeval x.1, p.aeval x.2) := by simp [aeval_prod]
+
+section Pi
+
+variable {I : Type*} {A : I → Type*} [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)]
+variable (x : Π i, A i) (p : R[X])
+
+/-- Polynomial evaluation on an indexed tuple is the indexed product of the evaluations
+on the components.
+Generalizes `Polynomial.aeval_prod` to indexed products. -/
+theorem aeval_pi (x : Π i, A i) : aeval (R := R) x = Pi.algHom R A (fun i ↦ aeval (x i)) :=
+  (funext fun i ↦ aeval_algHom (Pi.evalAlgHom R A i) x) ▸
+    (Pi.algHom_comp R A (Pi.evalAlgHom R A) (aeval x))
+
+theorem aeval_pi_apply₂ (j : I) : p.aeval x j = p.aeval (x j) :=
+  aeval_pi (R := R) x ▸ Pi.algHom_apply R A (fun i ↦ aeval (x i)) p j
+
+/-- Polynomial evaluation on an indexed tuple is the indexed tuple of the evaluations
+on the components.
+Generalizes `Polynomial.aeval_prod_apply` to indexed products. -/
+theorem aeval_pi_apply : p.aeval x = fun j ↦ p.aeval (x j) :=
+  funext fun j ↦ aeval_pi_apply₂ x p j
+
+end Pi
+
 @[simp]
 theorem coe_aeval_eq_eval (r : R) : (aeval r : R[X] → R) = eval r :=
   rfl

Mathlib/AlgebraicGeometry/Noetherian.lean

@@ -191,9 +191,8 @@ lemma noetherianSpace_of_isAffineOpen (U : X.Opens) (hU : IsAffineOpen U)
     (Scheme.restrictFunctorΓ.app (op U)).symm.commRingCatIsoToRingEquiv
   exact @noetherianSpace_of_isAffine _ hU _
 
-/-- Any open immersion `Z ⟶ X` with `X` locally Noetherian is quasi-compact.
-
-[Stacks: Lemma 01OX](https://stacks.math.columbia.edu/tag/01OX) -/
+/-- Any open immersion `Z ⟶ X` with `X` locally Noetherian is quasi-compact. -/
+@[stacks 01OX]
 instance (priority := 100) {Z : Scheme} [IsLocallyNoetherian X]
     {f : Z ⟶ X} [IsOpenImmersion f] : QuasiCompact f := by
   apply (quasiCompact_iff_forall_affine f).mpr
@@ -206,9 +205,8 @@ instance (priority := 100) {Z : Scheme} [IsLocallyNoetherian X]
     · exact Set.inter_subset_left
   · exact Set.inter_subset_right
 
-/-- A locally Noetherian scheme is quasi-separated.
-
-[Stacks: Lemma 01OY](https://stacks.math.columbia.edu/tag/01OY) -/
+/-- A locally Noetherian scheme is quasi-separated. -/
+@[stacks 01OY]
 instance (priority := 100) IsLocallyNoetherian.quasiSeparatedSpace [IsLocallyNoetherian X] :
     QuasiSeparatedSpace X := by
   apply (quasiSeparatedSpace_iff_affine X).mpr
@@ -266,9 +264,8 @@ theorem isNoetherian_iff_of_finite_affine_openCover {𝒰 : Scheme.OpenCover.{v,
     · exact Scheme.OpenCover.compactSpace 𝒰
 
 open CategoryTheory in
-/-- A Noetherian scheme has a Noetherian underlying topological space.
-
-[Stacks, Lemma 01OZ](https://stacks.math.columbia.edu/tag/01OZ) -/
+/-- A Noetherian scheme has a Noetherian underlying topological space. -/
+@[stacks 01OZ]
 instance (priority := 100) IsNoetherian.noetherianSpace [IsNoetherian X] :
     NoetherianSpace X := by
   apply TopologicalSpace.noetherian_univ_iff.mp
@@ -284,9 +281,8 @@ instance (priority := 100) IsNoetherian.noetherianSpace [IsNoetherian X] :
   convert noetherianSpace_of_isAffineOpen U.1 U.2
   apply IsLocallyNoetherian.component_noetherian
 
-/-- Any morphism of schemes `f : X ⟶ Y` with `X` Noetherian is quasi-compact.
-
-[Stacks, Lemma 01P0](https://stacks.math.columbia.edu/tag/01P0) -/
+/-- Any morphism of schemes `f : X ⟶ Y` with `X` Noetherian is quasi-compact. -/
+@[stacks 01P0]
 instance (priority := 100) quasiCompact_of_noetherianSpace_source {X Y : Scheme}
     [NoetherianSpace X] (f : X ⟶ Y) : QuasiCompact f :=
   ⟨fun _ _ _ => NoetherianSpace.isCompact _⟩
@@ -325,9 +321,8 @@ theorem isNoetherian_Spec {R : CommRingCat} :
   ⟨fun _ => inferInstance,
    fun _ => inferInstance⟩
 
-/-- A Noetherian scheme has a finite number of irreducible components.
-
-[Stacks, Lemma 0BA8](https://stacks.math.columbia.edu/tag/0BA8) -/
+/-- A Noetherian scheme has a finite number of irreducible components. -/
+@[stacks 0BA8]
 theorem finite_irreducibleComponents_of_isNoetherian [IsNoetherian X] :
     (irreducibleComponents X).Finite := NoetherianSpace.finite_irreducibleComponents
 

Mathlib/Analysis/Asymptotics/TVS.lean

@@ -193,6 +193,17 @@ lemma IsLittleOTVS.insert [TopologicalSpace α] {x : α} {s : Set α}
 lemma IsLittleOTVS.bot : f =o[𝕜;⊥] g :=
   fun u hU => ⟨univ, by simp⟩
 
+theorem IsLittleOTVS.add [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
+    {f₁ f₂ : α → E} {g : α → F} {l : Filter α}
+    (h₁ : f₁ =o[𝕜; l] g) (h₂ : f₂ =o[𝕜; l] g) : (f₁ + f₂) =o[𝕜; l] g := by
+  rw [(nhds_basis_balanced 𝕜 E).add_self.isLittleOTVS_iff (basis_sets _)]
+  rintro U ⟨hU, hUb⟩
+  rcases ((h₁.eventually_smallSets U hU).and (h₂.eventually_smallSets U hU)).exists_mem_of_smallSets
+    with ⟨V, hV, hVf₁, hVf₂⟩
+  refine ⟨V, hV, fun ε hε ↦ ?_⟩
+  filter_upwards [hVf₁ ε hε, hVf₂ ε hε] with x hx₁ hx₂
+  exact (egauge_add_add_le hUb hUb _ _).trans (max_le hx₁ hx₂)
+
 protected lemma IsLittleOTVS.smul_left (h : f =o[𝕜;l] g) (c : α → 𝕜) :
     (fun x ↦ c x • f x) =o[𝕜;l] (fun x ↦ c x • g x) := by
   unfold IsLittleOTVS at *

Mathlib/Analysis/Convex/EGauge.lean

@@ -67,7 +67,7 @@ lemma egauge_union (s t : Set E) (x : E) : egauge 𝕜 (s ∪ t) x = egauge 𝕜
 
 lemma le_egauge_inter (s t : Set E) (x : E) :
     egauge 𝕜 s x ⊔ egauge 𝕜 t x ≤ egauge 𝕜 (s ∩ t) x :=
-  max_le_iff.2 ⟨egauge_anti _ inter_subset_left _, egauge_anti _ inter_subset_right _⟩
+  max_le (egauge_anti _ inter_subset_left _) (egauge_anti _ inter_subset_right _)
 
 end SMul
 
@@ -168,6 +168,23 @@ lemma egauge_smul_right (h : c = 0 → s.Nonempty) (x : E) :
 
 end Module
 
+section VectorSpace
+
+variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+
+theorem egauge_add_add_le {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) :
+    egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b) := by
+  refine le_of_forall_lt' fun c hc ↦ ?_
+  simp only [max_lt_iff, egauge_lt_iff] at hc ⊢
+  rcases hc with ⟨⟨x, hx, hxc⟩, ⟨y, hy, hyc⟩⟩
+  wlog hxy : ‖x‖ ≤ ‖y‖ generalizing a b x y U V
+  · simpa only [add_comm] using this hV hU b a y hy hyc x hx hxc (le_of_not_le hxy)
+  refine ⟨y, ?_, hyc⟩
+  rw [smul_add]
+  exact add_mem_add (hU.smul_mono hxy hx) hy
+
+end VectorSpace
+
 section SeminormedAddCommGroup
 
 variable (𝕜 : Type*) [NormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

Mathlib/CategoryTheory/Galois/Topology.lean

@@ -17,7 +17,7 @@ embedding of `Aut F` into `∀ X, Aut (F.obj X)` where
 
 ## References
 
-- Stacks Project: Tag 0BMQ
+- [Stacks 0BMQ](https://stacks.math.columbia.edu/tag/0BMQ)
 
 -/
 

Mathlib/CategoryTheory/Limits/Final.lean

@@ -335,11 +335,8 @@ section
 variable (G)
 
 /-- When `F : C ⥤ D` is final, and `G : D ⥤ E` has a colimit, then `F ⋙ G` has a colimit also and
-`colimit (F ⋙ G) ≅ colimit G`
-
-https://stacks.math.columbia.edu/tag/04E7
--/
-@[simps! (config := .lemmasOnly)]
+`colimit (F ⋙ G) ≅ colimit G`. -/
+@[simps! (config := .lemmasOnly), stacks 04E7]
 def colimitIso [HasColimit G] : colimit (F ⋙ G) ≅ colimit G :=
   asIso (colimit.pre G F)
 
@@ -684,11 +681,8 @@ section
 variable (G)
 
 /-- When `F : C ⥤ D` is initial, and `G : D ⥤ E` has a limit, then `F ⋙ G` has a limit also and
-`limit (F ⋙ G) ≅ limit G`
-
-https://stacks.math.columbia.edu/tag/04E7
--/
-@[simps! (config := .lemmasOnly)]
+`limit (F ⋙ G) ≅ limit G`. -/
+@[simps! (config := .lemmasOnly), stacks 04E7]
 def limitIso [HasLimit G] : limit (F ⋙ G) ≅ limit G :=
   (asIso (limit.pre G F)).symm
 

Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

@@ -219,9 +219,7 @@ instance sequentialFunctor_initial : (sequentialFunctor J).Initial where
     · right
       exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
 
-/--
-This is proved in https://stacks.math.columbia.edu/tag/0032
--/
+@[stacks 0032]
 proof_wanted preorder_of_cofiltered (J : Type*) [Category J] [IsCofiltered J] :
     ∃ (I : Type*) (_ : Preorder I) (_ : IsCofiltered I) (F : I ⥤ J), F.Initial
 

Mathlib/CategoryTheory/Sites/Canonical.lean

@@ -139,11 +139,9 @@ theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type v) (R S : Sieve X)
     rw [this]
     apply hR' hf
 
-/-- Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf.
-
-This is a special case of https://stacks.math.columbia.edu/tag/00Z9, but following a different
-proof (see the comments there).
--/
+/-- Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf. -/
+@[stacks 00Z9 "This is a special case of the Stacks entry, but following a different
+proof (see the Stacks comments)."]
 def finestTopologySingle (P : Cᵒᵖ ⥤ Type v) : GrothendieckTopology C where
   sieves X S := ∀ (Y) (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f : Presieve Y)
   top_mem' X Y f := by
@@ -164,11 +162,9 @@ def finestTopologySingle (P : Cᵒᵖ ⥤ Type v) : GrothendieckTopology C where
       rw [pullback_id, pullback_comp] at this
       apply this
 
-/--
-Construct the finest (largest) Grothendieck topology for which all the given presheaves are sheaves.
-
-This is equal to the construction of <https://stacks.math.columbia.edu/tag/00Z9>.
--/
+/-- Construct the finest (largest) Grothendieck topology for which all the given presheaves are
+sheaves. -/
+@[stacks 00Z9 "Equal to that Stacks construction"]
 def finestTopology (Ps : Set (Cᵒᵖ ⥤ Type v)) : GrothendieckTopology C :=
   sInf (finestTopologySingle '' Ps)
 

Mathlib/CategoryTheory/Sites/CoverLifting.lean

@@ -211,11 +211,9 @@ variable [∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F]
 
 /-- If `G` is cocontinuous, then `G.op.ran` pushes sheaves to sheaves.
 
-This is SGA 4 III 2.2. An alternative reference is
-https://stacks.math.columbia.edu/tag/00XK (where results
-are obtained under the additional assumption that
-`C` and `D` have pullbacks).
--/
+This is SGA 4 III 2.2. -/
+@[stacks 00XK "Alternative reference. There, results are obtained under the additional assumption
+that `C` and `D` have pullbacks."]
 theorem ran_isSheaf_of_isCocontinuous (ℱ : Sheaf J A) :
     Presheaf.IsSheaf K (G.op.ran.obj ℱ.val) := by
   rw [Presheaf.isSheaf_iff_multifork]

Mathlib/CategoryTheory/Sites/CoverPreserving.lean

@@ -154,11 +154,8 @@ theorem compatiblePreservingOfDownwardsClosed (F : C ⥤ D) [F.Full] [F.Faithful
 
 variable {F J K}
 
-/-- If `F` is cover-preserving and compatible-preserving,
-then `F` is a continuous functor.
-
-This result is basically <https://stacks.math.columbia.edu/tag/00WW>.
--/
+/-- If `F` is cover-preserving and compatible-preserving, then `F` is a continuous functor. -/
+@[stacks 00WW "This is basically this Stacks entry."]
 lemma Functor.isContinuous_of_coverPreserving (hF₁ : CompatiblePreserving.{w} K F)
     (hF₂ : CoverPreserving J K F) : Functor.IsContinuous.{w} F J K where
   op_comp_isSheaf_of_types G X S hS x hx := by

Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

@@ -45,8 +45,9 @@ noncomputable section
 
 /--
 The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram
-of <https://stacks.math.columbia.edu/tag/00VM>.
+of the Stacks entry.
 -/
+@[stacks 00VM "This is the middle object of the fork diagram there."]
 def FirstObj : Type max v u :=
   ∏ᶜ fun f : ΣY, { f : Y ⟶ X // R f } => P.obj (op f.1)
 
@@ -78,8 +79,9 @@ instance : Inhabited (FirstObj P ((⊥ : Sieve X) : Presieve X)) :=
 
 /--
 The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram
-of <https://stacks.math.columbia.edu/tag/00VM>.
+of the Stacks entry.
 -/
+@[stacks 00VM "This is the left morphism of the fork diagram there."]
 def forkMap : P.obj (op X) ⟶ FirstObj P R :=
   Pi.lift fun f => P.map f.2.1.op
 
@@ -176,15 +178,17 @@ namespace Presieve
 variable [R.hasPullbacks]
 
 /--
-The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which
+The rightmost object of the fork diagram of the Stacks entry, which
 contains the data used to check a family of elements for a presieve is compatible.
 -/
-@[simp] def SecondObj : Type max v u :=
+@[simp, stacks 00VM "This is the rightmost object of the fork diagram there."]
+def SecondObj : Type max v u :=
   ∏ᶜ fun fg : (ΣY, { f : Y ⟶ X // R f }) × ΣZ, { g : Z ⟶ X // R g } =>
     haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2
     P.obj (op (pullback fg.1.2.1 fg.2.2.1))
 
-/-- The map `pr₀*` of <https://stacks.math.columbia.edu/tag/00VL>. -/
+/-- The map `pr₀*` of the Stacks entry. -/
+@[stacks 00VM "This is the map `pr₀*` there."]
 def firstMap : FirstObj P R ⟶ SecondObj P R :=
   Pi.lift fun fg =>
     haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2
@@ -193,7 +197,8 @@ def firstMap : FirstObj P R ⟶ SecondObj P R :=
 instance [HasPullbacks C] : Inhabited (SecondObj P (⊥ : Presieve X)) :=
   ⟨firstMap _ _ default⟩
 
-/-- The map `pr₁*` of <https://stacks.math.columbia.edu/tag/00VL>. -/
+/-- The map `pr₁*` of the Stacks entry. -/
+@[stacks 00VM "This is the map `pr₁*` there."]
 def secondMap : FirstObj P R ⟶ SecondObj P R :=
   Pi.lift fun fg =>
     haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2
@@ -254,10 +259,11 @@ variable {B : C} {I : Type} (X : I → C) (π : (i : I) → X i ⟶ B)
 -- TODO: allow `I : Type w`
 
 /--
-The middle object of the fork diagram of <https://stacks.math.columbia.edu/tag/00VM>.
+The middle object of the fork diagram of the Stacks entry.
 The difference between this and `Equalizer.FirstObj P (ofArrows X π)` arises if the family of
 arrows `π` contains duplicates. The `Presieve.ofArrows` doesn't see those.
 -/
+@[stacks 00VM "The middle object of the fork diagram there."]
 def FirstObj : Type w := ∏ᶜ (fun i ↦ P.obj (op (X i)))
 
 @[ext]
@@ -268,10 +274,11 @@ lemma FirstObj.ext (z₁ z₂ : FirstObj P X) (h : ∀ i, (Pi.π _ i : FirstObj
   exact h i
 
 /--
-The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM.
+The rightmost object of the fork diagram of the Stacks entry.
 The difference between this and `Equalizer.Presieve.SecondObj P (ofArrows X π)` arises if the
 family of arrows `π` contains duplicates. The `Presieve.ofArrows` doesn't see those.
 -/
+@[stacks 00VM "The rightmost object of the fork diagram there."]
 def SecondObj : Type w  :=
   ∏ᶜ (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2))))
 

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

@@ -83,9 +83,10 @@ A presheaf is a sheaf (resp, separated) if every *compatible* family of elements
 (resp, at most one) amalgamation.
 
 This data is referred to as a `family` in [MM92], Chapter III, Section 4. It is also a concrete
-version of the elements of the middle object in https://stacks.math.columbia.edu/tag/00VM which is
+version of the elements of the middle object in the Stacks entry which is
 more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant].
 -/
+@[stacks 00VM "This is a concrete version of the elements of the middle object there."]
 def FamilyOfElements (P : Cᵒᵖ ⥤ Type w) (R : Presieve X) :=
   ∀ ⦃Y : C⦄ (f : Y ⟶ X), R f → P.obj (op Y)
 
@@ -416,8 +417,8 @@ This version is also useful to establish that being a sheaf is preserved under i
 presheaves.
 
 See the discussion before Equation (3) of [MM92], Chapter III, Section 4. See also C2.1.4 of
-[Elephant]. This is also a direct reformulation of <https://stacks.math.columbia.edu/tag/00Z8>.
--/
+[Elephant]. -/
+@[stacks 00Z8 "Direct reformulation"]
 def YonedaSheafCondition (P : Cᵒᵖ ⥤ Type v₁) (S : Sieve X) : Prop :=
   ∀ f : S.functor ⟶ P, ∃! g, S.functorInclusion ≫ g = f