Skip to content

Commit 87adeae

Browse files
committed
chore: namespace CategoryTheory.isoMk to CategoryTheory.WideSubcategory.isoMk (leanprover-community#42532)
1 parent ac10dc7 commit 87adeae

1 file changed

Lines changed: 3 additions & 1 deletion

File tree

Mathlib/CategoryTheory/Widesubcategory.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -137,11 +137,13 @@ instance wideSubcategory.faithful : (wideSubcategoryInclusion P).Faithful :=
137137
variable {P} in
138138
/-- Build an isomorphism in `WideSubcategory P` from an isomorphism in `C`. -/
139139
@[simps!]
140-
def isoMk {X Y : WideSubcategory P} (e : X.obj ≅ Y.obj)
140+
def WideSubcategory.isoMk {X Y : WideSubcategory P} (e : X.obj ≅ Y.obj)
141141
(h₁ : P e.hom) (h₂ : P e.inv) : X ≅ Y where
142142
hom := ⟨e.hom, h₁⟩
143143
inv := ⟨e.inv, h₂⟩
144144

145+
@[deprecated (since := "2026-08-07")] alias isoMk := WideSubcategory.isoMk
146+
145147
end WideSubcategory
146148

147149
end CategoryTheory

0 commit comments

Comments
 (0)