Skip to content

Commit

Permalink
# This is a combination of 126 commits.
Browse files Browse the repository at this point in the history 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# fix all but one decl

# The commit message #15 will be skipped:

# fix last errors

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# fix some errors

# The commit message #32 will be skipped:

# some more fixes

# The commit message #33 will be skipped:

# more fixes

# The commit message #34 will be skipped:

# finally fixed

# The commit message #35 will be skipped:

# lint

# The commit message #36 will be skipped:

# add porting note for scary warning

# The commit message #37 will be skipped:

# add porting note about proliferation of match

# The commit message #38 will be skipped:

# initial pass

# The commit message #39 will be skipped:

# fix errors

# The commit message #40 will be skipped:

# lint

# The commit message #41 will be skipped:

# fix errors; lint; add porting notes

# The commit message #42 will be skipped:

# fix errors; lint; add porting note

# The commit message #43 will be skipped:

# fix error

# The commit message #44 will be skipped:

# fix some errors

# The commit message #45 will be skipped:

# minor fixes

# The commit message #46 will be skipped:

# fix all but four

# The commit message #47 will be skipped:

# fix last errors; lint

# The commit message #48 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #49 will be skipped:

# Initial file copy from mathport

# The commit message #50 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #51 will be skipped:

# get file to build

# The commit message #52 will be skipped:

# lint

# The commit message #53 will be skipped:

# lint some more

# The commit message #54 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #55 will be skipped:

# Initial file copy from mathport

# The commit message #56 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #57 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #58 will be skipped:

# Initial file copy from mathport

# The commit message #59 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #60 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #61 will be skipped:

# Initial file copy from mathport

# The commit message #62 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #63 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #64 will be skipped:

# Initial file copy from mathport

# The commit message #65 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #66 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #67 will be skipped:

# Initial file copy from mathport

# The commit message #68 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #69 will be skipped:

# first pass

# The commit message #70 will be skipped:

# names and removing restate_axiom

# The commit message #71 will be skipped:

# fix lint

# The commit message #72 will be skipped:

# remove spurious edit

# The commit message #73 will be skipped:

# fix errors; lint

# The commit message #74 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #77 will be skipped:

# Initial file copy from mathport

# The commit message #78 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #79 will be skipped:

# push it as far as possible

# The commit message #80 will be skipped:

# minor changes

# The commit message #81 will be skipped:

# seems to work

# The commit message #82 will be skipped:

# add example and equivalence file for testing

# The commit message #83 will be skipped:

# test: create `slice.lean` test file

# The commit message #84 will be skipped:

# remove equivalence.lean

# The commit message #85 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #86 will be skipped:

# add documentation and clean up

# The commit message #87 will be skipped:

# move iteration tactics to core

# The commit message #88 will be skipped:

# modify documentation lines

# The commit message #89 will be skipped:

# add module documentation(?)

# The commit message #90 will be skipped:

# fix module docs

# The commit message #91 will be skipped:

# fix test/slice.lean

# The commit message #92 will be skipped:

# fix all but refl error

# The commit message #93 will be skipped:

# fix refl error and lint errors

# The commit message #94 will be skipped:

# fix final long line

# The commit message #95 will be skipped:

# use `Mathport` syntax
# * use existing docs
# * fix docs typos

# The commit message #96 will be skipped:

# test: add simple `rhs`/`lhs` tests

# The commit message #97 will be skipped:

# minor changes to `Tactic.Core`
# * use `m` instead of `TacticM` now that we use `MonadExcept`
# * simplify code for `iterateRange`
# * minor docs tweaks

# The commit message #98 will be skipped:

# update slice naming

# The commit message #99 will be skipped:

# some progress

# The commit message #100 will be skipped:

# only one error left

# The commit message #101 will be skipped:

# filled in last sorry

# The commit message #102 will be skipped:

# break long lines

# The commit message #103 will be skipped:

# delete linter command

# The commit message #104 will be skipped:

# fix comments

# The commit message #105 will be skipped:

# fix two simpNF lints

# The commit message #106 will be skipped:

# fill in some docstrings

# The commit message #107 will be skipped:

# fix most linter issues

# The commit message #108 will be skipped:

# add missing aligns for fields; lint

# The commit message #109 will be skipped:

# restore lost import line

# The commit message #110 will be skipped:

# fix errors; lint

# The commit message #111 will be skipped:

