[#14536] [downstream PR] Julia's instance check

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-06
+leanprover/lean4-pr-releases:pr-release-14536-bb2ac20

mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean

@@ -289,6 +289,8 @@ theorem monotone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
   ⟨(Monotone.monotoneOn · _), fun hf ↦ monotone_iff_forall_lt.2 <|
     AddConstMapClass.rel_map_of_Icc ha fun _x hx _y hy hxy ↦ hf hx hy hxy.le⟩
 
+-- Defeq abuse: there is no `AddConstMapClass _ _ Hᵒᵈ _ _`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem antitone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
     [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
@@ -301,6 +303,8 @@ theorem strictMono_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid
     StrictMono f ↔ StrictMonoOn f (Icc l (l + a)) :=
   ⟨(StrictMono.strictMonoOn · _), AddConstMapClass.rel_map_of_Icc ha⟩
 
+-- Defeq abuse: there is no `AddConstMapClass _ _ Hᵒᵈ _ _`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem strictAnti_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
     [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :

mathlib4/Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -100,6 +100,9 @@ variable [Semiring R] [Semiring S] {φ : R →+* S}
   {A B : Type*} [NonUnitalNonAssocSemiring A] [Module R A]
   [NonUnitalNonAssocSemiring B] [Module S B]
 
+-- This needs `DFunLike.coe φ = DFunLike.coe (φ : R →* S)` to hold at `instances` transparency,
+-- which seems reasonable but isn't true at the moment.
+set_option backward.isDefEq.respectTransparency.instances false in
 -- see Note [lower instance priority]
 instance (priority := 100) {F R S A B : Type*}
     {_ : Semiring R} {_ : Semiring S} {φ : R →+* S}

mathlib4/Mathlib/Algebra/Azumaya/Matrix.lean

@@ -54,8 +54,7 @@ lemma AlgHom.mulLeftRightMatrix.comp_inv :
   apply (Matrix.stdBasis _ _ _).ext
   intro ⟨i, j⟩
   simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
-    map_smul, stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply,
-    LinearMap.smul_apply, LinearMap.id_coe, id_eq]
+    stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply, LinearMap.id_coe, id_eq]
   ext k l
   simp [sum_apply, Matrix.mul_apply, single, Fintype.sum_prod_type, ite_and]
 

mathlib4/Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean

@@ -95,6 +95,7 @@ variable (A B) in
 variable (A B) in
 @[simp] lemma braiding_inv_hom : (β_ A B).inv.hom = (comm R B A).toAlgHom := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local ext] Quiver.Hom.unop_inj in
 instance : CartesianMonoidalCategory (CommAlgCat.{u} R)ᵒᵖ where
   isTerminalTensorUnit := terminalOpOfInitial isInitialSelf

