address comments

leanprover-community · Jan 6, 2025 · 8b7fa3b · 8b7fa3b
1 parent 9f5ff59
commit 8b7fa3b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/Mathlib/RingTheory/Kaehler/CotangentComplex.lean b/Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@@ -353,7 +353,8 @@ lemma H1Cotangent.map_comp
     map (g.comp f) = (map g).restrictScalars S ∘ₗ map f := by
   ext; simp [Cotangent.map_comp]
 
-/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions induce an isomorphism of `H¹(L)`. -/
+/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions
+induce an isomorphism between `H¹(L_P₁)` and `H¹(L_P₂)`. -/
 @[simps! apply]
 noncomputable
 def H1Cotangent.equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) :

diff --git a/Mathlib/RingTheory/Smooth/Kaehler.lean b/Mathlib/RingTheory/Smooth/Kaehler.lean
@@ -527,7 +527,7 @@ def homInfinitesimal (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] :
       exact FormallySmooth.liftOfSurjective_apply _
             (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) _ _ x }
 
-/-- Formally smooth extensions have isomorphic `H¹(L)`. -/
+/-- Formally smooth extensions have isomorphic `H¹(L_P)`. -/
 noncomputable
 def H1Cotangent.equivOfFormallySmooth (P₁ P₂ : Extension R S)
     [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] :