Skip to content

Commit 03dd195

Browse files
jcommelinkim-emgrunweg
committed
chore: remove backward.privateInPublic from lakefile (#33034)
This PR removes the global `backward.privateInPublic true` setting from the lakefile. It adds the setting locally to many declarations. This is technical debt that will need to be cleaned later. A few modules seem to be particularly problematic. In those the backward compatibility setting is enabled at the file level, instead of at the declaration level. Part of the diff has been created with the help of Claude. But it struggled to do things correctly at scale and speed. To help review, I'm giving some hints below on how to digest the diff. These might be useful in the future, so I suggest including them in the commit message. ## Review hints ### Deletions This PR contains 14 deletions. They are contained in the following files: ```shell-session $ git diff master --numstat | awk '$2 > 0 && $3 ~ /\.lean$/ {print $3}' | xargs git diff master --stat -- Mathlib/Algebra/Lie/TraceForm.lean | 4 ++-- Mathlib/Analysis/SpecialFunctions/Exp.lean | 4 + Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
1 parent fc5f005 commit 03dd195

File tree

260 files changed

+1543
-18
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

260 files changed

+1543
-18
lines changed

‎Mathlib/Algebra/Category/AlgCat/Basic.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ universe v u
2626

2727
variable (R : Type u) [CommRing R]
2828

29+
set_option backward.privateInPublic true in
2930
/-- The category of R-algebras and their morphisms. -/
3031
structure AlgCat where
3132
private mk ::
@@ -45,6 +46,8 @@ instance : CoeSort (AlgCat R) (Type v) :=
4546

4647
attribute [coe] AlgCat.carrier
4748

49+
set_option backward.privateInPublic true in
50+
set_option backward.privateInPublic.warn false in
4851
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
4952
typeclasses. This is the preferred way to construct a term of `AlgCat R`. -/
5053
abbrev of (X : Type v) [Ring X] [Algebra R X] : AlgCat.{v} R :=
@@ -54,18 +57,23 @@ lemma coe_of (X : Type v) [Ring X] [Algebra R X] : (of R X : Type v) = X :=
5457
rfl
5558

5659
variable {R} in
60+
set_option backward.privateInPublic true in
5761
/-- The type of morphisms in `AlgCat R`. -/
5862
@[ext]
5963
structure Hom (A B : AlgCat.{v} R) where
6064
private mk ::
6165
/-- The underlying algebra map. -/
6266
hom' : A →ₐ[R] B
6367

68+
set_option backward.privateInPublic true in
69+
set_option backward.privateInPublic.warn false in
6470
instance : Category (AlgCat.{v} R) where
6571
Hom A B := Hom A B
6672
id A := ⟨AlgHom.id R A⟩
6773
comp f g := ⟨g.hom'.comp f.hom'⟩
6874

75+
set_option backward.privateInPublic true in
76+
set_option backward.privateInPublic.warn false in
6977
instance : ConcreteCategory (AlgCat.{v} R) (· →ₐ[R] ·) where
7078
hom := Hom.hom'
7179
ofHom := Hom.mk

‎Mathlib/Algebra/Category/BoolRing.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,18 +52,23 @@ instance : Inhabited BoolRing :=
5252
⟨of PUnit⟩
5353

5454
variable {R} in
55+
set_option backward.privateInPublic true in
5556
/-- The type of morphisms in `BoolRing`. -/
5657
@[ext]
5758
structure Hom (R S : BoolRing) where
5859
private mk ::
5960
/-- The underlying ring hom. -/
6061
hom' : R →+* S
6162

63+
set_option backward.privateInPublic true in
64+
set_option backward.privateInPublic.warn false in
6265
instance : Category BoolRing where
6366
Hom R S := Hom R S
6467
id R := ⟨RingHom.id R⟩
6568
comp f g := ⟨g.hom'.comp f.hom'⟩
6669

70+
set_option backward.privateInPublic true in
71+
set_option backward.privateInPublic.warn false in
6772
instance : ConcreteCategory BoolRing (· →+* ·) where
6873
hom f := f.hom'
6974
ofHom f := ⟨f⟩
@@ -85,6 +90,8 @@ instance hasForgetToCommRing : HasForget₂ BoolRing CommRingCat where
8590
{ obj := fun R ↦ CommRingCat.of R
8691
map := fun f ↦ CommRingCat.ofHom f.hom }
8792

93+
set_option backward.privateInPublic true in
94+
set_option backward.privateInPublic.warn false in
8895
/-- Constructs an isomorphism of Boolean rings from a ring isomorphism between them. -/
8996
@[simps]
9097
def Iso.mk {α β : BoolRing.{u}} (e : α ≃+* β) : α ≅ β where

‎Mathlib/Algebra/Category/CommAlgCat/Basic.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ universe w v u
2626
variable {R : Type u} [CommRing R]
2727

2828
variable (R) in
29+
set_option backward.privateInPublic true in
2930
/-- The category of R-algebras and their morphisms. -/
3031
structure CommAlgCat where
3132
private mk ::
@@ -47,25 +48,32 @@ instance : CoeSort (CommAlgCat R) (Type v) := ⟨carrier⟩
4748
attribute [coe] carrier
4849

4950
variable (R) in
51+
set_option backward.privateInPublic true in
52+
set_option backward.privateInPublic.warn false in
5053
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
5154
typeclasses. This is the preferred way to construct a term of `CommAlgCat R`. -/
5255
abbrev of (X : Type v) [CommRing X] [Algebra R X] : CommAlgCat.{v} R := ⟨X⟩
5356

5457
variable (R) in
5558
lemma coe_of (X : Type v) [CommRing X] [Algebra R X] : (of R X : Type v) = X := rfl
5659

60+
set_option backward.privateInPublic true in
5761
/-- The type of morphisms in `CommAlgCat R`. -/
5862
@[ext]
5963
structure Hom (A B : CommAlgCat.{v} R) where
6064
private mk ::
6165
/-- The underlying algebra map. -/
6266
hom' : A →ₐ[R] B
6367

68+
set_option backward.privateInPublic true in
69+
set_option backward.privateInPublic.warn false in
6470
instance : Category (CommAlgCat.{v} R) where
6571
Hom A B := Hom A B
6672
id A := ⟨AlgHom.id R A⟩
6773
comp f g := ⟨g.hom'.comp f.hom'⟩
6874

75+
set_option backward.privateInPublic true in
76+
set_option backward.privateInPublic.warn false in
6977
instance : ConcreteCategory (CommAlgCat.{v} R) (· →ₐ[R] ·) where
7078
hom := Hom.hom'
7179
ofHom := Hom.mk

‎Mathlib/Algebra/Category/CommBialgCat.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ universe v u
2727
variable {R : Type u} [CommRing R]
2828

2929
variable (R) in
30+
set_option backward.privateInPublic true in
3031
/-- The category of commutative `R`-bialgebras and their morphisms. -/
3132
structure CommBialgCat where
3233
private mk ::
@@ -48,6 +49,8 @@ instance : CoeSort (CommBialgCat R) (Type v) := ⟨carrier⟩
4849
attribute [coe] CommBialgCat.carrier
4950

5051
variable (R) in
52+
set_option backward.privateInPublic true in
53+
set_option backward.privateInPublic.warn false in
5154
/-- Turn an unbundled `R`-bialgebra into the corresponding object in the category of `R`-bialgebras.
5255
5356
This is the preferred way to construct a term of `CommBialgCat R`. -/
@@ -56,18 +59,23 @@ abbrev of (X : Type v) [CommRing X] [Bialgebra R X] : CommBialgCat.{v} R := ⟨X
5659
variable (R) in
5760
lemma coe_of (X : Type v) [CommRing X] [Bialgebra R X] : (of R X : Type v) = X := rfl
5861

62+
set_option backward.privateInPublic true in
5963
/-- The type of morphisms in `CommBialgCat R`. -/
6064
@[ext]
6165
structure Hom (A B : CommBialgCat.{v} R) where
6266
private mk ::
6367
/-- The underlying bialgebra map. -/
6468
hom' : A →ₐc[R] B
6569

70+
set_option backward.privateInPublic true in
71+
set_option backward.privateInPublic.warn false in
6672
instance : Category (CommBialgCat.{v} R) where
6773
Hom A B := Hom A B
6874
id A := ⟨.id R A⟩
6975
comp f g := ⟨g.hom'.comp f.hom'⟩
7076

77+
set_option backward.privateInPublic true in
78+
set_option backward.privateInPublic.warn false in
7179
instance : ConcreteCategory (CommBialgCat.{v} R) (· →ₐc[R] ·) where
7280
hom := Hom.hom'
7381
ofHom := Hom.mk

‎Mathlib/Algebra/Category/FGModuleCat/Basic.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -247,20 +247,24 @@ theorem FGModuleCatEvaluation_apply' (f : FGModuleCatDual K V) (x : V) :
247247
(FGModuleCatEvaluation K V).hom.hom (f ⊗ₜ x) = f.toFun x :=
248248
contractLeft_apply f x
249249

250+
set_option backward.privateInPublic true in
250251
private theorem coevaluation_evaluation :
251252
letI V' : FGModuleCat K := FGModuleCatDual K V
252253
V' ◁ FGModuleCatCoevaluation K V ≫ (α_ V' V V').inv ≫ FGModuleCatEvaluation K V ▷ V' =
253254
(ρ_ V').hom ≫ (λ_ V').inv := by
254255
ext : 1
255256
apply contractLeft_assoc_coevaluation K V
256257

258+
set_option backward.privateInPublic true in
257259
private theorem evaluation_coevaluation :
258260
FGModuleCatCoevaluation K V ▷ V ≫
259261
(α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V =
260262
(λ_ V).hom ≫ (ρ_ V).inv := by
261263
ext : 1
262264
apply contractLeft_assoc_coevaluation' K V
263265

266+
set_option backward.privateInPublic true in
267+
set_option backward.privateInPublic.warn false in
264268
instance exactPairing : ExactPairing V (FGModuleCatDual K V) where
265269
coevaluation' := FGModuleCatCoevaluation K V
266270
evaluation' := FGModuleCatEvaluation K V

‎Mathlib/Algebra/Category/Grp/Basic.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@ structure AddGrpCat.Hom (A B : AddGrpCat.{u}) where
6767
/-- The underlying monoid homomorphism. -/
6868
hom' : A →+ B
6969

70+
set_option backward.privateInPublic true in
7071
/-- The type of morphisms in `GrpCat R`. -/
7172
@[to_additive, ext]
7273
structure GrpCat.Hom (A B : GrpCat.{u}) where
@@ -76,12 +77,16 @@ structure GrpCat.Hom (A B : GrpCat.{u}) where
7677

7778
namespace GrpCat
7879

80+
set_option backward.privateInPublic true in
81+
set_option backward.privateInPublic.warn false in
7982
@[to_additive]
8083
instance : Category GrpCat.{u} where
8184
Hom X Y := Hom X Y
8285
id X := ⟨MonoidHom.id X⟩
8386
comp f g := ⟨g.hom'.comp f.hom'⟩
8487

88+
set_option backward.privateInPublic true in
89+
set_option backward.privateInPublic.warn false in
8590
@[to_additive]
8691
instance : ConcreteCategory GrpCat (· →* ·) where
8792
hom := Hom.hom'
@@ -276,6 +281,7 @@ structure AddCommGrpCat.Hom (A B : AddCommGrpCat.{u}) where
276281
/-- The underlying monoid homomorphism. -/
277282
hom' : A →+ B
278283

284+
set_option backward.privateInPublic true in
279285
/-- The type of morphisms in `CommGrpCat R`. -/
280286
@[to_additive, ext]
281287
structure CommGrpCat.Hom (A B : CommGrpCat.{u}) where
@@ -285,12 +291,16 @@ structure CommGrpCat.Hom (A B : CommGrpCat.{u}) where
285291

286292
namespace CommGrpCat
287293

294+
set_option backward.privateInPublic true in
295+
set_option backward.privateInPublic.warn false in
288296
@[to_additive]
289297
instance : Category CommGrpCat.{u} where
290298
Hom X Y := Hom X Y
291299
id X := ⟨MonoidHom.id X⟩
292300
comp f g := ⟨g.hom'.comp f.hom'⟩
293301

302+
set_option backward.privateInPublic true in
303+
set_option backward.privateInPublic.warn false in
294304
@[to_additive]
295305
instance : ConcreteCategory CommGrpCat (· →* ·) where
296306
hom := Hom.hom'

‎Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,10 @@ namespace leftExactFunctorForgetEquivalence
4646
attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
4747
attribute [local instance] AddCommGrpCat.cartesianMonoidalCategoryAddCommGrp
4848

49+
set_option backward.privateInPublic true in
4950
private noncomputable local instance : CartesianMonoidalCategory C := .ofHasFiniteProducts
5051

52+
set_option backward.privateInPublic true in
5153
private noncomputable local instance : BraidedCategory C := .ofCartesianMonoidalCategory
5254

5355
/-- Implementation, see `leftExactFunctorForgetEquivalence`. -/

‎Mathlib/Algebra/Category/HopfAlgCat/Basic.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ universe v u
2626

2727
variable (R : Type u) [CommRing R]
2828

29+
set_option backward.privateInPublic true in
2930
/-- The category of `R`-Hopf algebras. -/
3031
structure HopfAlgCat where
3132
private mk ::
@@ -46,6 +47,8 @@ instance : CoeSort (HopfAlgCat.{v} R) (Type v) :=
4647
⟨(·.carrier)⟩
4748

4849
variable (R) in
50+
set_option backward.privateInPublic true in
51+
set_option backward.privateInPublic.warn false in
4952
/-- The object in the category of `R`-Hopf algebras associated to an `R`-Hopf algebra. -/
5053
abbrev of (X : Type v) [Ring X] [HopfAlgebra R X] :
5154
HopfAlgCat R where

‎Mathlib/Algebra/Category/ModuleCat/Basic.lean‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ universe v u
4646

4747
variable (R : Type u) [Ring R]
4848

49+
set_option backward.privateInPublic true in
4950
/-- The category of R-modules and their morphisms.
5051
5152
Note that in the case of `R = ℤ`, we cannot
@@ -68,6 +69,8 @@ instance : CoeSort (ModuleCat.{v} R) (Type v) :=
6869

6970
attribute [coe] ModuleCat.carrier
7071

72+
set_option backward.privateInPublic true in
73+
set_option backward.privateInPublic.warn false in
7174
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
7275
typeclasses. This is the preferred way to construct a term of `ModuleCat R`. -/
7376
abbrev of (X : Type v) [AddCommGroup X] [Module R X] : ModuleCat.{v} R :=
@@ -80,6 +83,7 @@ lemma coe_of (X : Type v) [Ring X] [Module R X] : (of R X : Type v) = X :=
8083
example (X : Type v) [Ring X] [Module R X] : (of R X : Type v) = X := by with_reducible rfl
8184
example (M : ModuleCat.{v} R) : of R M = M := by with_reducible rfl
8285

86+
set_option backward.privateInPublic true in
8387
variable {R} in
8488
/-- The type of morphisms in `ModuleCat R`. -/
8589
@[ext]
@@ -88,11 +92,15 @@ structure Hom (M N : ModuleCat.{v} R) where
8892
/-- The underlying linear map. -/
8993
hom' : M →ₗ[R] N
9094

95+
set_option backward.privateInPublic true in
96+
set_option backward.privateInPublic.warn false in
9197
instance moduleCategory : Category.{v, max (v + 1) u} (ModuleCat.{v} R) where
9298
Hom M N := Hom M N
9399
id _ := ⟨LinearMap.id⟩
94100
comp f g := ⟨g.hom'.comp f.hom'⟩
95101

102+
set_option backward.privateInPublic true in
103+
set_option backward.privateInPublic.warn false in
96104
instance : ConcreteCategory (ModuleCat.{v} R) (· →ₗ[R] ·) where
97105
hom := Hom.hom'
98106
ofHom := Hom.mk
@@ -186,6 +194,8 @@ def homEquiv {M N : ModuleCat.{v} R} : (M ⟶ N) ≃ (M →ₗ[R] N) where
186194
toFun := Hom.hom
187195
invFun := ofHom
188196

197+
set_option backward.privateInPublic true in
198+
set_option backward.privateInPublic.warn false in
189199
/-- The categorical equivalence between `ModuleCat` and `SemimoduleCat`.
190200
191201
In the inverse direction, data (such as the negation operation) is created which may lead to
@@ -306,31 +316,43 @@ section AddCommGroup
306316

307317
variable {M N : ModuleCat.{v} R}
308318

319+
set_option backward.privateInPublic true in
320+
set_option backward.privateInPublic.warn false in
309321
instance : Add (M ⟶ N) where
310322
add f g := ⟨f.hom + g.hom⟩
311323

312324
@[simp] lemma hom_add (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom := rfl
313325

326+
set_option backward.privateInPublic true in
327+
set_option backward.privateInPublic.warn false in
314328
instance : Zero (M ⟶ N) where
315329
zero := ⟨0⟩
316330

317331
@[simp] lemma hom_zero : (0 : M ⟶ N).hom = 0 := rfl
318332

333+
set_option backward.privateInPublic true in
334+
set_option backward.privateInPublic.warn false in
319335
instance : SMul ℕ (M ⟶ N) where
320336
smul n f := ⟨n • f.hom⟩
321337

322338
@[simp] lemma hom_nsmul (n : ℕ) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl
323339

340+
set_option backward.privateInPublic true in
341+
set_option backward.privateInPublic.warn false in
324342
instance : Neg (M ⟶ N) where
325343
neg f := ⟨-f.hom⟩
326344

327345
@[simp] lemma hom_neg (f : M ⟶ N) : (-f).hom = -f.hom := rfl
328346

347+
set_option backward.privateInPublic true in
348+
set_option backward.privateInPublic.warn false in
329349
instance : Sub (M ⟶ N) where
330350
sub f g := ⟨f.hom - g.hom⟩
331351

332352
@[simp] lemma hom_sub (f g : M ⟶ N) : (f - g).hom = f.hom - g.hom := rfl
333353

354+
set_option backward.privateInPublic true in
355+
set_option backward.privateInPublic.warn false in
334356
instance : SMul ℤ (M ⟶ N) where
335357
smul n f := ⟨n • f.hom⟩
336358

@@ -375,6 +397,8 @@ section SMul
375397

376398
variable {M N : ModuleCat.{v} R} {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
377399

400+
set_option backward.privateInPublic true in
401+
set_option backward.privateInPublic.warn false in
378402
instance : SMul S (M ⟶ N) where
379403
smul c f := ⟨c • f.hom⟩
380404

@@ -439,10 +463,14 @@ instance : Linear S (ModuleCat.{v} S) := ModuleCat.Algebra.instLinear
439463

440464
variable {X Y X' Y' : ModuleCat.{v} S}
441465

466+
set_option backward.privateInPublic true in
467+
set_option backward.privateInPublic.warn false in
442468
theorem Iso.homCongr_eq_arrowCongr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) :
443469
Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr i.toLinearEquiv j.toLinearEquiv f.hom⟩ :=
444470
rfl
445471

472+
set_option backward.privateInPublic true in
473+
set_option backward.privateInPublic.warn false in
446474
theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) :
447475
Iso.conj i f = ⟨LinearEquiv.conj i.toLinearEquiv f.hom⟩ :=
448476
rfl
@@ -504,6 +532,8 @@ instance : AddCommGroup (mkOfSMul' φ) := by
504532
dsimp only [mkOfSMul']
505533
infer_instance
506534

535+
set_option backward.privateInPublic true in
536+
set_option backward.privateInPublic.warn false in
507537
instance : SMul R (mkOfSMul' φ) := ⟨fun r (x : A) => (show A ⟶ A from φ r) x⟩
508538

509539
@[simp]
@@ -534,6 +564,8 @@ variable {M N}
534564
(forget₂ (ModuleCat R) AddCommGrpCat).obj N)
535565
(hφ : ∀ (r : R), φ ≫ N.smul r = M.smul r ≫ φ)
536566

567+
set_option backward.privateInPublic true in
568+
set_option backward.privateInPublic.warn false in
537569
/-- Constructor for morphisms in `ModuleCat R` which takes as inputs
538570
a morphism between the underlying objects in `AddCommGrpCat` and the compatibility
539571
with the scalar multiplication. -/

0 commit comments

Comments
 (0)