Skip to content

Commit fafc2d8

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
2 parents dab2576 + 1f53427 commit fafc2d8

File tree

24 files changed

+221
-39
lines changed

24 files changed

+221
-39
lines changed

‎Mathlib.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5045,6 +5045,7 @@ import Mathlib.RingTheory.Congruence.Opposite
50455045
import Mathlib.RingTheory.Coprime.Basic
50465046
import Mathlib.RingTheory.Coprime.Ideal
50475047
import Mathlib.RingTheory.Coprime.Lemmas
5048+
import Mathlib.RingTheory.CotangentLocalizationAway
50485049
import Mathlib.RingTheory.DedekindDomain.AdicValuation
50495050
import Mathlib.RingTheory.DedekindDomain.Basic
50505051
import Mathlib.RingTheory.DedekindDomain.Different
@@ -5074,6 +5075,7 @@ import Mathlib.RingTheory.Etale.Field
50745075
import Mathlib.RingTheory.Etale.Kaehler
50755076
import Mathlib.RingTheory.Etale.Pi
50765077
import Mathlib.RingTheory.EuclideanDomain
5078+
import Mathlib.RingTheory.Extension
50775079
import Mathlib.RingTheory.Extension.Basic
50785080
import Mathlib.RingTheory.Extension.Cotangent.Basic
50795081
import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
@@ -5116,6 +5118,7 @@ import Mathlib.RingTheory.FractionalIdeal.Operations
51165118
import Mathlib.RingTheory.FreeCommRing
51175119
import Mathlib.RingTheory.FreeRing
51185120
import Mathlib.RingTheory.Frobenius
5121+
import Mathlib.RingTheory.Generators
51195122
import Mathlib.RingTheory.GradedAlgebra.Basic
51205123
import Mathlib.RingTheory.GradedAlgebra.FiniteType
51215124
import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
@@ -5198,6 +5201,7 @@ import Mathlib.RingTheory.Jacobson.Radical
51985201
import Mathlib.RingTheory.Jacobson.Ring
51995202
import Mathlib.RingTheory.Jacobson.Semiprimary
52005203
import Mathlib.RingTheory.Kaehler.Basic
5204+
import Mathlib.RingTheory.Kaehler.CotangentComplex
52015205
import Mathlib.RingTheory.Kaehler.JacobiZariski
52025206
import Mathlib.RingTheory.Kaehler.Polynomial
52035207
import Mathlib.RingTheory.Kaehler.TensorProduct
@@ -5362,6 +5366,7 @@ import Mathlib.RingTheory.PowerSeries.Substitution
53625366
import Mathlib.RingTheory.PowerSeries.Trunc
53635367
import Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
53645368
import Mathlib.RingTheory.PowerSeries.WellKnown
5369+
import Mathlib.RingTheory.Presentation
53655370
import Mathlib.RingTheory.Prime
53665371
import Mathlib.RingTheory.PrincipalIdealDomain
53675372
import Mathlib.RingTheory.PrincipalIdealDomainOfPrime

‎Mathlib/Algebra/Polynomial/FieldDivision.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -521,6 +521,10 @@ theorem monic_normalize [DecidableEq R] (hp0 : p ≠ 0) : Monic (normalize p) :=
521521
rw [Monic, leadingCoeff_normalize, normalize_eq_one]
522522
apply hp0
523523

524+
theorem normalize_eq_self_iff_monic [DecidableEq R] {p : Polynomial R} (hp : p ≠ 0) :
525+
normalize p = p ↔ p.Monic :=
526+
⟨fun h ↦ h ▸ monic_normalize hp, fun h ↦ Monic.normalize_eq_self h⟩
527+
524528
theorem leadingCoeff_div (hpq : q.degree ≤ p.degree) :
525529
(p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff := by
526530
by_cases hq : q = 0
@@ -670,6 +674,21 @@ theorem leadingCoeff_mul_prod_normalizedFactors [DecidableEq R] (a : R[X]) :
670674
mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀] <;>
671675
simp_all
672676

