Skip to content

Commit 79c6822

Browse files
mattrobballmattrobball
committed
revisit all places where Type* fails
1 parent e02809f commit 79c6822

47 files changed

Lines changed: 209 additions & 152 deletions

File tree

Some content is hidden

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

‎Mathlib/Algebra/Algebra/Subalgebra/Basic.lean‎

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ variable (S : Subalgebra R A)
104104
instance instSMulMemClass : SMulMemClass (Subalgebra R A) R A where
105105
smul_mem {S} r x hx := (Algebra.smul_def r x).symm ▸ mul_mem (S.algebraMap_mem' r) hx
106106

107-
theorem _root_.algebraMap_mem {S R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
107+
theorem _root_.algebraMap_mem {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
108108
[SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R) :
109109
algebraMap R A r ∈ s :=
110110
Algebra.algebraMap_eq_smul_one (A := A) r ▸ SMulMemClass.smul_mem r (one_mem s)
@@ -184,7 +184,7 @@ protected theorem prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemir
184184
prod_mem h
185185
#align subalgebra.prod_mem Subalgebra.prod_mem
186186

187-
instance {R A : Type _} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A :=
187+
instance {R A : Type*} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A :=
188188
{ Subalgebra.SubsemiringClass with
189189
neg_mem := fun {S x} hx => neg_one_smul R x ▸ S.smul_mem hx _ }
190190

@@ -454,7 +454,7 @@ theorem toSubsemiring_subtype : S.toSubsemiring.subtype = (S.val : S →+* A) :=
454454
#align subalgebra.to_subsemiring_subtype Subalgebra.toSubsemiring_subtype
455455

456456
@[simp]
457-
theorem toSubring_subtype {R A : Type _} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
457+
theorem toSubring_subtype {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
458458
S.toSubring.subtype = (S.val : S →+* A) := rfl
459459
#align subalgebra.to_subring_subtype Subalgebra.toSubring_subtype
460460

@@ -532,12 +532,12 @@ theorem coe_comap (S : Subalgebra R B) (f : A →ₐ[R] B) : (S.comap f : Set A)
532532
rfl
533533
#align subalgebra.coe_comap Subalgebra.coe_comap
534534

535-
instance noZeroDivisors {R A : Type _} [CommSemiring R] [Semiring A] [NoZeroDivisors A]
535+
instance noZeroDivisors {R A : Type*} [CommSemiring R] [Semiring A] [NoZeroDivisors A]
536536
[Algebra R A] (S : Subalgebra R A) : NoZeroDivisors S :=
537537
inferInstanceAs (NoZeroDivisors S.toSubsemiring)
538538
#align subalgebra.no_zero_divisors Subalgebra.noZeroDivisors
539539

540-
instance isDomain {R A : Type _} [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
540+
instance isDomain {R A : Type*} [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
541541
(S : Subalgebra R A) : IsDomain S :=
542542
inferInstanceAs (IsDomain S.toSubring)
543543
#align subalgebra.is_domain Subalgebra.isDomain
@@ -546,7 +546,7 @@ end Subalgebra
546546

547547
namespace Submodule
548548

549-
variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
549+
variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
550550

551551
variable (p : Submodule R A)
552552

@@ -733,7 +733,7 @@ theorem ofInjective_apply (f : A →ₐ[R] B) (hf : Function.Injective f) (x : A
733733
#align alg_equiv.of_injective_apply AlgEquiv.ofInjective_apply
734734

735735
/-- Restrict an algebra homomorphism between fields to an algebra isomorphism -/
736-
noncomputable def ofInjectiveField {E F : Type _} [DivisionRing E] [Semiring F] [Nontrivial F]
736+
noncomputable def ofInjectiveField {E F : Type*} [DivisionRing E] [Semiring F] [Nontrivial F]
737737
[Algebra R E] [Algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] f.range :=
738738
ofInjective f f.toRingHom.injective
739739
#align alg_equiv.of_injective_field AlgEquiv.ofInjectiveField
@@ -798,7 +798,7 @@ theorem top_toSubsemiring : (⊤ : Subalgebra R A).toSubsemiring = ⊤ := rfl
798798
#align algebra.top_to_subsemiring Algebra.top_toSubsemiring
799799

800800
@[simp]
801-
theorem top_toSubring {R A : Type _} [CommRing R] [Ring A] [Algebra R A] :
801+
theorem top_toSubring {R A : Type*} [CommRing R] [Ring A] [Algebra R A] :
802802
(⊤ : Subalgebra R A).toSubring = ⊤ := rfl
803803
#align algebra.top_to_subring Algebra.top_toSubring
804804

@@ -813,7 +813,7 @@ theorem toSubsemiring_eq_top {S : Subalgebra R A} : S.toSubsemiring = ⊤ ↔ S
813813
#align algebra.to_subsemiring_eq_top Algebra.toSubsemiring_eq_top
814814

815815
@[simp]
816-
theorem toSubring_eq_top {R A : Type _} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} :
816+
theorem toSubring_eq_top {R A : Type*} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} :
817817
S.toSubring = ⊤ ↔ S = ⊤ :=
818818
Subalgebra.toSubring_injective.eq_iff' top_toSubring
819819
#align algebra.to_subring_eq_top Algebra.toSubring_eq_top
@@ -955,7 +955,7 @@ theorem surjective_algebraMap_iff :
955955
fun h y => Algebra.mem_bot.1 <| eq_bot_iff.1 h (Algebra.mem_top : y ∈ _)⟩
956956
#align algebra.surjective_algebra_map_iff Algebra.surjective_algebraMap_iff
957957

958-
theorem bijective_algebraMap_iff {R A : Type _} [Field R] [Semiring A] [Nontrivial A]
958+
theorem bijective_algebraMap_iff {R A : Type*} [Field R] [Semiring A] [Nontrivial A]
959959
[Algebra R A] : Function.Bijective (algebraMap R A) ↔ (⊤ : Subalgebra R A) = ⊥ :=
960960
⟨fun h => surjective_algebraMap_iff.1 h.2, fun h =>
961961
⟨(algebraMap R A).injective, surjective_algebraMap_iff.2 h⟩⟩
@@ -973,7 +973,7 @@ noncomputable def botEquivOfInjective (h : Function.Injective (algebraMap R A))
973973

974974
/-- The bottom subalgebra is isomorphic to the field. -/
975975
@[simps! symm_apply]
976-
noncomputable def botEquiv (F R : Type _) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
976+
noncomputable def botEquiv (F R : Type*) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
977977
(⊥ : Subalgebra F R) ≃ₐ[F] F :=
978978
botEquivOfInjective (RingHom.injective _)
979979
#align algebra.bot_equiv Algebra.botEquiv
@@ -1146,7 +1146,7 @@ end Prod
11461146

11471147
section SuprLift
11481148

1149-
variable {ι : Type _}
1149+
variable {ι : Type*}
11501150

11511151
theorem coe_iSup_of_directed [Nonempty ι] {S : ι → Subalgebra R A} (dir : Directed (· ≤ ·) S) :
11521152
↑(iSup S) = ⋃ i, (S i : Set A) :=
@@ -1246,7 +1246,7 @@ These are just copies of the definitions about `Subsemiring` starting from
12461246

12471247
section Actions
12481248

1249-
variable {α β : Type _}
1249+
variable {α β : Type*}
12501250

12511251
/-- The action by a subalgebra is the action by the underlying algebra. -/
12521252
instance [SMul A α] (S : Subalgebra R A) : SMul S α :=
@@ -1271,7 +1271,7 @@ instance isScalarTower_left [SMul α β] [SMul A α] [SMul A β] [IsScalarTower
12711271
inferInstanceAs (IsScalarTower S.toSubsemiring α β)
12721272
#align subalgebra.is_scalar_tower_left Subalgebra.isScalarTower_left
12731273

1274-
instance isScalarTower_mid {R S T : Type _} [CommSemiring R] [Semiring S] [AddCommMonoid T]
1274+
instance isScalarTower_mid {R S T : Type*} [CommSemiring R] [Semiring S] [AddCommMonoid T]
12751275
[Algebra R S] [Module R T] [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) :
12761276
IsScalarTower R S' T :=
12771277
⟨fun _x y _z => (smul_assoc _ (y : S) _ : _)⟩
@@ -1302,25 +1302,25 @@ instance moduleLeft [AddCommMonoid α] [Module A α] (S : Subalgebra R A) : Modu
13021302
#align subalgebra.module_left Subalgebra.moduleLeft
13031303

13041304
/-- The action by a subalgebra is the action by the underlying algebra. -/
1305-
instance toAlgebra {R A : Type _} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
1305+
instance toAlgebra {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
13061306
[Algebra A α] (S : Subalgebra R A) : Algebra S α :=
13071307
Algebra.ofSubsemiring S.toSubsemiring
13081308
#align subalgebra.to_algebra Subalgebra.toAlgebra
13091309

1310-
theorem algebraMap_eq {R A : Type _} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
1310+
theorem algebraMap_eq {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
13111311
[Algebra A α] (S : Subalgebra R A) : algebraMap S α = (algebraMap A α).comp S.val :=
13121312
rfl
13131313
#align subalgebra.algebra_map_eq Subalgebra.algebraMap_eq
13141314

13151315
@[simp]
1316-
theorem rangeS_algebraMap {R A : Type _} [CommSemiring R] [CommSemiring A] [Algebra R A]
1316+
theorem rangeS_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
13171317
(S : Subalgebra R A) : (algebraMap S A).rangeS = S.toSubsemiring := by
13181318
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubsemiring_subtype,
13191319
Subsemiring.rangeS_subtype]
13201320
#align subalgebra.srange_algebra_map Subalgebra.rangeS_algebraMap
13211321

13221322
@[simp]
1323-
theorem range_algebraMap {R A : Type _} [CommRing R] [CommRing A] [Algebra R A]
1323+
theorem range_algebraMap {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
13241324
(S : Subalgebra R A) : (algebraMap S A).range = S.toSubring := by
13251325
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubring_subtype,
13261326
Subring.range_subtype]
@@ -1358,13 +1358,13 @@ theorem center_toSubsemiring : (center R A).toSubsemiring = Subsemiring.center A
13581358
#align subalgebra.center_to_subsemiring Subalgebra.center_toSubsemiring
13591359

13601360
@[simp]
1361-
theorem center_toSubring (R A : Type _) [CommRing R] [Ring A] [Algebra R A] :
1361+
theorem center_toSubring (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
13621362
(center R A).toSubring = Subring.center A :=
13631363
rfl
13641364
#align subalgebra.center_to_subring Subalgebra.center_toSubring
13651365

13661366
@[simp]
1367-
theorem center_eq_top (A : Type _) [CommSemiring A] [Algebra R A] : center R A = ⊤ :=
1367+
theorem center_eq_top (A : Type*) [CommSemiring A] [Algebra R A] : center R A = ⊤ :=
13681368
SetLike.coe_injective (Set.center_eq_univ A)
13691369
#align subalgebra.center_eq_top Subalgebra.center_eq_top
13701370

@@ -1373,7 +1373,7 @@ variable {R A}
13731373
instance : CommSemiring (center R A) :=
13741374
inferInstanceAs (CommSemiring (Subsemiring.center A))
13751375

1376-
instance {A : Type _} [Ring A] [Algebra R A] : CommRing (center R A) :=
1376+
instance {A : Type*} [Ring A] [Algebra R A] : CommRing (center R A) :=
13771377
inferInstanceAs (CommRing (Subring.center A))
13781378

13791379
theorem mem_center_iff {a : A} : a ∈ center R A ↔ ∀ b : A, b * a = a * b :=
@@ -1429,8 +1429,8 @@ end Centralizer
14291429
/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` in `S`, and `S'` a subalgebra of `S` that contains
14301430
`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
14311431
`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
1432-
theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Algebra R S]
1433-
(S' : Subalgebra R S) {ι : Type _} (ι' : Finset ι) (s : ι → S) (l : ι → S)
1432+
theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type*} [CommRing S] [Algebra R S]
1433+
(S' : Subalgebra R S) {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S)
14341434
(e : ∑ i in ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
14351435
(H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
14361436
-- Porting note: needed to add this instance
@@ -1460,7 +1460,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Alge
14601460
exact ⟨⟨_, hn i⟩, rfl⟩
14611461
#align subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem
14621462

1463-
theorem mem_of_span_eq_top_of_smul_pow_mem {S : Type _} [CommRing S] [Algebra R S]
1463+
theorem mem_of_span_eq_top_of_smul_pow_mem {S : Type*} [CommRing S] [Algebra R S]
14641464
(S' : Subalgebra R S) (s : Set S) (l : s →₀ S) (hs : Finsupp.total s S S (↑) l = 1)
14651465
(hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
14661466
x ∈ S' :=
@@ -1471,7 +1471,7 @@ end Subalgebra
14711471

14721472
section Nat
14731473

1474-
variable {R : Type _} [Semiring R]
1474+
variable {R : Type*} [Semiring R]
14751475

14761476
/-- A subsemiring is an `ℕ`-subalgebra. -/
14771477
def subalgebraOfSubsemiring (S : Subsemiring R) : Subalgebra ℕ R :=
@@ -1488,7 +1488,7 @@ end Nat
14881488

14891489
section Int
14901490

1491-
variable {R : Type _} [Ring R]
1491+
variable {R : Type*} [Ring R]
14921492

14931493
/-- A subring is a `ℤ`-subalgebra. -/
14941494
def subalgebraOfSubring (S : Subring R) : Subalgebra ℤ R :=
@@ -1501,7 +1501,7 @@ def subalgebraOfSubring (S : Subring R) : Subalgebra ℤ R :=
15011501
exact S.sub_mem ih S.one_mem }
15021502
#align subalgebra_of_subring subalgebraOfSubring
15031503

1504-
variable {S : Type _} [Semiring S]
1504+
variable {S : Type*} [Semiring S]
15051505

15061506
@[simp]
15071507
theorem mem_subalgebraOfSubring {x : R} {S : Subring R} : x ∈ subalgebraOfSubring S ↔ x ∈ S :=

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ set_option linter.uppercaseLean3 false in
103103
#align SemiRing.coe_of SemiRingCat.coe_of
104104

105105
@[simp]
106-
lemma RingEquiv_coe_eq {X Y : Type _} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
106+
lemma RingEquiv_coe_eq {X Y : Type u} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
107107
(@FunLike.coe (SemiRingCat.of X ⟶ SemiRingCat.of Y) _ (fun _ => (forget SemiRingCat).obj _)
108108
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
109109
rfl
@@ -242,7 +242,7 @@ set_option linter.uppercaseLean3 false in
242242
#align Ring.coe_of RingCat.coe_of
243243

244244
@[simp]
245-
lemma RingEquiv_coe_eq {X Y : Type _} [Ring X] [Ring Y] (e : X ≃+* Y) :
245+
lemma RingEquiv_coe_eq {X Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
246246
(@FunLike.coe (RingCat.of X ⟶ RingCat.of Y) _ (fun _ => (forget RingCat).obj _)
247247
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
248248
rfl
@@ -325,7 +325,7 @@ set_option linter.uppercaseLean3 false in
325325
#align CommSemiRing.of_hom CommSemiRingCat.ofHom
326326

327327
@[simp]
328-
lemma RingEquiv_coe_eq {X Y : Type _} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
328+
lemma RingEquiv_coe_eq {X Y : Type u} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
329329
(@FunLike.coe (CommSemiRingCat.of X ⟶ CommSemiRingCat.of Y) _
330330
(fun _ => (forget CommSemiRingCat).obj _)
331331
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
@@ -441,7 +441,7 @@ set_option linter.uppercaseLean3 false in
441441
#align CommRing.of_hom CommRingCat.ofHom
442442

443443
@[simp]
444-
lemma RingEquiv_coe_eq {X Y : Type _} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
444+
lemma RingEquiv_coe_eq {X Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
445445
(@FunLike.coe (CommRingCat.of X ⟶ CommRingCat.of Y) _ (fun _ => (forget CommRingCat).obj _)
446446
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
447447
rfl
@@ -600,7 +600,7 @@ theorem CommRingCat.comp_eq_ring_hom_comp {R S T : CommRingCat} (f : R ⟶ S) (g
600600
set_option linter.uppercaseLean3 false in
601601
#align CommRing.comp_eq_ring_hom_comp CommRingCat.comp_eq_ring_hom_comp
602602

603-
theorem CommRingCat.ringHom_comp_eq_comp {R S T : Type _} [CommRing R] [CommRing S] [CommRing T]
603+
theorem CommRingCat.ringHom_comp_eq_comp {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
604604
(f : R →+* S) (g : S →+* T) : g.comp f = CommRingCat.ofHom f ≫ CommRingCat.ofHom g :=
605605
rfl
606606
set_option linter.uppercaseLean3 false in

‎Mathlib/Algebra/Category/Ring/Instances.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ import Mathlib.RingTheory.Ideal.LocalRing
1313
# Ring-theoretic results in terms of categorical languages
1414
-/
1515

16+
universe u
1617

1718
open CategoryTheory
1819

@@ -27,7 +28,7 @@ instance localization_unit_isIso' (R : CommRingCat) :
2728
exact localization_unit_isIso _
2829
#align localization_unit_is_iso' localization_unit_isIso'
2930

30-
theorem IsLocalization.epi {R : Type*} [CommRing R] (M : Submonoid R) (S : Type _) [CommRing S]
31+
theorem IsLocalization.epi {R : Type u} [CommRing R] (M : Submonoid R) (S : Type u) [CommRing S]
3132
[Algebra R S] [IsLocalization M S] : Epi (CommRingCat.ofHom <| algebraMap R S) :=
3233
⟨fun {T} _ _ => @IsLocalization.ringHom_ext R _ M S _ _ T _ _ _ _⟩
3334
#align is_localization.epi IsLocalization.epi

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ theorem coe_of (R : Type u) [Mul R] : (MagmaCat.of R : Type u) = R :=
9797
#align AddMagma.coe_of AddMagmaCat.coe_of
9898

9999
@[to_additive (attr := simp)]
100-
lemma MulEquiv_coe_eq {X Y : Type _} [Mul X] [Mul Y] (e : X ≃* Y) :
100+
lemma MulEquiv_coe_eq {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) :
101101
(@FunLike.coe (MagmaCat.of X ⟶ MagmaCat.of Y) _ (fun _ => (forget MagmaCat).obj _)
102102
ConcreteCategory.funLike (e : X →ₙ* Y) : X → Y) = ↑e :=
103103
rfl
@@ -182,7 +182,7 @@ theorem coe_of (R : Type u) [Semigroup R] : (SemigroupCat.of R : Type u) = R :=
182182
#align AddSemigroup.coe_of AddSemigroupCat.coe_of
183183

184184
@[to_additive (attr := simp)]
185-
lemma MulEquiv_coe_eq {X Y : Type _} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
185+
lemma MulEquiv_coe_eq {X Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
186186
(@FunLike.coe (SemigroupCat.of X ⟶ SemigroupCat.of Y) _ (fun _ => (forget SemigroupCat).obj _)
187187
ConcreteCategory.funLike (e : X →ₙ* Y) : X → Y) = ↑e :=
188188
rfl

‎Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ Then we establish that `Proj 𝒜` is a `LocallyRingedSpace`:
4747
4848
-/
4949

50+
universe ur ua
5051

5152
noncomputable section
5253

@@ -56,7 +57,7 @@ open scoped DirectSum BigOperators Pointwise
5657

5758
open DirectSum SetLike Localization TopCat TopologicalSpace CategoryTheory Opposite
5859

59-
variable {R A : Type*}
60+
variable {R : Type ur} {A : Type ua}
6061

6162
variable [CommRing R] [CommRing A] [Algebra R A]
6263

@@ -188,7 +189,7 @@ end
188189

189190
/-- The structure sheaf (valued in `Type`, not yet `CommRing`) is the subsheaf consisting of
190191
functions satisfying `isLocallyFraction`.-/
191-
def structureSheafInType : Sheaf (Type _) (ProjectiveSpectrum.top 𝒜) :=
192+
def structureSheafInType : Sheaf (Type ua) (ProjectiveSpectrum.top 𝒜) :=
192193
subsheafToTypes (isLocallyFraction 𝒜)
193194
#align algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType
194195

‎Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,8 @@ theorem paths_homotopic {x y : X} (p₁ p₂ : Path x y) : Path.Homotopic p₁ p
6767
Quotient.eq.mp (@Subsingleton.elim (Path.Homotopic.Quotient x y) _ _ _)
6868
#align simply_connected_space.paths_homotopic SimplyConnectedSpace.paths_homotopic
6969

70-
instance (priority := 100) ofContractible (Y : Type _) [TopologicalSpace Y] [ContractibleSpace Y] :
70+
-- FIXME: I should be universe polymorphic in Y
71+
instance (priority := 100) ofContractible (Y : Type) [TopologicalSpace Y] [ContractibleSpace Y] :
7172
SimplyConnectedSpace Y where
7273
equiv_unit :=
7374
let H : TopCat.of Y ≃ₕ TopCat.of Unit := (ContractibleSpace.hequiv_unit Y).some

‎Mathlib/CategoryTheory/Monoidal/Preadditive.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,7 @@ theorem rightDistributor_assoc {J : Type} [Fintype J] (f : J → C) (X Y : C) :
256256
simp only [← tensor_id, associator_inv_naturality, Iso.hom_inv_id_assoc]
257257
#align category_theory.right_distributor_assoc CategoryTheory.rightDistributor_assoc
258258

259-
theorem leftDistributor_rightDistributor_assoc {J : Type _} [Fintype J]
259+
theorem leftDistributor_rightDistributor_assoc {J : Type} [Fintype J]
260260
(X : C) (f : J → C) (Y : C) :
261261
(leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor _ Y =
262262
α_ X (⨁ f) Y ≪≫

‎Mathlib/CategoryTheory/Monoidal/Types/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ theorem associator_inv_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
7474
/-- If `F` is a monoidal functor out of `Type`, it takes the (n+1)st cartesian power
7575
of a type to the image of that type, tensored with the image of the nth cartesian power. -/
7676
noncomputable def MonoidalFunctor.mapPi {C : Type*} [Category C] [MonoidalCategory C]
77-
(F : MonoidalFunctor (Type*) C) (n : ℕ) (β : Type _) :
77+
(F : MonoidalFunctor (Type v) C) (n : ℕ) (β : Type v) :
7878
F.obj (Fin (n + 1) → β) ≅ F.obj β ⊗ F.obj (Fin n → β) :=
7979
Functor.mapIso _ (Equiv.piFinSucc n β).toIso ≪≫ (asIso (F.μ β (Fin n → β))).symm
8080
#align category_theory.monoidal_functor.map_pi CategoryTheory.MonoidalFunctor.mapPi

‎Mathlib/CategoryTheory/Quotient.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ theorem functor_map_eq_iff [h : Congruence r] {X Y : C} (f f' : X ⟶ Y) :
157157
· apply Quotient.sound
158158
#align category_theory.quotient.functor_map_eq_iff CategoryTheory.Quotient.functor_map_eq_iff
159159

160-
variable {D : Type _} [Category D] (F : C ⥤ D)
160+
variable {D : Type*} [Category D] (F : C ⥤ D)
161161
(H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂)
162162

163163
/-- The induced functor on the quotient category. -/

‎Mathlib/CategoryTheory/Sites/Coherent.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ namespace CategoryTheory
3131

3232
open Limits
3333

34-
variable (C : Type*) [Category C]
34+
universe v u
35+
variable (C : Type u) [Category.{v} C]
3536

3637
/--
3738
The condition `Precoherent C` is essentially the minimal condition required to define the

0 commit comments

Comments
 (0)