# feat: port CategoryTheory.Limits.Shapes.StrongEpi

# The commit message #112 will be skipped:

# Initial file copy from mathport

# The commit message #113 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #114 will be skipped:

# fix errors; lint

# The commit message #115 will be skipped:

# Update Mathlib.lean

# The commit message #116 will be skipped:

# fix errors; lint

# The commit message #117 will be skipped:

# fix errors; lint; shorten filename

# The commit message #118 will be skipped:

# fix some errors

# The commit message #119 will be skipped:

# fix some more

# The commit message #120 will be skipped:

# fix errors

# The commit message #121 will be skipped:

# lint

# The commit message #122 will be skipped:

# fix errors

# The commit message #123 will be skipped:

# lint

# The commit message #124 will be skipped:

# feat: port CategoryTheory.Category.Ulift

# The commit message #125 will be skipped:

# Initial file copy from mathport

# The commit message #126 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean
  • Loading branch information
@mattrobball
mattrobball committed Feb 25, 2023
1 parent e22a9d9 commit 8fcb216
Show file tree
Hide file tree
Showing 20 changed files with 2,550 additions and 391 deletions.
22 changes: 1 addition & 21 deletions Mathlib.lean
View file
Expand Up @@ -223,10 +223,6 @@ import Mathlib.Algebra.Tropical.Basic
import Mathlib.Algebra.Tropical.BigOperators
import Mathlib.Algebra.Tropical.Lattice
import Mathlib.CategoryTheory.Adjunction.Basic
import Mathlib.CategoryTheory.Adjunction.FullyFaithful
import Mathlib.CategoryTheory.Adjunction.Mates
import Mathlib.CategoryTheory.Adjunction.Reflective
import Mathlib.CategoryTheory.Adjunction.Whiskering
import Mathlib.CategoryTheory.Arrow
import Mathlib.CategoryTheory.Balanced
import Mathlib.CategoryTheory.Bicategory.Basic
Expand All @@ -238,16 +234,9 @@ import Mathlib.CategoryTheory.Category.GaloisConnection
import Mathlib.CategoryTheory.Category.KleisliCat
import Mathlib.CategoryTheory.Category.Preorder
import Mathlib.CategoryTheory.Category.RelCat
import Mathlib.CategoryTheory.Category.ULift
import Mathlib.CategoryTheory.CommSq
import Mathlib.CategoryTheory.Category.Ulift
import Mathlib.CategoryTheory.Comma
import Mathlib.CategoryTheory.ConcreteCategory.Bundled
import Mathlib.CategoryTheory.Conj
import Mathlib.CategoryTheory.Core
import Mathlib.CategoryTheory.DiscreteCategory
import Mathlib.CategoryTheory.Endomorphism
import Mathlib.CategoryTheory.EpiMono
import Mathlib.CategoryTheory.EqToHom
import Mathlib.CategoryTheory.Equivalence
import Mathlib.CategoryTheory.EssentialImage
import Mathlib.CategoryTheory.EssentiallySmall
Expand All @@ -265,24 +254,15 @@ import Mathlib.CategoryTheory.Functor.Hom
import Mathlib.CategoryTheory.Functor.InvIsos
import Mathlib.CategoryTheory.Functor.ReflectsIso
import Mathlib.CategoryTheory.Groupoid
import Mathlib.CategoryTheory.Groupoid.Basic
import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.IsomorphismClasses
import Mathlib.CategoryTheory.LiftingProperties.Adjunction
import Mathlib.CategoryTheory.LiftingProperties.Basic
import Mathlib.CategoryTheory.Limits.Cones
import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
import Mathlib.CategoryTheory.Monoidal.Category
import Mathlib.CategoryTheory.Monoidal.Functor
import Mathlib.CategoryTheory.NatIso
import Mathlib.CategoryTheory.NatTrans
import Mathlib.CategoryTheory.Opposites
import Mathlib.CategoryTheory.PEmpty
import Mathlib.CategoryTheory.PUnit
import Mathlib.CategoryTheory.Pi.Basic
import Mathlib.CategoryTheory.Products.Associator
import Mathlib.CategoryTheory.Products.Basic
import Mathlib.CategoryTheory.Products.Bifunctor
import Mathlib.CategoryTheory.Sigma.Basic
import Mathlib.CategoryTheory.Skeletal
import Mathlib.CategoryTheory.Sums.Basic
Expand Down
10 changes: 5 additions & 5 deletions Mathlib/CategoryTheory/Adjunction/Basic.lean
View file
Expand Up @@ -177,14 +177,14 @@ theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
#align category_theory.adjunction.hom_equiv_naturality_right_symm CategoryTheory.Adjunction.homEquiv_naturality_right_symm

