We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 04f69b5 commit 8e3a342Copy full SHA for 8e3a342
1 file changed
Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
@@ -137,7 +137,7 @@ noncomputable def self [Projective Z] : ProjectiveResolution Z where
137
138
variable {Z} {Z' : C} (P' : ProjectiveResolution Z')
139
140
-/-- Given injective resolutions `P` and `P'` of two objects `Z` and `Z'`,
+/-- Given projective resolutions `P` and `P'` of two objects `Z` and `Z'`,
141
and a morphism `f : Z ⟶ Z'`, this structure contains the data of a morphism
142
`P.complex ⟶ P'.complex` which is compatible with `f` -/
143
structure Hom (f : Z ⟶ Z') where
0 commit comments