Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f153a85

Browse files
kim-emkim-em
committed
chore(category_theory/*): fix long lines (#6471)
 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent c7a2d67 commit f153a85

44 files changed

Lines changed: 180 additions & 93 deletions

Some content is hidden

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

‎src/category_theory/abelian/exact.lean‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -67,13 +67,15 @@ begin
6767
{ rw exact_iff,
6868
refine λ h, ⟨h.1, _⟩,
6969
apply zero_of_epi_comp (is_limit.cone_point_unique_up_to_iso hg (limit.is_limit _)).hom,
70-
apply zero_of_comp_mono (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _) hf).hom,
70+
apply zero_of_comp_mono
71+
(is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _) hf).hom,
7172
simp [h.2] }
7273
end
7374

7475
/-- If `(f, g)` is exact, then `images.image.ι f` is a kernel of `g`. -/
7576
def is_limit_image [h : exact f g] :
76-
is_limit (kernel_fork.of_ι (images.image.ι f) (images.image_ι_comp_eq_zero h.1) : kernel_fork g) :=
77+
is_limit
78+
(kernel_fork.of_ι (images.image.ι f) (images.image_ι_comp_eq_zero h.1) : kernel_fork g) :=
7779
begin
7880
rw exact_iff at h,
7981
refine is_limit.of_ι _ _ _ _ _,

‎src/category_theory/abelian/non_preadditive.lean‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -187,11 +187,13 @@ has_colimit.mk
187187
(λ s, (cancel_epi a).1 $
188188
by { rw cokernel_cofork.π_of_π at ha', simp [reassoc_of ha', pushout_cocone.condition s] })
189189
(λ s, (cancel_epi b).1 $ by { rw cokernel_cofork.π_of_π at hb', simp [reassoc_of hb'] })
190-
(λ s m h₁ h₂, (cancel_epi (cokernel.π (coprod.desc f g))).1 $ calc cokernel.π (coprod.desc f g) ≫ m
190+
(λ s m h₁ h₂, (cancel_epi (cokernel.π (coprod.desc f g))).1 $
191+
calc cokernel.π (coprod.desc f g) ≫ m
191192
= (a ≫ a') ≫ m : by { congr, exact ha'.symm }
192193
... = a ≫ pushout_cocone.inl s : by rw [category.assoc, h₁]
193194
... = b ≫ pushout_cocone.inr s : pushout_cocone.condition s
194-
... = cokernel.π (coprod.desc f g) ≫ cokernel.desc (coprod.desc f g) (b ≫ pushout_cocone.inr s) _ :
195+
... = cokernel.π (coprod.desc f g) ≫
196+
cokernel.desc (coprod.desc f g) (b ≫ pushout_cocone.inr s) _ :
195197
by rw cokernel.π_desc) }
196198

197199
section

‎src/category_theory/abelian/pseudoelements.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,8 @@ rfl
169169
with each morphism. Sadly, this is not a definitional equality, but at least it is
170170
true. -/
171171
theorem comp_apply {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (a : P) : (f ≫ g) a = g (f a) :=
172-
quotient.induction_on a $ λ x, quotient.sound $ by { unfold app, rw [←category.assoc, over.coe_hom] }
172+
quotient.induction_on a $ λ x, quotient.sound $
173+
by { unfold app, rw [←category.assoc, over.coe_hom] }
173174

174175
/-- Composition of functions on pseudoelements is composition of morphisms. -/
175176
theorem comp_comp {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) : g ∘ f = f ≫ g :=

‎src/category_theory/adjunction/limits.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,8 @@ The unit for the adjunction for `cocones.functoriality K F : cocone K ⥤ cocone
3939
4040
Auxiliary definition for `functoriality_is_left_adjoint`.
4141
-/
42-
@[simps] def functoriality_unit : 𝟭 (cocone K) ⟶ cocones.functoriality _ F ⋙ functoriality_right_adjoint adj K :=
42+
@[simps] def functoriality_unit :
43+
𝟭 (cocone K) ⟶ cocones.functoriality _ F ⋙ functoriality_right_adjoint adj K :=
4344
{ app := λ c, { hom := adj.unit.app c.X } }
4445

4546
/--

‎src/category_theory/closed/cartesian.lean‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -329,7 +329,12 @@ strict_initial initial_is_initial _
329329

330330
/-- If an initial object `0` exists in a CCC then every morphism from it is monic. -/
331331
lemma initial_mono {I : C} (B : C) (t : is_initial I) [cartesian_closed C] : mono (t.to B) :=
332-
⟨λ B g h _, by { haveI := strict_initial t g, haveI := strict_initial t h, exact eq_of_inv_eq_inv (t.hom_ext _ _) }⟩
332+
⟨λ B g h _,
333+
begin
334+
haveI := strict_initial t g,
335+
haveI := strict_initial t h,
336+
exact eq_of_inv_eq_inv (t.hom_ext _ _)
337+
end⟩
333338

334339
instance initial.mono_to [has_initial C] (B : C) [cartesian_closed C] : mono (initial.to B) :=
335340
initial_mono B initial_is_initial

‎src/category_theory/comma.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,8 @@ comma, slice, coslice, over, under, arrow
4444

4545
namespace category_theory
4646

47-
universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
47+
-- declare the `v`'s first; see `category_theory.category` for an explanation
48+
universes v₁ v₂ v₃ u₁ u₂ u₃
4849
variables {A : Type u₁} [category.{v₁} A]
4950
variables {B : Type u₂} [category.{v₂} B]
5051
variables {T : Type u₃} [category.{v₃} T]

‎src/category_theory/concrete_category/unbundled_hom.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,8 @@ include 𝒞'
4848
variables (obj : Π ⦃α⦄, c α → c' α)
4949
(map : ∀ ⦃α β Iα Iβ f⦄, @hom α β Iα Iβ f → hom' (obj Iα) (obj Iβ) f)
5050

51-
/-- A custom constructor for forgetful functor between concrete categories defined using `unbundled_hom`. -/
51+
/-- A custom constructor for forgetful functor
52+
between concrete categories defined using `unbundled_hom`. -/
5253
def mk_has_forget₂ : has_forget₂ (bundled c) (bundled c') :=
5354
bundled_hom.mk_has_forget₂ obj (λ X Y f, ⟨f.val, map f.property⟩) (λ _ _ _, rfl)
5455

‎src/category_theory/conj.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ An isomorphism `α : X ≅ Y` defines
1313
- a monoid isomorphism `conj : End X ≃* End Y` by `α.conj f = α.inv ≫ f ≫ α.hom`;
1414
- a group isomorphism `conj_Aut : Aut X ≃* Aut Y` by `α.conj_Aut f = α.symm ≪≫ f ≪≫ α`.
1515
16-
For completeness, we also define `hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)`, cf. `equiv.arrow_congr`.
16+
For completeness, we also define `hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)`,
17+
cf. `equiv.arrow_congr`.
1718
-/
1819

1920
universes v u

‎src/category_theory/const.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ Authors: Scott Morrison, Bhavik Mehta
55
-/
66
import category_theory.opposites
77

8-
universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
8+
-- declare the `v`'s first; see `category_theory.category` for an explanation
9+
universes v₁ v₂ v₃ u₁ u₂ u₃
910

1011
open category_theory
1112

‎src/category_theory/filtered.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,8 @@ begin
181181
end
182182

183183
/--
184-
An arbitrary choice of object "to the right" of a finite collection of objects `O` and morphisms `H`,
184+
An arbitrary choice of object "to the right"
185+
of a finite collection of objects `O` and morphisms `H`,
185186
making all the triangles commute.
186187
-/
187188
noncomputable

0 commit comments

Comments
 (0)