@[simp]
theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _ := by
theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = NatTrans.id _ := by
ext; dsimp
erw [← adj.homEquiv_counit, Equiv.symm_apply_eq, adj.homEquiv_unit]
simp
#align category_theory.adjunction.left_triangle CategoryTheory.Adjunction.left_triangle

@[simp]
theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 _ := by
theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = NatTrans.id _ := by
ext; dsimp
erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit]
simp
Expand Down Expand Up @@ -387,10 +387,10 @@ def mkOfUnitCounit (adj : CoreUnitCounit F G) : F ⊣ G :=
exact t } }
#align category_theory.adjunction.mk_of_unit_counit CategoryTheory.Adjunction.mkOfUnitCounit

/- Porting note: simpNF linter claims these are solved by simp but that
/- Porting note: simpNF linter claims these are solved by simp but that
is not true -/
attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply
attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply
attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply
attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply

/-- The adjunction between the identity functor on a category and itself. -/
def id : 𝟭 C ⊣ 𝟭 C where
Expand Down
223 changes: 223 additions & 0 deletions Mathlib/CategoryTheory/Category/Ulift.lean
View file
@@ -0,0 +1,223 @@
/-
Copyright (c) 2021 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz
! This file was ported from Lean 3 source module category_theory.category.ulift
! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Equivalence
import Mathlib.CategoryTheory.EqToHom

/-!
# Basic API for ulift
This file contains a very basic API for working with the categorical
instance on `ulift C` where `C` is a type with a category instance.
1. `category_theory.ulift.up` is the functorial version of the usual `ulift.up`.
2. `category_theory.ulift.down` is the functorial version of the usual `ulift.down`.
3. `category_theory.ulift.equivalence` is the categorical equivalence between
`C` and `ulift C`.
# ulift_hom
Given a type `C : Type u`, `ulift_hom.{w} C` is just an alias for `C`.
If we have `category.{v} C`, then `ulift_hom.{w} C` is endowed with a category instance
whose morphisms are obtained by applying `ulift.{w}` to the morphisms from `C`.
This is a category equivalent to `C`. The forward direction of the equivalence is `ulift_hom.up`,
the backward direction is `ulift_hom.donw` and the equivalence is `ulift_hom.equiv`.
# as_small
This file also contains a construction which takes a type `C : Type u` with a
category instance `category.{v} C` and makes a small category
`as_small.{w} C : Type (max w v u)` equivalent to `C`.
The forward direction of the equivalence, `C ⥤ as_small C`, is denoted `as_small.up`
and the backward direction is `as_small.down`. The equivalence itself is `as_small.equiv`.
-/


universe w₁ v₁ v₂ u₁ u₂

namespace CategoryTheory

variable {C : Type u₁} [Category.{v₁} C]

/-- The functorial version of `ulift.up`. -/
@[simps]
def Ulift.upFunctor : C ⥤ ULift.{u₂} C where
obj := ULift.up
map X Y f := f
#align category_theory.ulift.up_functor CategoryTheory.Ulift.upFunctor

/-- The functorial version of `ulift.down`. -/
@[simps]
def Ulift.downFunctor : ULift.{u₂} C ⥤ C
where
obj := ULift.down
map X Y f := f
#align category_theory.ulift.down_functor CategoryTheory.Ulift.downFunctor

/-- The categorical equivalence between `C` and `ulift C`. -/
@[simps]
def Ulift.equivalence : C ≌ ULift.{u₂} C
where
Functor := Ulift.upFunctor
inverse := Ulift.downFunctor
unitIso :=
{ Hom := 𝟙 _
inv := 𝟙 _ }
counitIso :=
{ Hom :=
{ app := fun X => 𝟙 _
naturality' := fun X Y f => by
change f ≫ 𝟙 _ = 𝟙 _ ≫ f
simp }
inv :=
{ app := fun X => 𝟙 _
naturality' := fun X Y f => by
change f ≫ 𝟙 _ = 𝟙 _ ≫ f
simp }
hom_inv_id' := by
ext
change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
simp
inv_hom_id' := by
ext
change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
simp }
functor_unitIso_comp' X := by
change 𝟙 X ≫ 𝟙 X = 𝟙 X
simp
#align category_theory.ulift.equivalence CategoryTheory.Ulift.equivalence

