Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore(CategoryTheory): generalize universes for multiequalizers #17997

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(CategoryTheory): generalize universes for multiequalizers #17997

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7d7d8e2
chore(CategoryTheory): generalize universes for multiequalizers
joelriou Oct 21, 2024
830224b
fix
joelriou Oct 21, 2024
4f5c5e0
fix
joelriou Oct 21, 2024
759a412
Update Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
joelriou Oct 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ wide-pullbacks, wide-pushouts, multiequalizers and cokernels.

-/

universe w v u t r
universe w w' v u t r

namespace CategoryTheory.Limits.Concrete

Expand Down Expand Up @@ -247,9 +247,9 @@ end WidePullback

section Multiequalizer

variable [ConcreteCategory.{max w v} C]
variable [ConcreteCategory.{max w w' v} C]

theorem multiequalizer_ext {I : MulticospanIndex.{w} C} [HasMultiequalizer I]
theorem multiequalizer_ext {I : MulticospanIndex.{w, w'} C} [HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)] (x y : ↑(multiequalizer I))
(h : ∀ t : I.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y) : x = y := by
apply Concrete.limit_ext
Expand All @@ -259,7 +259,7 @@ theorem multiequalizer_ext {I : MulticospanIndex.{w} C} [HasMultiequalizer I]
simp [h]

/-- An auxiliary equivalence to be used in `multiequalizerEquiv` below. -/
def multiequalizerEquivAux (I : MulticospanIndex C) :
def multiequalizerEquivAux (I : MulticospanIndex.{w, w'} C) :
(I.multicospan ⋙ forget C).sections ≃
{ x : ∀ i : I.L, I.left i // ∀ i : I.R, I.fst i (x _) = I.snd i (x _) } where
toFun x :=
Expand Down Expand Up @@ -292,17 +292,17 @@ def multiequalizerEquivAux (I : MulticospanIndex C) :

/-- The equivalence between the noncomputable multiequalizer and
the concrete multiequalizer. -/
noncomputable def multiequalizerEquiv (I : MulticospanIndex.{w} C) [HasMultiequalizer I]
noncomputable def multiequalizerEquiv (I : MulticospanIndex.{w, w'} C) [HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)] :
(multiequalizer I : C) ≃
{ x : ∀ i : I.L, I.left i // ∀ i : I.R, I.fst i (x _) = I.snd i (x _) } :=
letI h1 := limit.isLimit I.multicospan
letI h2 := isLimitOfPreserves (forget C) h1
letI E := h2.conePointUniqueUpToIso (Types.limitConeIsLimit.{w, v} _)
Equiv.trans E.toEquiv (Concrete.multiequalizerEquivAux.{w, v} I)
letI E := h2.conePointUniqueUpToIso (Types.limitConeIsLimit.{max w w', v} _)
Equiv.trans E.toEquiv (Concrete.multiequalizerEquivAux I)

@[simp]
theorem multiequalizerEquiv_apply (I : MulticospanIndex.{w} C) [HasMultiequalizer I]
theorem multiequalizerEquiv_apply (I : MulticospanIndex.{w, w'} C) [HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)] (x : ↑(multiequalizer I)) (i : I.L) :
((Concrete.multiequalizerEquiv I) x : ∀ i : I.L, I.left i) i = Multiequalizer.ι I i x :=
rfl
Expand Down
58 changes: 30 additions & 28 deletions Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,29 +31,29 @@ namespace CategoryTheory.Limits

open CategoryTheory

universe w v u
universe w w' v u

/-- The type underlying the multiequalizer diagram. -/
--@[nolint unused_arguments]
inductive WalkingMulticospan {L R : Type w} (fst snd : R → L) : Type w
inductive WalkingMulticospan {L : Type w} {R : Type w'} (fst snd : R → L) : Type max w w'
| left : L → WalkingMulticospan fst snd
| right : R → WalkingMulticospan fst snd

/-- The type underlying the multiecoqualizer diagram. -/
--@[nolint unused_arguments]
inductive WalkingMultispan {L R : Type w} (fst snd : L → R) : Type w
inductive WalkingMultispan {L : Type w} {R : Type w'} (fst snd : L → R) : Type max w w'
| left : L → WalkingMultispan fst snd
| right : R → WalkingMultispan fst snd

namespace WalkingMulticospan

variable {L R : Type w} {fst snd : R → L}
variable {L : Type w} {R : Type w'} {fst snd : R → L}

instance [Inhabited L] : Inhabited (WalkingMulticospan fst snd) :=
⟨left default⟩

/-- Morphisms for `WalkingMulticospan`. -/
inductive Hom : ∀ _ _ : WalkingMulticospan fst snd, Type w
inductive Hom : ∀ _ _ : WalkingMulticospan fst snd, Type max w w'
| id (A) : Hom A A
| fst (b) : Hom (left (fst b)) (right b)
| snd (b) : Hom (left (snd b)) (right b)
Expand Down Expand Up @@ -94,13 +94,13 @@ end WalkingMulticospan

namespace WalkingMultispan

variable {L R : Type v} {fst snd : L → R}
variable {L : Type w} {R : Type w'} {fst snd : L → R}

instance [Inhabited L] : Inhabited (WalkingMultispan fst snd) :=
⟨left default⟩

/-- Morphisms for `WalkingMultispan`. -/
inductive Hom : ∀ _ _ : WalkingMultispan fst snd, Type v
inductive Hom : ∀ _ _ : WalkingMultispan fst snd, Type max w w'
| id (A) : Hom A A
| fst (a) : Hom (left a) (right (fst a))
| snd (a) : Hom (left a) (right (snd a))
Expand Down Expand Up @@ -139,10 +139,11 @@ lemma Hom.comp_eq_comp {X Y Z : WalkingMultispan fst snd}
end WalkingMultispan

/-- This is a structure encapsulating the data necessary to define a `Multicospan`. -/
-- Porting note(#5171): linter not ported yet
-- @[nolint has_nonempty_instance]
-- Porting note(#5171): has_nonempty_instance linter not ported yet
@[nolint checkUnivs]
structure MulticospanIndex (C : Type u) [Category.{v} C] where
(L R : Type w)
(L : Type w)
(R : Type w')
(fstTo sndTo : R → L)
left : L → C
right : R → C
Expand All @@ -151,9 +152,10 @@ structure MulticospanIndex (C : Type u) [Category.{v} C] where

/-- This is a structure encapsulating the data necessary to define a `Multispan`. -/
-- Porting note(#5171): linter not ported yet
joelriou marked this conversation as resolved.
Show resolved Hide resolved
-- @[nolint has_nonempty_instance]
@[nolint checkUnivs]
structure MultispanIndex (C : Type u) [Category.{v} C] where
(L R : Type w)
(L : Type w)
(R : Type w')
(fstFrom sndFrom : L → R)
left : L → C
right : R → C
Expand All @@ -162,7 +164,7 @@ structure MultispanIndex (C : Type u) [Category.{v} C] where

namespace MulticospanIndex

variable {C : Type u} [Category.{v} C] (I : MulticospanIndex.{w} C)
variable {C : Type u} [Category.{v} C] (I : MulticospanIndex.{w, w'} C)

/-- The multicospan associated to `I : MulticospanIndex`. -/
@[simps]
Expand Down Expand Up @@ -210,7 +212,7 @@ end MulticospanIndex

namespace MultispanIndex

variable {C : Type u} [Category.{v} C] (I : MultispanIndex.{w} C)
variable {C : Type u} [Category.{v} C] (I : MultispanIndex.{w, w'} C)

/-- The multispan associated to `I : MultispanIndex`. -/
def multispan : WalkingMultispan I.fstFrom I.sndFrom ⥤ C where
Expand Down Expand Up @@ -276,18 +278,18 @@ variable {C : Type u} [Category.{v} C]
/-- A multifork is a cone over a multicospan. -/
-- Porting note(#5171): linter not ported yet
-- @[nolint has_nonempty_instance]
abbrev Multifork (I : MulticospanIndex.{w} C) :=
abbrev Multifork (I : MulticospanIndex.{w, w'} C) :=
Cone I.multicospan

/-- A multicofork is a cocone over a multispan. -/
-- Porting note(#5171): linter not ported yet
-- @[nolint has_nonempty_instance]
abbrev Multicofork (I : MultispanIndex.{w} C) :=
abbrev Multicofork (I : MultispanIndex.{w, w'} C) :=
Cocone I.multispan

namespace Multifork

variable {I : MulticospanIndex.{w} C} (K : Multifork I)
variable {I : MulticospanIndex.{w, w'} C} (K : Multifork I)

/-- The maps from the cone point of a multifork to the objects on the left. -/
def ι (a : I.L) : K.pt ⟶ I.left a :=
Expand Down Expand Up @@ -315,7 +317,7 @@ theorem hom_comp_ι (K₁ K₂ : Multifork I) (f : K₁ ⟶ K₂) (j : I.L) : f.

/-- Construct a multifork using a collection `ι` of morphisms. -/
@[simps]
def ofι (I : MulticospanIndex.{w} C) (P : C) (ι : ∀ a, P ⟶ I.left a)
def ofι (I : MulticospanIndex.{w, w'} C) (P : C) (ι : ∀ a, P ⟶ I.left a)
(w : ∀ b, ι (I.fstTo b) ≫ I.fst b = ι (I.sndTo b) ≫ I.snd b) : Multifork I where
pt := P
π :=
Expand Down Expand Up @@ -438,7 +440,7 @@ end Multifork

namespace MulticospanIndex

variable (I : MulticospanIndex.{w} C) [HasProduct I.left] [HasProduct I.right]
variable (I : MulticospanIndex.{w, w'} C) [HasProduct I.left] [HasProduct I.right]

--attribute [local tidy] tactic.case_bash

Expand Down Expand Up @@ -485,7 +487,7 @@ end MulticospanIndex

namespace Multicofork

variable {I : MultispanIndex.{w} C} (K : Multicofork I)
variable {I : MultispanIndex.{w, w'} C} (K : Multicofork I)

/-- The maps to the cocone point of a multicofork from the objects on the right. -/
def π (b : I.R) : I.right b ⟶ K.pt :=
Expand All @@ -511,7 +513,7 @@ lemma π_comp_hom (K₁ K₂ : Multicofork I) (f : K₁ ⟶ K₂) (b : I.R) : K

/-- Construct a multicofork using a collection `π` of morphisms. -/
@[simps]
def ofπ (I : MultispanIndex.{w} C) (P : C) (π : ∀ b, I.right b ⟶ P)
def ofπ (I : MultispanIndex.{w, w'} C) (P : C) (π : ∀ b, I.right b ⟶ P)
(w : ∀ a, I.fst a ≫ π (I.fstFrom a) = I.snd a ≫ π (I.sndFrom a)) : Multicofork I where
pt := P
ι :=
Expand Down Expand Up @@ -614,7 +616,7 @@ end Multicofork

namespace MultispanIndex

variable (I : MultispanIndex.{w} C) [HasCoproduct I.left] [HasCoproduct I.right]
variable (I : MultispanIndex.{w, w'} C) [HasCoproduct I.left] [HasCoproduct I.right]

--attribute [local tidy] tactic.case_bash

Expand Down Expand Up @@ -673,27 +675,27 @@ end MultispanIndex

/-- For `I : MulticospanIndex C`, we say that it has a multiequalizer if the associated
multicospan has a limit. -/
abbrev HasMultiequalizer (I : MulticospanIndex.{w} C) :=
abbrev HasMultiequalizer (I : MulticospanIndex.{w, w'} C) :=
HasLimit I.multicospan

noncomputable section

/-- The multiequalizer of `I : MulticospanIndex C`. -/
abbrev multiequalizer (I : MulticospanIndex.{w} C) [HasMultiequalizer I] : C :=
abbrev multiequalizer (I : MulticospanIndex.{w, w'} C) [HasMultiequalizer I] : C :=
limit I.multicospan

/-- For `I : MultispanIndex C`, we say that it has a multicoequalizer if
the associated multicospan has a limit. -/
abbrev HasMulticoequalizer (I : MultispanIndex.{w} C) :=
abbrev HasMulticoequalizer (I : MultispanIndex.{w, w'} C) :=
HasColimit I.multispan

/-- The multiecoqualizer of `I : MultispanIndex C`. -/
abbrev multicoequalizer (I : MultispanIndex.{w} C) [HasMulticoequalizer I] : C :=
abbrev multicoequalizer (I : MultispanIndex.{w, w'} C) [HasMulticoequalizer I] : C :=
colimit I.multispan

namespace Multiequalizer

variable (I : MulticospanIndex.{w} C) [HasMultiequalizer I]
variable (I : MulticospanIndex.{w, w'} C) [HasMultiequalizer I]

/-- The canonical map from the multiequalizer to the objects on the left. -/
abbrev ι (a : I.L) : multiequalizer I ⟶ I.left a :=
Expand Down Expand Up @@ -758,7 +760,7 @@ end Multiequalizer

namespace Multicoequalizer

variable (I : MultispanIndex.{w} C) [HasMulticoequalizer I]
variable (I : MultispanIndex.{w, w'} C) [HasMulticoequalizer I]

/-- The canonical map from the multiequalizer to the objects on the left. -/
abbrev π (b : I.R) : I.right b ⟶ multicoequalizer I :=
Expand Down
Loading