mathlib4/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -0,0 +1,220 @@
+/-
+Copyright (c) 2025 Richard Hill. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Hill, Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.Topology.Homology
+public import Mathlib.Algebra.Homology.Embedding.Restriction
+public import Mathlib.Algebra.Homology.Functor
+public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+public import Mathlib.CategoryTheory.Action.Limits
+public import Mathlib.Topology.ContinuousMap.Algebra
+
+/-!
+
+# Continuous cohomology
+
+We define continuous cohomology as the homology of homogeneous cochains.
+
+## Implementation details
+
+We define homogeneous cochains as `g`-invariant continuous function in `C(G, C(G,...,C(G, M)))`
+instead of the usual `C(Gⁿ, M)` to allow more general topological groups other than locally compact
+ones. For this to work, we also work in `Action (TopModuleCat R) G`, where the `G` action on `M`
+is only continuous on `M`, and not necessarily continuous in both variables, because the `G` action
+on `C(G, M)` might not be continuous on both variables even if it is on `M`.
+
+For the differential map, instead of a finite sum we use the inductive definition
+`d₋₁ : M → C(G, M) := const : m ↦ g ↦ m` and
+`dₙ₊₁ : C(G, _) → C(G, C(G, _)) := const - C(G, dₙ) : f ↦ g ↦ f - dₙ (f (g))`
+See `ContinuousCohomology.MultiInd.d`.
+
+## Main definition
+- `ContinuousCohomology.homogeneousCochains`:
+  The functor taking an `R`-linear `G`-representation to the complex of homogeneous cochains.
+- `continuousCohomology`:
+  The functor taking an `R`-linear `G`-representation to its `n`-th continuous cohomology.
+
+## TODO
+- Show that it coincides with `groupCohomology` for discrete groups.
+- Give the usual description of cochains in terms of `n`-ary functions for locally compact groups.
+- Show that short exact sequences induce long exact sequences in certain scenarios.
+-/
+
+set_option backward.defeqAttrib.useBackward true
+
+@[expose] public section
+
+open CategoryTheory Functor ContinuousMap
+
+variable (R G : Type*) [CommRing R] [Group G] [TopologicalSpace R]
+
+namespace ContinuousCohomology
+
+variable [TopologicalSpace G] [IsTopologicalGroup G]
+
+variable {R G} in
+/-- The `G` representation `C(G, rep)` given a representation `rep`.
+The `G` action is defined by `g • f := x ↦ g • f (g⁻¹ * x)`. -/
+abbrev Iobj (rep : Action (TopModuleCat R) G) : Action (TopModuleCat R) G where
+  V := .of R C(G, rep.V)
+  ρ :=
+  { toFun g := TopModuleCat.ofHom
+      { toFun f := .comp (rep.ρ g).hom (f.comp (Homeomorph.mulLeft g⁻¹))
+        map_add' _ _ := by ext; simp
+        map_smul' _ _ := by ext; simp
+        cont := (continuous_postcomp _).comp (continuous_precomp _) }
+    map_one' := ConcreteCategory.ext (by ext; simp)
+    map_mul' _ _ := ConcreteCategory.ext (by ext; simp [mul_assoc]) }
+
+lemma Iobj_ρ_apply (rep : Action (TopModuleCat R) G) (g f x) :
+    ((Iobj rep).ρ g).hom f x = (rep.ρ g).hom (f (g⁻¹ * x)) := rfl
+
+/-- The functor taking a representation `rep` to the representation `C(G, rep)`. -/
+@[simps]
+def I : Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G where
+  obj := Iobj
+  map {M N} φ :=
+  { hom := TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous _ _ φ.hom.hom)
+    comm g := by
+      ext f g'
+      change (M.ρ g ≫ φ.hom).hom (f (g⁻¹ * g')) = (φ.hom ≫ N.ρ g).hom (f (g⁻¹ * g'))
+      rw [φ.comm] }
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+instance : (I R G).Additive where
+instance : (I R G).Linear R where
+
+/-- The constant function `rep ⟶ C(G, rep)` as a natural transformation. -/
+@[simps]
+def const : 𝟭 _ ⟶ I R G where
+  app _ := { hom := TopModuleCat.ofHom (.const _ _), comm _ := rfl }
+  naturality _ _ _ := rfl
+
+namespace MultiInd
+
+set_option linter.style.whitespace false in -- manual alignment is not recognised
+/-- The n-th functor taking `M` to `C(G, C(G,...,C(G, M)))` (with n `G`s).
+These functors form a complex, see `MultiInd.complex`. -/
+def functor : ℕ → Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G
+  | 0     => 𝟭 _
+  | n + 1 => functor n ⋙ I R G
+
+set_option linter.style.whitespace false in -- manual alignment is not recognised
+set_option backward.isDefEq.respectTransparency.instances false in
+/-- The differential map in `MultiInd.complex`. -/
+def d : ∀ n : ℕ, functor R G n ⟶ functor R G (n + 1)
+  | 0     => const R G
+  | n + 1 => whiskerLeft (functor R G (n + 1)) (const R G) - (by exact whiskerRight (d n) (I R G))
+
+lemma d_zero : d R G 0 = const R G := rfl
+
+set_option backward.isDefEq.respectTransparency.instances false in
+lemma d_succ (n : ℕ) :
+    d R G (n + 1) = whiskerLeft (functor R G (n + 1)) (const R G) -
+      (by exact whiskerRight (d R G n) (I R G)) := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc (attr := simp)]
+lemma d_comp_d (n : ℕ) :
+    d R G n ≫ d R G (n + 1) = 0 := by
+  induction n with
+  | zero =>
+    rw [d_succ, Preadditive.comp_sub, sub_eq_zero]
+    rfl
+  | succ n ih =>
+    rw [d_succ R G (n + 1), Preadditive.comp_sub]
+    nth_rw 2 [d_succ]
+    rw [Preadditive.sub_comp, ← whiskerRight_comp, ih,
+      Functor.whiskerRight_zero, sub_zero, sub_eq_zero]
+    rfl
+
+/-- The complex of functors whose behaviour pointwise takes an `R`-linear `G`-representation `M`
+to the complex `M → C(G, M) → ⋯ → C(G, C(G,...,C(G, M))) → ⋯`
+The `G`-invariant submodules of it is the homogeneous cochains (shifted by one). -/
+def complex : CochainComplex (Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) ℕ :=
+  CochainComplex.of (functor R G) (d R G) (d_comp_d R G)
+
+end MultiInd
+
+/-- The functor taking an `R`-linear `G`-representation to its `G`-invariant submodule. -/
+def invariants : Action (TopModuleCat R) G ⥤ TopModuleCat R where
+  obj M := .of R
+    { carrier := { x | ∀ g : G, (M.ρ g).hom x = x }
+      add_mem' hx hy g := by simp [hx g, hy g]
+      zero_mem' := by simp
+      smul_mem' r x hx g := by simp [hx g] : Submodule R M.V }
+  map f := TopModuleCat.ofHom
+    { toLinearMap := f.hom.hom.restrict fun x hx g ↦
+        congr($(f.comm g) x).symm.trans congr(f.hom.hom $(hx g))
+      cont := continuous_induced_rng.mpr (f.hom.hom.2.comp continuous_subtype_val) }
+
+instance : (invariants R G).Linear R where
+instance : (invariants R G).Additive where
+
+/-- `homogeneousCochains R G` is the functor taking
+an `R`-linear `G`-representation to the complex of homogeneous cochains. -/
+def homogeneousCochains : Action (TopModuleCat R) G ⥤ CochainComplex (TopModuleCat R) ℕ :=
+  (MultiInd.complex R G).asFunctor ⋙ (invariants R G).mapHomologicalComplex _ ⋙
+    (ComplexShape.embeddingUp'Add 1 1).restrictionFunctor _
+
+/-- `continuousCohomology R G n` is the functor taking
+an `R`-linear `G`-representation to its `n`-th continuous cohomology. -/
+noncomputable
+def _root_.continuousCohomology (n : ℕ) : Action (TopModuleCat R) G ⥤ TopModuleCat R :=
+  homogeneousCochains R G ⋙ HomologicalComplex.homologyFunctor _ _ n
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The `0`-homogeneous cochains are isomorphic to `Xᴳ`. -/
+def kerHomogeneousCochainsZeroEquiv
+    (X : Action (TopModuleCat R) G) (n : ℕ) (hn : n = 1) :
+    (((homogeneousCochains R G).obj X).d 0 n).hom.ker ≃L[R] (invariants R G).obj X where
+  toFun x :=
+  { val := DFunLike.coe (F := C(G, _)) x.1.1 1
+    property g := by
+      subst hn
+      obtain ⟨⟨x : C(G, _), hx⟩, hx'⟩ := x
+      have : (X.ρ g).hom (x (g⁻¹ * 1)) = x 1 := congr(DFunLike.coe (F := C(G, _)) $(hx g) 1)
+      have hx' : x (g⁻¹ * 1) - x 1 = 0 :=
+        congr(DFunLike.coe (F := C(G, _)) (DFunLike.coe (F := C(G, _)) ($hx').1 1) (g⁻¹ * 1))
+      rw [sub_eq_zero] at hx'
+      exact congr((X.ρ g).hom $hx').symm.trans this }
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  invFun x := by
+    refine ⟨⟨ContinuousLinearMap.const R _ x.1, fun g ↦ ContinuousMap.ext fun a ↦
+      by subst hn; exact x.2 g⟩, ?_⟩
+    subst hn
+    exact Subtype.ext (ContinuousMap.ext fun a ↦
+      ContinuousMap.ext fun b ↦ show x.1 - x.1 = (0 : X.V) by simp)
+  left_inv x := by
+    subst hn
+    obtain ⟨⟨x : C(G, _), hx⟩, hx'⟩ := x
+    refine Subtype.ext (Subtype.ext <| ContinuousMap.ext fun a ↦ ?_)
+    have hx' : x 1 - x a = 0 :=
+      congr(DFunLike.coe (F := C(G, _)) (DFunLike.coe (F := C(G, _)) ($hx').1 a) 1)
+    rwa [sub_eq_zero] at hx'
+  right_inv _ := rfl
+  continuous_toFun := continuous_induced_rng.mpr ((continuous_eval_const (F := C(G, _)) 1).comp
+      (continuous_subtype_val.comp continuous_subtype_val))
+  continuous_invFun := continuous_induced_rng.mpr
+    (continuous_induced_rng.mpr ((ContinuousLinearMap.const R G).cont.comp continuous_subtype_val))
+
+set_option backward.isDefEq.respectTransparency false in
+open ShortComplex HomologyData in
+/-- `H⁰_cont(G, X) ≅ Xᴳ`. -/
+noncomputable
+def continuousCohomologyZeroIso : (continuousCohomology R G 0) ≅ invariants R G :=
+  NatIso.ofComponents (fun X ↦ (ofIsLimitKernelFork _ (by simp) _
+    (TopModuleCat.isLimitKer _)).left.homologyIso ≪≫ TopModuleCat.ofIso
+      (kerHomogeneousCochainsZeroEquiv R G X _ (by simp))) fun {X Y} f ↦ by
+  dsimp [continuousCohomology, HomologicalComplex.homologyMap]
+  rw [Category.assoc, ← Iso.inv_comp_eq]
+  rw [LeftHomologyData.leftHomologyIso_inv_naturality_assoc, Iso.inv_hom_id_assoc,
+    ← cancel_epi (LeftHomologyData.π _), leftHomologyπ_naturality'_assoc]
+  rfl
+
+end ContinuousCohomology

mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -110,6 +110,8 @@ variable {R} in
 instance (V : FGModuleCat.{v} R) : Module.Finite R V :=
   V.property
 
+-- Needs to unfold the `forget₂` at `instances` transparency.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : (forget₂ (FGModuleCat.{v} R) (ModuleCat.{v} R)).Full where
   map_surjective f := ⟨ofHom f.hom, rfl⟩
 

mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean

@@ -301,6 +301,13 @@ namespace AddCommGrpCat
 
 open QuotientAddGroup
 
+#adaptation_note
+/--
+This definition fails without `respectTransparency false`. Removing `lift_mk` from the `dsimp only`
+set in `inv_hom_id` would help. A more sustainable fix would probably be to revisit the `lift_mk`
+refl lemma: Its LHS and RHS are not defeq at implicit transparency. Either the lemma shouldn't be
+a refl lemma or more declarations need to be implicit-reducible.
+-/
 set_option backward.isDefEq.respectTransparency false in
 set_option backward.defeqAttrib.useBackward true in
 /-- The categorical cokernel of a morphism in `AddCommGrpCat`
@@ -321,8 +328,8 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGrpCat.{u}} (f : G ⟶ H) :
     rfl
   inv_hom_id := by
     ext x
-    dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk',
-      Function.comp_apply, AddMonoidHom.zero_apply, id_eq, lift_mk, hom_id, AddMonoidHom.coe_id]
+    dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk', lift_mk,
+      Function.comp_apply, AddMonoidHom.zero_apply, id_eq, hom_id, AddMonoidHom.coe_id]
     exact QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _
 
 end AddCommGrpCat

mathlib4/Mathlib/Algebra/Category/Grp/FiniteGrp.lean

@@ -48,6 +48,8 @@ instance : CoeSort FiniteGrp.{u} (Type u) where
 instance : Category FiniteGrp :=
   inferInstanceAs <| Category (InducedCategory _ FiniteGrp.toGrp)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 instance : ConcreteCategory FiniteGrp (· →* ·) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toGrp) _

mathlib4/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -98,6 +98,7 @@ lemma forget₂_map_restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ri
     (forget₂ _ Ab).map ((ModuleCat.restrictScalars f).map g) = (forget₂ _ Ab).map g :=
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     (restrictScalars.{v} f).Faithful where
   map_injective h := by
@@ -652,8 +653,10 @@ protected noncomputable def counit' : coextendScalars f ⋙ restrictScalars f 
 
 end RestrictionCoextensionAdj
 
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 -- Porting note: very fiddly universes
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Restriction of scalars is left adjoint to coextension of scalars. -/
 -- @[simps] Porting note: not in normal form and not used
 def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :

mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

@@ -78,6 +78,34 @@ variable (d : M.Derivation φ)
 @[simp] lemma d_one (X : Dᵒᵖ) : d.d (X := X) 1 = 0 := by
   simpa using d.d_mul (X := X) 1 1
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized, writing `Y` for
+`Opposite.op (F.obj (Opposite.unop X))`:
+`FunLike (↑(M.obj Y) →ₗ[↑(R.obj Y)] ↑(N.obj Y)) ↑(M.obj Y) ↑(N.obj Y)`
+It is needed by the `rw [map_zero]` in `d_app` below; the accompanying `ZeroHomClass` fails the
+same way.
+
+The failure happens while applying `@LinearMap.instFunLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Module ↑(R.obj Y) ↑(M.obj Y)`, whereas the assigned value `(M.obj (F.op.obj X)).isModule` has
+type `Module ↑((R ⋙ forget₂ CommRingCat RingCat).obj (F.op.obj X)) ↑(M.obj (F.op.obj X))`. The
+comparison bottoms out at
+`(R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj (F.op.obj X)).1`, which would require
+unfolding `Functor.comp` and `Functor.op`; both are `@[implicit_reducible]` and therefore do not
+unfold at the `.instances` transparency that instance search runs at. Lean falls back to synthesize
+an instance of the correct type, which succeeds, but it returns `(M.obj Y).isModule`, which is again
+not defeq to the assigned value, stalling at `F.op.1 X =?= Opposite.op (F.obj (Opposite.unop X))`.
+That comparison, too, runs at `.instances`, since `respectTransparency false` suppresses the
+transparency bump that instance-implicit arguments would otherwise receive.
+
+Potential fix: see `# Fix` below — mark `ModuleCat.restrictScalars` and
+`ModuleCat.RestrictScalars.obj'` implicit-reducible. Then `respectTransparency false` and
+`instanceTypes false` can both go, and the `erw` becomes an `rw`.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The postcomposition of a derivation by a morphism of presheaves of modules. -/
@@ -201,6 +229,7 @@ noncomputable def relativeDifferentials' :
 
 attribute [simp] relativeDifferentials'_obj
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma relativeDifferentials'_map_d {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : R.obj X) :
     DFunLike.coe (α := CommRingCat.KaehlerDifferential (φ'.app X))

mathlib4/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -156,8 +156,7 @@ def colimitCocone : Cocone F where
     { app := coconeMorphism F
       naturality _ _ f := by
         ext
-        simpa using! (Types.TypeMax.colimitCocone
-          (F ⋙ forget (ModuleCat R))).ι.naturality_apply f _ }
+        simpa using! (F ⋙ forget (ModuleCat R)).ιColimitType_map f _ }
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Given a cocone `t` of `F`, the induced monoid linear map from the colimit to the cocone point.

mathlib4/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean

@@ -137,6 +137,7 @@ lemma hasInjectiveDimensionLE_iff_of_semiLinearEquiv [Small.{v'} R']
     hasInjectiveDimensionLE_iff_of_linearEquiv_aux eN]
   exact hasInjectiveDimensionLE_iff_of_semiLinearEquiv_aux eR ((eM.symm.trans e).trans eN) n
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma injectiveDimension_eq_of_semiLinearEquiv [Small.{v'} R']
     {M : ModuleCat.{v} R} {N : ModuleCat.{v'} R'} (e : M ≃ₛₗ[RingHomClass.toRingHom eR] N) :
     injectiveDimension M = injectiveDimension N := by