section UliftHom

/-- `ulift_hom.{w} C` is an alias for `C`, which is endowed with a category instance
whose morphisms are obtained by applying `ulift.{w}` to the morphisms from `C`.
-/
def UliftHom.{w, u} (C : Type u) :=
C
#align category_theory.ulift_hom CategoryTheory.UliftHom

instance {C} [Inhabited C] : Inhabited (UliftHom C) :=
⟨(Inhabited.default C : C)⟩

/-- The obvious function `ulift_hom C → C`. -/
def UliftHom.objDown {C} (A : UliftHom C) : C :=
A
#align category_theory.ulift_hom.obj_down CategoryTheory.UliftHom.objDown

/-- The obvious function `C → ulift_hom C`. -/
def UliftHom.objUp {C} (A : C) : UliftHom C :=
A
#align category_theory.ulift_hom.obj_up CategoryTheory.UliftHom.objUp

@[simp]
theorem objDown_objUp {C} (A : C) : (UliftHom.objUp A).objDown = A :=
rfl
#align category_theory.obj_down_obj_up CategoryTheory.objDown_objUp

@[simp]
theorem objUp_objDown {C} (A : UliftHom C) : UliftHom.objUp A.objDown = A :=
rfl
#align category_theory.obj_up_obj_down CategoryTheory.objUp_objDown

instance : Category.{max v₂ v₁} (UliftHom.{v₂} C)
where
Hom A B := ULift.{v₂} <| A.objDown ⟶ B.objDown
id A := ⟨𝟙 _⟩
comp A B C f g := ⟨f.down ≫ g.down⟩

/-- One half of the quivalence between `C` and `ulift_hom C`. -/
@[simps]
def UliftHom.up : C ⥤ UliftHom C where
obj := UliftHom.objUp
map X Y f := ⟨f⟩
#align category_theory.ulift_hom.up CategoryTheory.UliftHom.up

/-- One half of the quivalence between `C` and `ulift_hom C`. -/
@[simps]
def UliftHom.down : UliftHom C ⥤ C where
obj := UliftHom.objDown
map X Y f := f.down
#align category_theory.ulift_hom.down CategoryTheory.UliftHom.down

/-- The equivalence between `C` and `ulift_hom C`. -/
def UliftHom.equiv : C ≌ UliftHom C
where
Functor := UliftHom.up
inverse := UliftHom.down
unitIso := NatIso.ofComponents (fun A => eqToIso rfl) (by tidy)
counitIso := NatIso.ofComponents (fun A => eqToIso rfl) (by tidy)
#align category_theory.ulift_hom.equiv CategoryTheory.UliftHom.equiv

end UliftHom

/-- `as_small C` is a small category equivalent to `C`.
More specifically, if `C : Type u` is endowed with `category.{v} C`, then
`as_small.{w} C : Type (max w v u)` is endowed with an instance of a small category.
The objects and morphisms of `as_small C` are defined by applying `ulift` to the
objects and morphisms of `C`.
Note: We require a category instance for this definition in order to have direct
access to the universe level `v`.
-/
@[nolint unused_arguments]
def AsSmall.{w, v, u} (C : Type u) [Category.{v} C] :=
ULift.{max w v} C
#align category_theory.as_small CategoryTheory.AsSmall

instance : SmallCategory (AsSmall.{w₁} C)
where
Hom X Y := ULift.{max w₁ u₁} <| X.down ⟶ Y.down
id X := ⟨𝟙 _⟩
comp X Y Z f g := ⟨f.down ≫ g.down⟩

/-- One half of the equivalence between `C` and `as_small C`. -/
@[simps]
def AsSmall.up : C ⥤ AsSmall C where
obj X := ⟨X⟩
map X Y f := ⟨f⟩
#align category_theory.as_small.up CategoryTheory.AsSmall.up

/-- One half of the equivalence between `C` and `as_small C`. -/
@[simps]
def AsSmall.down : AsSmall C ⥤ C where
obj X := X.down
map X Y f := f.down
#align category_theory.as_small.down CategoryTheory.AsSmall.down

