doc: turn links to Stacks into stacks attributes (#21046)

I did not touch the links that are in module docs.

Author: YaelDillies

Mathlib/CategoryTheory/Abelian/Basic.lean

@@ -242,11 +242,9 @@ attribute [local instance] OfCoimageImageComparisonIsIso.isNormalEpiCategory
 
 /-- A preadditive category with kernels, cokernels, and finite products,
 in which the coimage-image comparison morphism is always an isomorphism,
-is an abelian category.
-
-The Stacks project uses this characterisation at the definition of an abelian category.
-See <https://stacks.math.columbia.edu/tag/0109>.
--/
+is an abelian category. -/
+@[stacks 0109
+"The Stacks project uses this characterisation at the definition of an abelian category."]
 def ofCoimageImageComparisonIsIso : Abelian C where
 
 end CategoryTheory.Abelian

Mathlib/CategoryTheory/Abelian/Images.lean

@@ -85,10 +85,8 @@ end Coimage
 In any abelian category this is an isomorphism.
 
 Conversely, any additive category with kernels and cokernels and
-in which this is always an isomorphism, is abelian.
-
-See <https://stacks.math.columbia.edu/tag/0107>
--/
+in which this is always an isomorphism, is abelian. -/
+@[stacks 0107]
 def coimageImageComparison : Abelian.coimage f ⟶ Abelian.image f :=
   cokernel.desc (kernel.ι f) (kernel.lift (cokernel.π f) f (by simp)) (by ext; simp)
 

Mathlib/CategoryTheory/Abelian/Transfer.lean

@@ -154,10 +154,8 @@ open AbelianOfAdjunction
 we have `F : C ⥤ D` `G : D ⥤ C` (both preserving zero morphisms),
 `G` is left exact (that is, preserves finite limits),
 and further we have `adj : G ⊣ F` and `i : F ⋙ G ≅ 𝟭 C`,
-then `C` is also abelian.
-
-See <https://stacks.math.columbia.edu/tag/03A3>
--/
+then `C` is also abelian. -/
+@[stacks 03A3]
 def abelianOfAdjunction {C : Type u₁} [Category.{v₁} C] [Preadditive C] [HasFiniteProducts C]
     {D : Type u₂} [Category.{v₂} D] [Abelian D] (F : C ⥤ D) [Functor.PreservesZeroMorphisms F]
     (G : D ⥤ C) [Functor.PreservesZeroMorphisms G] [PreservesFiniteLimits G] (i : F ⋙ G ≅ 𝟭 C)

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -97,10 +97,8 @@ There is also a constructor `Adjunction.mkOfHomEquiv` which constructs an adjunc
 hom set equivalence.
 
 To construct adjoints to a given functor, there are constructors `leftAdjointOfEquiv` and
-`adjunctionOfEquivLeft` (as well as their duals).
-
-See <https://stacks.math.columbia.edu/tag/0037>.
--/
+`adjunctionOfEquivLeft` (as well as their duals). -/
+@[stacks 0037]
 structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where
   /-- The unit of an adjunction -/
   unit : 𝟭 C ⟶ F.comp G
@@ -508,11 +506,8 @@ section
 variable {E : Type u₃} [ℰ : Category.{v₃} E] {H : D ⥤ E} {I : E ⥤ D}
   (adj₁ : F ⊣ G) (adj₂ : H ⊣ I)
 
-/-- Composition of adjunctions.
-
-See <https://stacks.math.columbia.edu/tag/0DV0>.
--/
-@[simps! (config := .lemmasOnly) unit counit]
+/-- Composition of adjunctions. -/
+@[simps! (config := .lemmasOnly) unit counit, stacks 0DV0]
 def comp : F ⋙ H ⊣ I ⋙ G :=
   mk' {
     homEquiv := fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)

Mathlib/CategoryTheory/Adjunction/Limits.lean

@@ -79,10 +79,8 @@ def functorialityAdjunction : Cocones.functoriality K F ⊣ functorialityRightAd
   counit := functorialityCounit adj K
 
 include adj in