677+
open UniqueFactorizationMonoid in
678+
protected theorem mem_normalizedFactors_iff [DecidableEq R] (hq : q ≠ 0) :
679+
p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q := by
680+
by_cases hp : p = 0
681+
· simpa [hp] using zero_notMem_normalizedFactors _
682+
· rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]
683+
684+
variable (p) in
685+
@[simp]
686+
theorem map_normalize [DecidableEq R] [Field S] [DecidableEq S] (f : R →+* S) :
687+
map f (normalize p) = normalize (map f p) := by
688+
by_cases hp : p = 0
689+
· simp [hp]
690+
· simp [normalize_apply, Polynomial.map_mul, normUnit, hp]
691+
673692
end Field
674693

675694
end Polynomial

‎Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -130,8 +130,8 @@ theorem SuperpolynomialDecay.trans_eventuallyLE (hk : 0 ≤ᶠ[l] k) (hg : Super
130130
(hg' : SuperpolynomialDecay l k g') (hfg : g ≤ᶠ[l] f) (hfg' : f ≤ᶠ[l] g') :
131131
SuperpolynomialDecay l k f := fun z =>
132132
tendsto_of_tendsto_of_tendsto_of_le_of_le' (hg z) (hg' z)
133-
(hfg.mp (hk.mono fun _ hx hx' => mul_le_mul_of_nonneg_left hx' (pow_nonneg hx z)))
134-
(hfg'.mp (hk.mono fun _ hx hx' => mul_le_mul_of_nonneg_left hx' (pow_nonneg hx z)))
133+
(by filter_upwards [hfg, hk] with x hx (hx' : 0 ≤ k x) using by gcongr)
134+
(by filter_upwards [hfg', hk] with x hx (hx' : 0 ≤ k x) using by gcongr)
135135

136136
end OrderedCommSemiring
137137

‎Mathlib/Analysis/BoxIntegral/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -710,8 +710,8 @@ theorem integrable_of_bounded_and_ae_continuousWithinAt [CompleteSpace E] {I : B
710710
· have : ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C) := by
711711
intro J _
712712
rw [norm_smul, μ.toBoxAdditive_apply, Real.norm_of_nonneg measureReal_nonneg, two_mul]
713-
refine mul_le_mul_of_nonneg_left (le_trans (norm_sub_le _ _) (add_le_add ?_ ?_)) (by simp) <;>
714-
exact hC _ (TaggedPrepartition.tag_mem_Icc _ J)
713+
gcongr
714+
apply norm_sub_le_of_le <;> exact hC _ (TaggedPrepartition.tag_mem_Icc _ J)
715715
apply (norm_sum_le_of_le B' this).trans
716716
simp_rw [← sum_mul, μ.toBoxAdditive_apply, measureReal_def,
717717
← toReal_sum (fun J hJ ↦ μJ_ne_top J (hB' hJ))]

‎Mathlib/Analysis/Calculus/ContDiff/Bounds.lean‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -68,8 +68,8 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
6868
‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
6969
IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
7070
_ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
71-
‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
72-
mul_le_mul_of_nonneg_right (B.norm_precompR_le Du) (by positivity)
71+
‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ := by
72+
gcongr; exact B.norm_precompR_le Du
7373
_ = _ := by
7474
congr 1
7575
apply Finset.sum_congr rfl fun i hi => ?_
@@ -90,8 +90,8 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
9090
IH _ (hf.fderivWithin hs In) (hg.of_le (Nat.cast_le.2 (Nat.le_succ n)))
9191
_ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1),
9292
n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
93-
‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
94-
mul_le_mul_of_nonneg_right (B.norm_precompL_le Du) (by positivity)
93+
‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ := by
94+
gcongr; exact B.norm_precompL_le Du
9595
_ = _ := by
9696
congr 1
9797
apply Finset.sum_congr rfl fun i _ => ?_
@@ -198,7 +198,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear (B : E →L
198198
‖iteratedFDerivWithin 𝕜 (n - i) gu su xu‖ :=
199199
Bu.norm_iteratedFDerivWithin_le_of_bilinear_aux hfu hgu hsu hxu
200200
simp only [Nfu, Ngu, NBu] at this
201-
exact this.trans (mul_le_mul_of_nonneg_right Bu_le (by positivity))
201+
exact this.trans <| by gcongr
202202

203203
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the
204204
iterated derivatives of `f` and `g` when `B` is bilinear:
@@ -550,7 +550,8 @@ theorem norm_iteratedFDerivWithin_clm_apply_const {f : E → F →L[𝕜] G} {c
550550
let g : (F →L[𝕜] G) →L[𝕜] G := ContinuousLinearMap.apply 𝕜 G c
551551
have h := g.norm_compContinuousMultilinearMap_le (iteratedFDerivWithin 𝕜 n f s x)
552552
rw [← g.iteratedFDerivWithin_comp_left hf hs hx hn] at h
553-
refine h.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))
553+
refine h.trans ?_
554+
gcongr
554555
refine g.opNorm_le_bound (norm_nonneg _) fun f => ?_
555556
rw [ContinuousLinearMap.apply_apply, mul_comm]
556557
exact f.le_opNorm c

‎Mathlib/Analysis/Calculus/LagrangeMultipliers.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Yury Kudryashov
55
-/
66
import Mathlib.Analysis.Calculus.FDeriv.Prod
77
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
8-
import Mathlib.GroupTheory.MonoidLocalization.Basic
98
import Mathlib.LinearAlgebra.Dual.Defs
109

1110
/-!

‎Mathlib/Analysis/InnerProductSpace/Basic.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis
66
import Mathlib.Algebra.BigOperators.Field
77
import Mathlib.Analysis.Complex.Basic
88
import Mathlib.Analysis.InnerProductSpace.Defs
9-
import Mathlib.GroupTheory.MonoidLocalization.Basic
109

1110
/-!
1211
# Properties of inner product spaces

‎Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
88
import Mathlib.Analysis.Complex.RealDeriv
99
import Mathlib.Analysis.SpecialFunctions.Exp
1010
import Mathlib.Analysis.SpecialFunctions.Exponential
11-
import Mathlib.GroupTheory.MonoidLocalization.Basic
1211

1312
/-!
1413
# Complex and real exponential

‎Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean‎

Lines changed: 146 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,8 @@ open Category Limits
3333

3434
namespace Functor
3535

36-
variable {C D H : Type*} [Category C] [Category D] [Category H] (L : C ⥤ D) (F : C ⥤ H)
36+
variable {C D D' H : Type*} [Category C] [Category D] [Category D'] [Category H]
37+
(L : C ⥤ D) (L' : C ⥤ D') (F : C ⥤ H)
3738

3839
/-- The condition that a functor `F` has a pointwise left Kan extension along `L` at `Y`.
3940
It means that the functor `CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H`
@@ -55,6 +56,108 @@ abbrev HasPointwiseRightKanExtensionAt (Y : D) :=
5556
that it has a pointwise right Kan extension at any object. -/
5657
abbrev HasPointwiseRightKanExtension := ∀ (Y : D), HasPointwiseRightKanExtensionAt L F Y
5758

59+
lemma hasPointwiseLeftKanExtensionAt_iff_of_iso {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂) :
60+
HasPointwiseLeftKanExtensionAt L F Y₁ ↔
61+
HasPointwiseLeftKanExtensionAt L F Y₂ := by
62+
revert Y₁ Y₂ e
63+
suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseLeftKanExtensionAt L F Y₁],
64+
HasPointwiseLeftKanExtensionAt L F Y₂ from
65+
fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
66+
intro Y₁ Y₂ e _
67+
change HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)
68+
infer_instance
69+
70+
lemma hasPointwiseRightKanExtensionAt_iff_of_iso {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂) :
71+
HasPointwiseRightKanExtensionAt L F Y₁ ↔
72+
HasPointwiseRightKanExtensionAt L F Y₂ := by
73+
revert Y₁ Y₂ e
74+
suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseRightKanExtensionAt L F Y₁],
75+
HasPointwiseRightKanExtensionAt L F Y₂ from
76+
fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
77+
intro Y₁ Y₂ e _
78+
change HasLimit ((StructuredArrow.mapIso e.symm).functor ⋙ StructuredArrow.proj Y₁ L ⋙ F)
79+
infer_instance
80+
81+
variable {L} in
82+
/-- `HasPointwiseLeftKanExtensionAt` is invariant when we replace `L` by an equivalent functor. -/
83+
lemma hasPointwiseLeftKanExtensionAt_iff_of_natIso {L' : C ⥤ D} (e : L ≅ L') (Y : D) :
84+
HasPointwiseLeftKanExtensionAt L F Y ↔
85+
HasPointwiseLeftKanExtensionAt L' F Y := by
86+
revert L L' e
87+
suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseLeftKanExtensionAt L F Y],
88+
HasPointwiseLeftKanExtensionAt L' F Y from
89+
fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
90+
intro L L' e _
91+
let Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso _ e.symm
92+
let e' : CostructuredArrow.proj L' Y ⋙ F ≅
93+
Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F := Iso.refl _
94+
exact hasColimit_of_iso e'
95+
96+
variable {L} in
97+
/-- `HasPointwiseRightKanExtensionAt` is invariant when we replace `L` by an equivalent functor. -/
98+
lemma hasPointwiseRightKanExtensionAt_iff_of_natIso {L' : C ⥤ D} (e : L ≅ L') (Y : D) :
99+
HasPointwiseRightKanExtensionAt L F Y ↔
100+
HasPointwiseRightKanExtensionAt L' F Y := by
101+
revert L L' e
102+
suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y],
103+
HasPointwiseRightKanExtensionAt L' F Y from
104+
fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
105+
intro L L' e _
106+
let Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso _ e.symm
107+
let e' : StructuredArrow.proj Y L' ⋙ F ≅
108+
Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F := Iso.refl _
109+
exact hasLimit_of_iso e'.symm
110+
111+
lemma hasPointwiseLeftKanExtensionAt_of_equivalence
112+
(E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y')
113+
[HasPointwiseLeftKanExtensionAt L F Y] :
114+
HasPointwiseLeftKanExtensionAt L' F Y' := by
115+
rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso F eL,
116+
hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]
117+
let Φ := CostructuredArrow.post L E.functor Y
118+
have : HasColimit ((asEquivalence Φ).functor ⋙
119+
CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
120+
(inferInstance : HasPointwiseLeftKanExtensionAt L F Y)
121+
exact hasColimit_of_equivalence_comp (asEquivalence Φ)
122+
123+
lemma hasPointwiseLeftKanExtensionAt_iff_of_equivalence
124+
(E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y') :
125+
HasPointwiseLeftKanExtensionAt L F Y ↔
126+
HasPointwiseLeftKanExtensionAt L' F Y' := by
127+
constructor
128+
· intro
129+
exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e
130+
· intro
131+
exact hasPointwiseLeftKanExtensionAt_of_equivalence L' L F E.symm
132+
(isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
133+
isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
134+
(E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
135+
136+
lemma hasPointwiseRightKanExtensionAt_of_equivalence
137+
(E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y')
138+
[HasPointwiseRightKanExtensionAt L F Y] :
139+
HasPointwiseRightKanExtensionAt L' F Y' := by
140+
rw [← hasPointwiseRightKanExtensionAt_iff_of_natIso F eL,
141+
hasPointwiseRightKanExtensionAt_iff_of_iso _ F e.symm]
142+
let Φ := StructuredArrow.post Y L E.functor
143+
have : HasLimit ((asEquivalence Φ).functor ⋙
144+
StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F) :=
145+
(inferInstance : HasPointwiseRightKanExtensionAt L F Y)
146+
exact hasLimit_of_equivalence_comp (asEquivalence Φ)
147+
148+
lemma hasPointwiseRightKanExtensionAt_iff_of_equivalence
149+
(E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y') :
150+
HasPointwiseRightKanExtensionAt L F Y ↔
151+
HasPointwiseRightKanExtensionAt L' F Y' := by
152+
constructor
153+
· intro
154+
exact hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e
155+
· intro
156+
exact hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
157+
(isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
158+
isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
159+
(E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
160+
58161
namespace LeftExtension
59162

60163
variable {F L}
@@ -98,6 +201,27 @@ lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app
98201
IsIso (E.hom.app X) := by
99202
simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal
100203

204+
/-- The condition of being a pointwise left Kan extension at an object `Y` is
205+
unchanged by replacing `Y` by an isomorphic object `Y'`. -/
206+
def isPointwiseLeftKanExtensionAtOfIso'
207+
{Y : D} (hY : E.IsPointwiseLeftKanExtensionAt Y) {Y' : D} (e : Y ≅ Y') :
208+
E.IsPointwiseLeftKanExtensionAt Y' :=
209+
IsColimit.ofIsoColimit (hY.whiskerEquivalence (CostructuredArrow.mapIso e.symm))
210+
(Cocones.ext (E.right.mapIso e))
211+
212+
/-- The condition of being a pointwise left Kan extension at an object `Y` is
213+
unchanged by replacing `Y` by an isomorphic object `Y'`. -/
214+
def isPointwiseLeftKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
215+
E.IsPointwiseLeftKanExtensionAt Y ≃ E.IsPointwiseLeftKanExtensionAt Y' where
216+
toFun h := E.isPointwiseLeftKanExtensionAtOfIso' h e
217+
invFun h := E.isPointwiseLeftKanExtensionAtOfIso' h e.symm
218+
left_inv h := by
219+
dsimp only [IsPointwiseLeftKanExtensionAt]
220+
apply Subsingleton.elim
221+
right_inv h := by
222+
dsimp only [IsPointwiseLeftKanExtensionAt]
223+
apply Subsingleton.elim
224+
101225
namespace IsPointwiseLeftKanExtensionAt
102226

103227
variable {E} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y)
@@ -235,6 +359,27 @@ lemma IsPointwiseRightKanExtensionAt.isIso_hom_app
235359
IsIso (E.hom.app X) := by
236360
simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial
237361

362+
/-- The condition of being a pointwise right Kan extension at an object `Y` is
363+
unchanged by replacing `Y` by an isomorphic object `Y'`. -/
364+
def isPointwiseRightKanExtensionAtOfIso'
365+
{Y : D} (hY : E.IsPointwiseRightKanExtensionAt Y) {Y' : D} (e : Y ≅ Y') :
366+
E.IsPointwiseRightKanExtensionAt Y' :=
367+
IsLimit.ofIsoLimit (hY.whiskerEquivalence (StructuredArrow.mapIso e.symm))
368+
(Cones.ext (E.left.mapIso e))
369+
370+
/-- The condition of being a pointwise right Kan extension at an object `Y` is
371+
unchanged by replacing `Y` by an isomorphic object `Y'`. -/
372+
def isPointwiseRightKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
373+
E.IsPointwiseRightKanExtensionAt Y ≃ E.IsPointwiseRightKanExtensionAt Y' where
374+
toFun h := E.isPointwiseRightKanExtensionAtOfIso' h e
375+
invFun h := E.isPointwiseRightKanExtensionAtOfIso' h e.symm
376+
left_inv h := by
377+
dsimp only [IsPointwiseRightKanExtensionAt]
378+
apply Subsingleton.elim
379+
right_inv h := by
380+
dsimp only [IsPointwiseRightKanExtensionAt]
381+
apply Subsingleton.elim
382+
238383
namespace IsPointwiseRightKanExtensionAt
239384

240385
variable {E} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y)

‎Mathlib/CategoryTheory/Limits/HasLimits.lean‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -433,18 +433,23 @@ theorem limit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤
433433

434434
open CategoryTheory.Equivalence
435435

436-
instance hasLimitEquivalenceComp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
436+
instance hasLimit_equivalence_comp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
437437
HasLimit.mk
438438
{ cone := Cone.whisker e.functor (limit.cone F)
439439
isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) e }
440440

441441
-- not entirely sure why this is needed
442442
/-- If a `E ⋙ F` has a limit, and `E` is an equivalence, we can construct a limit of `F`.
443443
-/
444-
theorem hasLimitOfEquivalenceComp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F := by
445-
haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimitEquivalenceComp e.symm
444+
theorem hasLimit_of_equivalence_comp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F := by
445+
haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm
446446
apply hasLimit_of_iso (e.invFunIdAssoc F)
447447

448+
@[deprecated (since := "2025-03-02")] alias hasLimitEquivalenceComp :=
449+
hasLimit_equivalence_comp
450+
@[deprecated (since := "2025-03-02")] alias hasLimitOfEquivalenceComp :=
451+
hasLimit_of_equivalence_comp
452+
448453
-- `hasLimitCompEquivalence` and `hasLimitOfCompEquivalence`
449454
-- are proved in `CategoryTheory/Adjunction/Limits.lean`.
450455
section LimFunctor
@@ -560,7 +565,7 @@ theorem hasLimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e
560565
[HasLimitsOfShape J C] : HasLimitsOfShape J' C := by
561566
constructor
562567
intro F
563-
apply hasLimitOfEquivalenceComp e
568+
apply hasLimit_of_equivalence_comp e
564569

565570
variable (C)
566571

0 commit comments

Comments
 (0)