/-- The equivalence between `C` and `as_small C`. -/
@[simps]
def AsSmall.equiv : C ≌ AsSmall C where
Functor := AsSmall.up
inverse := AsSmall.down
unitIso := NatIso.ofComponents (fun X => eqToIso rfl) (by tidy)
counitIso :=
NatIso.ofComponents
(fun X =>
eqToIso <| by
ext
rfl)
(by tidy)
#align category_theory.as_small.equiv CategoryTheory.AsSmall.equiv

instance [Inhabited C] : Inhabited (AsSmall C) :=
⟨⟨Inhabited.default _⟩⟩

/-- The equivalence between `C` and `ulift_hom (ulift C)`. -/
def UliftHomUliftCategory.equiv.{v', u', v, u} (C : Type u) [Category.{v} C] :
C ≌ UliftHom.{v'} (ULift.{u'} C) :=
Ulift.equivalence.trans UliftHom.equiv
#align category_theory.ulift_hom_ulift_category.equiv CategoryTheory.UliftHomUliftCategory.equiv

end CategoryTheory

19 changes: 10 additions & 9 deletions Mathlib/CategoryTheory/CommSq.lean
View file
Expand Up @@ -121,7 +121,7 @@ structure LiftStruct (sq : CommSq f i p g) where

namespace LiftStruct

/-- A `LiftStruct` for a commutative square gives a `LiftStruct` for the
/-- A `lift_struct` for a commutative square gives a `lift_struct` for the
corresponding square in the opposite category. -/
@[simps]
def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
Expand All @@ -131,8 +131,8 @@ def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
fac_right := by rw [← op_comp, l.fac_left]
#align category_theory.comm_sq.lift_struct.op CategoryTheory.CommSq.LiftStruct.op

/-- A `LiftStruct` for a commutative square in the opposite category
gives a `LiftStruct` for the corresponding square in the original category. -/
/-- A `lift_struct` for a commutative square in the opposite category
gives a `lift_struct` for the corresponding square in the original category. -/
@[simps]
def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CommSq f i p g}
(l : LiftStruct sq) : LiftStruct sq.unop
Expand All @@ -142,7 +142,7 @@ def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B
fac_right := by rw [← unop_comp, l.fac_left]
#align category_theory.comm_sq.lift_struct.unop CategoryTheory.CommSq.LiftStruct.unop

/-- Equivalences of `LiftStruct` for a square and the corresponding square
/-- Equivalences of `lift_struct` for a square and the corresponding square
in the opposite category. -/
@[simps]
def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
Expand All @@ -153,7 +153,7 @@ def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
right_inv := by aesop_cat
#align category_theory.comm_sq.lift_struct.op_equiv CategoryTheory.CommSq.LiftStruct.opEquiv

/-- Equivalences of `LiftStruct` for a square in the oppositive category and
/-- Equivalences of `lift_struct` for a square in the oppositive category and
the corresponding square in the original category. -/
def unopEquiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
(sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.unop
Expand All @@ -171,7 +171,8 @@ instance subsingleton_liftStruct_of_epi (sq : CommSq f i p g) [Epi i] :
⟨fun l₁ l₂ => by
ext
rw [← cancel_epi i]
simp only [LiftStruct.fac_left]⟩
simp only [LiftStruct.fac_left]
⟩
#align category_theory.comm_sq.subsingleton_lift_struct_of_epi CategoryTheory.CommSq.subsingleton_liftStruct_of_epi

instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
Expand All @@ -185,9 +186,9 @@ instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
variable (sq : CommSq f i p g)


/-- The assertion that a square has a `LiftStruct`. -/
/-- The assertion that a square has a `lift_struct`. -/
class HasLift : Prop where
/-- Square has a `LiftStruct`. -/
/-- Square has a `lift_struct`. -/
exists_lift : Nonempty sq.LiftStruct
#align category_theory.comm_sq.has_lift CategoryTheory.CommSq.HasLift

Expand Down Expand Up @@ -219,7 +220,7 @@ theorem iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {

end HasLift

/-- A choice of a diagonal morphism that is part of a `LiftStruct` when
/-- A choice of a diagonal morphism that is part of a `lift_struct` when
the square has a lift. -/
noncomputable def lift [hsq : HasLift sq] : B ⟶ X :=
hsq.exists_lift.some.l
Expand Down

0 comments on commit 8fcb216

Please sign in to comment.