-/-- A left adjoint preserves colimits.
-
-See <https://stacks.math.columbia.edu/tag/0038>.
--/
+/-- A left adjoint preserves colimits. -/
+@[stacks 0038]
 lemma leftAdjoint_preservesColimits : PreservesColimitsOfSize.{v, u} F where
   preservesColimitsOfShape :=
     { preservesColimit :=
@@ -203,10 +201,8 @@ def functorialityAdjunction' : functorialityLeftAdjoint adj K ⊣ Cones.functori
   counit := functorialityCounit' adj K
 
 include adj in
-/-- A right adjoint preserves limits.
-
-See <https://stacks.math.columbia.edu/tag/0038>.
--/
+/-- A right adjoint preserves limits. -/
+@[stacks 0038]
 lemma rightAdjoint_preservesLimits : PreservesLimitsOfSize.{v, u} G where
   preservesLimitsOfShape :=
     { preservesLimit :=

Mathlib/CategoryTheory/Category/Basic.lean

@@ -142,11 +142,8 @@ attribute [aesop safe (rule_sets := [CategoryTheory])] Subsingleton.elim
 
 /-- The typeclass `Category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
-specified explicitly, as `Category.{v} C`. (See also `LargeCategory` and `SmallCategory`.)
-
-See <https://stacks.math.columbia.edu/tag/0014>.
--/
-@[pp_with_univ]
+specified explicitly, as `Category.{v} C`. (See also `LargeCategory` and `SmallCategory`.) -/
+@[pp_with_univ, stacks 0014]
 class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
   /-- Identity morphisms are left identities for composition. -/
   id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f := by aesop_cat
@@ -235,19 +232,15 @@ theorem dite_comp {P : Prop} [Decidable P]
     (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g := by aesop
 
 /-- A morphism `f` is an epimorphism if it can be cancelled when precomposed:
-`f ≫ g = f ≫ h` implies `g = h`.
-
-See <https://stacks.math.columbia.edu/tag/003B>.
--/
+`f ≫ g = f ≫ h` implies `g = h`. -/
+@[stacks 003B]
 class Epi (f : X ⟶ Y) : Prop where
   /-- A morphism `f` is an epimorphism if it can be cancelled when precomposed. -/
   left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
 
 /-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed:
-`g ≫ f = h ≫ f` implies `g = h`.
-
-See <https://stacks.math.columbia.edu/tag/003B>.
--/
+`g ≫ f = h ≫ f` implies `g = h`. -/
+@[stacks 003B]
 class Mono (f : X ⟶ Y) : Prop where
   /-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed. -/
   right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -39,10 +39,8 @@ The category structure coming from a preorder. There is a morphism `X ⟶ Y` if
 
 Because we don't allow morphisms to live in `Prop`,
 we have to define `X ⟶ Y` as `ULift (PLift (X ≤ Y))`.
-See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`.
-
-See <https://stacks.math.columbia.edu/tag/00D3>.
--/
+See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`. -/
+@[stacks 00D3]
 instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α where
   Hom U V := ULift (PLift (U ≤ V))
   id X := ⟨⟨le_refl X⟩⟩

Mathlib/CategoryTheory/Comma/Over.lean

@@ -30,10 +30,8 @@ variable {T : Type u₁} [Category.{v₁} T]
 variable {D : Type u₂} [Category.{v₂} D]
 
 /-- The over category has as objects arrows in `T` with codomain `X` and as morphisms commutative
-triangles.
-
-See <https://stacks.math.columbia.edu/tag/001G>.
--/
+triangles. -/
+@[stacks 001G]
 def Over (X : T) :=
   CostructuredArrow (𝟭 T) X
 
@@ -118,10 +116,8 @@ section
 
 variable (X)
 
-/-- The forgetful functor mapping an arrow to its domain.
-
-See <https://stacks.math.columbia.edu/tag/001G>.
--/
+/-- The forgetful functor mapping an arrow to its domain. -/
+@[stacks 001G]
 def forget : Over X ⥤ T :=
   Comma.fst _ _
 
@@ -141,10 +137,8 @@ def forgetCocone (X : T) : Limits.Cocone (forget X) :=
   { pt := X
     ι := { app := Comma.hom } }
 
-/-- A morphism `f : X ⟶ Y` induces a functor `Over X ⥤ Over Y` in the obvious way.
-
-See <https://stacks.math.columbia.edu/tag/001G>.
--/
+/-- A morphism `f : X ⟶ Y` induces a functor `Over X ⥤ Over Y` in the obvious way. -/
+@[stacks 001G]
 def map {Y : T} (f : X ⟶ Y) : Over X ⥤ Over Y :=
   Comma.mapRight _ <| Discrete.natTrans fun _ => f
 

Mathlib/CategoryTheory/DiscreteCategory.lean

@@ -67,10 +67,8 @@ instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) :=
 /-- The "Discrete" category on a type, whose morphisms are equalities.
 
 Because we do not allow morphisms in `Prop` (only in `Type`),
-somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`.
-
-See <https://stacks.math.columbia.edu/tag/001A>
--/
+somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`. -/
+@[stacks 001A]
 instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) where
   Hom X Y := ULift (PLift (X.as = Y.as))
   id _ := ULift.up (PLift.up rfl)

Mathlib/CategoryTheory/Equivalence.lean

@@ -71,11 +71,8 @@ universe v₁ v₂ v₃ u₁ u₂ u₃
 
   The triangle equation is written as a family of equalities between morphisms, it is more
   complicated if we write it as an equality of natural transformations, because then we would have
-  to insert natural transformations like `F ⟶ F1`.
-
-See <https://stacks.math.columbia.edu/tag/001J>
--/
-@[ext]
+  to insert natural transformations like `F ⟶ F1`. -/
+@[ext, stacks 001J]
 structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D] where mk' ::
   /-- A functor in one direction -/
   functor : C ⥤ D
@@ -425,10 +422,8 @@ theorem pow_neg_one (e : C ≌ C) : e ^ (-1 : ℤ) = e.symm :=
 -- Note: the better formulation of this would involve `HasShift`.
 end
 
-/-- The functor of an equivalence of categories is essentially surjective.
-
-See <https://stacks.math.columbia.edu/tag/02C3>.
--/
+/-- The functor of an equivalence of categories is essentially surjective. -/
+@[stacks 02C3]
 instance essSurj_functor (e : C ≌ E) : e.functor.EssSurj :=
   ⟨fun Y => ⟨e.inverse.obj Y, ⟨e.counitIso.app Y⟩⟩⟩
 
@@ -443,20 +438,16 @@ def fullyFaithfulFunctor (e : C ≌ E) : e.functor.FullyFaithful where
 def fullyFaithfulInverse (e : C ≌ E) : e.inverse.FullyFaithful where
   preimage {X Y} f := e.counitIso.inv.app X ≫ e.functor.map f ≫ e.counitIso.hom.app Y
 
-/-- The functor of an equivalence of categories is faithful.
-
-See <https://stacks.math.columbia.edu/tag/02C3>.
--/
+/-- The functor of an equivalence of categories is faithful. -/
+@[stacks 02C3]
 instance faithful_functor (e : C ≌ E) : e.functor.Faithful :=
   e.fullyFaithfulFunctor.faithful
 
 instance faithful_inverse (e : C ≌ E) : e.inverse.Faithful :=
   e.fullyFaithfulInverse.faithful
 
-/-- The functor of an equivalence of categories is full.
-
-See <https://stacks.math.columbia.edu/tag/02C3>.
--/
+/-- The functor of an equivalence of categories is full. -/
+@[stacks 02C3]
 instance full_functor (e : C ≌ E) : e.functor.Full :=
   e.fullyFaithfulFunctor.full
 
@@ -527,10 +518,8 @@ noncomputable def inv (F : C ⥤ D) [F.IsEquivalence] : D ⥤ C where
   map_id X := by apply F.map_injective; simp
   map_comp {X Y Z} f g := by apply F.map_injective; simp
 
-/-- Interpret a functor that is an equivalence as an equivalence.
-
-See <https://stacks.math.columbia.edu/tag/02C3>. -/
-@[simps functor]
+/-- Interpret a functor that is an equivalence as an equivalence. -/
+@[simps functor, stacks 02C3]
 noncomputable def asEquivalence (F : C ⥤ D) [F.IsEquivalence] : C ≌ D where
   functor := F
   inverse := F.inv