Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -81,6 +81,12 @@ lemma tendsto_rpow_atBot_of_base_lt_one (b : ℝ) (hb₀ : 0 < b) (hb₁ : b < 1
   refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_
   exact (log_neg_iff hb₀).mpr hb₁
 
+lemma tendsto_rpow_atTop_of_base_gt_one (b : ℝ) (hb : 1 < b) :
+    Tendsto (b ^ · : ℝ → ℝ) atTop atTop := by
+  simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
+  refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_pos <| tendsto_id (α := ℝ)).mpr ?_
+  exact log_pos hb
+
 lemma tendsto_rpow_atBot_of_base_gt_one (b : ℝ) (hb : 1 < b) :
     Tendsto (b ^ · : ℝ → ℝ) atBot (𝓝 0) := by
   simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]

Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2023 Yuma Mizuno. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yuma Mizuno
+Authors: Yuma Mizuno, Fernando Chu
 -/
 module
 
+public import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
+public import Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
 public import Mathlib.Tactic.CategoryTheory.Bicategory.Basic
 public import Mathlib.Tactic.CategoryTheory.BicategoricalComp
 
@@ -22,6 +24,9 @@ identities. The 2-morphism `η` is called the unit and `ε` is called the counit
 * `Bicategory.Equivalence.mkOfAdjointifyCounit`: construct an adjoint equivalence from
   2-isomorphisms
   `η : 𝟙 a ≅ f ≫ g` and `ε : g ≫ f ≅ 𝟙 b`, by upgrading `ε` to a counit.
+* `Pseudofunctor.mapAdjunction`: a pseudofunctor `F` carries an adjunction `f ⊣ g`
+  between 1-morphisms to an adjunction `F.map f ⊣ F.map g`. An analogous definition is given
+  for `StrictPseudofunctor`.
 
 ## TODO
 
@@ -34,15 +39,14 @@ identities. The 2-morphism `η` is called the unit and `ε` is called the counit
 
 namespace CategoryTheory
 
-namespace Bicategory
-
-open Category
+open Category Bicategory
 
-open scoped Bicategory
+universe w₁ w₂ v₁ v₂ u₁ u₂
 
-universe w v u
+variable {B : Type u₁} [Bicategory.{w₁, v₁} B] {C : Type u₂} [Bicategory.{w₂, v₂} C]
+  {a b c : B} {f : a ⟶ b} {g : b ⟶ a}
 
-variable {B : Type u} [Bicategory.{w, v} B] {a b c : B} {f : a ⟶ b} {g : b ⟶ a}
+namespace Bicategory
 
 /-- The 2-morphism defined by the following pasting diagram:
 ```
@@ -341,4 +345,55 @@ end
 
 end Bicategory
 
+namespace Pseudofunctor
+
+variable (F : Pseudofunctor B C) (adj : f ⊣ g)
+
+lemma leftZigzag_map :
+    leftZigzag ((F.mapId a).inv ≫ F.map₂ adj.unit ≫ (F.mapComp f g).hom)
+      ((F.mapComp g f).inv ≫ F.map₂ adj.counit ≫ (F.mapId b).hom) =
+    (F.mapId a).inv ▷ F.map f ⊗≫ (F.mapComp (𝟙 a) f).inv ≫
+      F.map₂ (leftZigzag adj.unit adj.counit) ≫
+        (F.mapComp f (𝟙 b)).hom ⊗≫ F.map f ◁ (F.mapId b).hom := by
+  simp [leftZigzag, bicategoricalComp]
+
+lemma rightZigzag_map :
+    rightZigzag ((F.mapId a).inv ≫ F.map₂ adj.unit ≫ (F.mapComp f g).hom)
+      ((F.mapComp g f).inv ≫ F.map₂ adj.counit ≫ (F.mapId b).hom) =
+    F.map g ◁ (F.mapId a).inv ⊗≫ (F.mapComp g (𝟙 a)).inv ≫
+      F.map₂ (rightZigzag adj.unit adj.counit) ≫
+        (F.mapComp (𝟙 b) g).hom ⊗≫ (F.mapId b).hom ▷ F.map g := by
+  simp [rightZigzag, bicategoricalComp, F.map₂_iso_inv]
+
+/-- A pseudofunctor carries an adjunction `f ⊣ g` to an adjunction `F.map f ⊣ F.map g`. -/
+@[simps]
+def mapAdjunction : F.map f ⊣ F.map g where
+  unit := (F.mapId a).inv ≫ F.map₂ adj.unit ≫ (F.mapComp f g).hom
+  counit := (F.mapComp g f).inv ≫ F.map₂ adj.counit ≫ (F.mapId b).hom
+  left_triangle := by simp [leftZigzag_map, bicategoricalComp, F.map₂_iso_inv]
+  right_triangle := by simp [rightZigzag_map, bicategoricalComp, F.map₂_iso_inv]
+
+end Pseudofunctor
+
+namespace StrictPseudofunctor
+
+variable (F : StrictPseudofunctor B C) (adj : f ⊣ g)
+
+/-- A strict pseudofunctor carries an adjunction `f ⊣ g` to an adjunction
+`F.map f ⊣ F.map g`. -/
+@[simps!]
+def mapAdjunction : F.map f ⊣ F.map g := F.toPseudofunctor.mapAdjunction adj
+
+lemma mapAdjunction_unit' :
+    (F.mapAdjunction adj).unit =
+      eqToHom (F.map_id a).symm ≫ F.map₂ adj.unit ≫ eqToHom (F.map_comp f g) := by
+  simp [F.mapId_eq_eqToIso, F.mapComp_eq_eqToIso]
+
+lemma mapAdjunction_counit' :
+    (F.mapAdjunction adj).counit =
+      eqToHom (F.map_comp g f).symm ≫ F.map₂ adj.counit ≫ eqToHom (F.map_id b) := by
+  simp [F.mapId_eq_eqToIso, F.mapComp_eq_eqToIso]
+
+end StrictPseudofunctor
+
 end CategoryTheory

Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean

@@ -175,6 +175,10 @@ lemma map₂_inv {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] : F.map₂ (inv η) =
   apply IsIso.eq_inv_of_hom_inv_id
   simp [← F.map₂_comp η (inv η)]
 
+lemma map₂_iso_inv {f g : a ⟶ b} (η : f ≅ g) :
+    F.map₂ η.inv = inv (F.map₂ η.hom) := by
+  rw [← F.map₂_inv, IsIso.Iso.inv_hom]
+
 @[reassoc, simp]
 lemma map₂_hom_inv {f g : a ⟶ b} (η : f ≅ g) :
     F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f) := by

Mathlib/Data/Finsupp/Weight.lean

@@ -200,6 +200,14 @@ theorem finite_of_nat_weight_le [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x 
   grw [← le_weight _ (hw x)] at hd
   simp [*]
 
+theorem finite_of_nat_weight_lt [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x ≠ 0) (n : ℕ) :
+    {d : σ →₀ ℕ | weight w d < n}.Finite :=
+  Set.Finite.subset (finite_of_nat_weight_le w hw n) (by grind)
+
+theorem finite_of_nat_weight_eq [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x ≠ 0) (n : ℕ) :
+    {d : σ →₀ ℕ | weight w d = n}.Finite :=
+  Set.Finite.subset (finite_of_nat_weight_le w hw n) (by grind)
+
 end CanonicallyOrderedAddCommMonoid
 
 variable {R : Type*} [AddCommMonoid R]
@@ -257,6 +265,9 @@ theorem finite_of_degree_le [Finite σ] (n : ℕ) :
 lemma finite_of_degree_lt [Finite σ] (n : ℕ) : {f : σ →₀ ℕ | degree f < n}.Finite :=
   Set.Finite.subset (finite_of_degree_le n) (by grind)
 
+lemma finite_of_degree_eq [Finite σ] (n : ℕ) : {f : σ →₀ ℕ | f.degree = n}.Finite :=
+  Set.Finite.subset (finite_of_degree_le n) (by grind)
+
 lemma range_single_one :
     Set.range (fun a : σ ↦ Finsupp.single a 1) = { d | d.degree = 1 } := by
   refine subset_antisymm ?_ ?_

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

@@ -109,6 +109,10 @@ theorem homogeneousSubmodule_eq_finsupp_supported (n : ℕ) :
   simp_rw [degree_eq_weight_one]
   exact weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n
 
+lemma homogeneousSubmodule_fg [Finite σ] (n : ℕ) :
+    (homogeneousSubmodule σ R n).FG :=
+  weightedHomogeneousSubmodule_fg R (1 : σ → ℕ) (by simp) n
+
 variable {σ R}
 
 set_option backward.isDefEq.respectTransparency false in
@@ -165,6 +169,10 @@ theorem isHomogeneous_zero (n : ℕ) : IsHomogeneous (0 : MvPolynomial σ R) n :
 theorem isHomogeneous_one : IsHomogeneous (1 : MvPolynomial σ R) 0 :=
   isHomogeneous_C _ _
 
+lemma isHomogeneous_of_isEmpty [IsEmpty σ] (f : MvPolynomial σ R) : f.IsHomogeneous 0 := by
+  rw [eq_C_of_isEmpty f]
+  exact isHomogeneous_C _ _
+
 variable {σ}
 
 theorem isHomogeneous_X (i : σ) : IsHomogeneous (X i : MvPolynomial σ R) 1 := by
@@ -565,11 +573,26 @@ theorem homogeneousComponent_of_mem {m n : ℕ} {p : MvPolynomial σ R}
     homogeneousComponent m p = if m = n then p else 0 :=
   weightedHomogeneousComponent_of_mem h
 
+lemma homogeneousComponent_eq_self {n : ℕ} {p : MvPolynomial σ R}
+    (hp : p.IsHomogeneous n) : homogeneousComponent n p = p := by
+  simp [homogeneousComponent_of_mem hp]
+
 lemma support_homogeneousComponent (n : ℕ) (p : MvPolynomial σ R) :
     (homogeneousComponent n p).support = {c ∈ p.support | c.degree = n} := by
   rw [degree_eq_weight_one]
   exact support_weightedHomogeneousComponent n p
 
+lemma rename_homogeneousComponent {τ : Type*} {φ : σ → τ} (n : ℕ) (p : MvPolynomial σ R) :
+    rename φ (homogeneousComponent n p) = homogeneousComponent n (rename φ p) := by
+  induction p using MvPolynomial.induction_on' with
+  | monomial d c =>
+    rw [rename_monomial,
+      homogeneousComponent_of_mem (isHomogeneous_monomial c rfl),
+      homogeneousComponent_of_mem (isHomogeneous_monomial c (Finsupp.degree_mapDomain φ d))]
+    split_ifs <;> simp [rename_monomial]
+  | add p q hp hq => simp [map_add, hp, hq]
+
+
 end HomogeneousComponent
 
 end
@@ -607,6 +630,18 @@ theorem decomposition.decompose'_eq :
   rw [degree_eq_weight_one]
   rfl
 
+attribute [local instance] MvPolynomial.gradedAlgebra
+
+lemma mem_iff_homogeneousComponent_mem {I : Ideal (MvPolynomial σ R)}
+    (h : I.IsHomogeneous (homogeneousSubmodule σ R)) (p : MvPolynomial σ R) :
+    p ∈ I ↔ ∀ n, (homogeneousComponent n p) ∈ I :=
+  mem_iff_weightedHomogeneousComponent_mem R (1 : σ → ℕ) h p
+
+lemma homogeneousComponent_mem_of_mem {I : Ideal (MvPolynomial σ R)}
+    (h : I.IsHomogeneous (homogeneousSubmodule σ R)) {p : MvPolynomial σ R} (hp : p ∈ I) (n : ℕ) :
+    (homogeneousComponent n p) ∈ I :=
+  weightedHomogeneousComponent_mem_of_mem R (1 : σ → ℕ) h hp n
+
 end GradedAlgebra
 
 end MvPolynomial

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

@@ -11,7 +11,8 @@ public import Mathlib.Algebra.GradedMonoid
 public import Mathlib.Algebra.MvPolynomial.Basic
 public import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 public import Mathlib.Data.Finsupp.Weight
-public import Mathlib.RingTheory.GradedAlgebra.Basic
+public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
+public import Mathlib.RingTheory.MvPolynomial.Basic
 public import Mathlib.Tactic.Order
 
 /-!
@@ -161,6 +162,12 @@ theorem weightedHomogeneousSubmodule_eq_finsupp_supported (w : σ → M) (m : M)
   simp [IsWeightedHomogeneous]
   simp [AddMonoidAlgebra.mem_supported, Set.subset_def, MvPolynomial, coeff]
 
+lemma weightedHomogeneousSubmodule_fg [Finite σ] (w : σ → ℕ) (hw : ∀ (x : σ), w x ≠ 0) (n : ℕ) :
+    (weightedHomogeneousSubmodule R w n).FG := by
+  rw [weightedHomogeneousSubmodule_eq_finsupp_supported, ← Module.Finite.iff_fg]
+  have := (Finsupp.finite_of_nat_weight_eq w hw n).to_subtype
+  exact Module.Finite.of_basis (basisRestrictSupport R {d | Finsupp.weight w d = n})
+
 variable {R}
 
 set_option backward.isDefEq.respectTransparency false in
@@ -217,6 +224,11 @@ theorem isWeightedHomogeneous_zero (w : σ → M) (m : M) :
 theorem isWeightedHomogeneous_one (w : σ → M) : IsWeightedHomogeneous w (1 : MvPolynomial σ R) 0 :=
   isWeightedHomogeneous_C _ _
 
+lemma isWeightedHomogeneous_of_isEmpty [IsEmpty σ] (w : σ → M) (f : MvPolynomial σ R) :
+    IsWeightedHomogeneous w f 0 := by
+  rw [eq_C_of_isEmpty f]
+  exact isWeightedHomogeneous_C _ _
+
 /-- An indeterminate `i : σ` is weighted homogeneous of degree `w i`. -/
 theorem isWeightedHomogeneous_X (w : σ → M) (i : σ) :
     IsWeightedHomogeneous w (X i : MvPolynomial σ R) (w i) := by
@@ -476,6 +488,10 @@ theorem weightedHomogeneousComponent_of_mem [DecidableEq M] {m n : M}
     · rfl
     · simp only [coeff_zero]
 
+lemma weightedHomogeneousComponent_eq_self {n : M} {p : MvPolynomial σ R}
+    (hp : p.IsWeightedHomogeneous w n) : weightedHomogeneousComponent w n p = p := by
+  classical simp [weightedHomogeneousComponent_of_mem hp]
+
 lemma support_weightedHomogeneousComponent [DecidableEq M] (n : M) (p : MvPolynomial σ R) :
     (weightedHomogeneousComponent w n p).support = {c ∈ p.support | (weight w) c = n} := by
   ext c
@@ -676,6 +692,19 @@ theorem weightedDecomposition.decompose'_apply [DecidableEq M]
       weightedHomogeneousComponent w m φ :=
   MvPolynomial.decompose'_apply R w φ m
 
+attribute [local instance] MvPolynomial.weightedGradedAlgebra
+
+lemma mem_iff_weightedHomogeneousComponent_mem [DecidableEq M] {I : Ideal (MvPolynomial σ R)}
+    (h : I.IsHomogeneous (weightedHomogeneousSubmodule R w)) (p : MvPolynomial σ R) :
+    p ∈ I ↔ ∀ m : M, (weightedHomogeneousComponent w m p) ∈ I := by
+  simp_rw [← weightedDecomposition.decompose'_apply]
+  exact h.mem_iff
+
+lemma weightedHomogeneousComponent_mem_of_mem [DecidableEq M] {I : Ideal (MvPolynomial σ R)}
+    (h : I.IsHomogeneous (weightedHomogeneousSubmodule R w)) {p : MvPolynomial σ R} (hp : p ∈ I)
+    (m : M) : (weightedHomogeneousComponent w m p) ∈ I :=
+  (mem_iff_weightedHomogeneousComponent_mem R w h p).mp hp m
+
 end GradedAlgebra
 
 end MvPolynomial