Skip to content

Commit 134bd66

Browse files
erdOneerdOne
committed
feat(AlgebraicGeometry): tilde-Gamma adjunction (#35123)
1 parent 706fd95 commit 134bd66

File tree

1 file changed

+259
-46
lines changed

1 file changed

+259
-46
lines changed

‎Mathlib/AlgebraicGeometry/Modules/Tilde.lean‎

Lines changed: 259 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Authors: Kevin Buzzard, Johan Commelin, Amelia Livingston, Sophie Morel, Jujian
77
module
88

99
public import Mathlib.Algebra.Module.LocalizedModule.Basic
10-
public import Mathlib.AlgebraicGeometry.StructureSheaf
10+
public import Mathlib.AlgebraicGeometry.AffineScheme
1111
public import Mathlib.AlgebraicGeometry.Modules.Sheaf
1212
public import Mathlib.Algebra.Category.ModuleCat.Sheaf
1313
public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
@@ -21,87 +21,300 @@ Given any commutative ring `R` and `R`-module `M`, we construct the sheaf `M^~`
2121
such that `M^~(U)` is the set of dependent functions that are locally fractions.
2222
2323
## Main definitions
24-
* `ModuleCat.tilde` : `M^~` as a sheaf of `𝒪_{Spec R}`-modules.
24+
* `AlgebraicGeometry.tilde` : `M^~` as a sheaf of `𝒪_{Spec R}`-modules.
25+
* `AlgebraicGeometry.tilde.adjunction` : `~` is left adjoint to taking global sections.
26+
2527
-/
2628

27-
@[expose] public section
29+
@[expose] public noncomputable section
2830

2931
universe u
3032

3133
open TopCat AlgebraicGeometry TopologicalSpace CategoryTheory Opposite
3234

33-
variable {R : Type u} [CommRing R] (M : ModuleCat.{u} R)
35+
variable {R : CommRingCat.{u}} (M : ModuleCat.{u} R)
3436

35-
namespace ModuleCat
37+
namespace AlgebraicGeometry
38+
39+
open _root_.PrimeSpectrum
40+
41+
/-- The forgetful functor from `𝒪_{Spec R}` modules to sheaves of `R`-modules. -/
42+
def modulesSpecToSheaf :
43+
(Spec R).Modules ⥤ TopCat.Sheaf (ModuleCat R) (Spec R) :=
44+
SheafOfModules.forgetToSheafModuleCat (Spec R).ringCatSheaf (.op ⊤)
45+
(Limits.initialOpOfTerminal Limits.isTerminalTop) ⋙
46+
sheafCompose _ (ModuleCat.restrictScalars (StructureSheaf.globalSectionsIso R).hom.hom)
47+
48+
/-- The global section functor for `𝒪_{Spec R}` modules -/
49+
noncomputable
50+
def moduleSpecΓFunctor : (Spec (.of R)).Modules ⥤ ModuleCat R :=
51+
modulesSpecToSheaf ⋙ TopCat.Sheaf.forget _ _ ⋙ (evaluation _ _).obj (.op ⊤)
52+
53+
open PrimeSpectrum in
54+
/-- The forgetful functor from `𝒪_{Spec R}` modules to sheaves of `R`-modules is fully faithful. -/
55+
def SpecModulesToSheafFullyFaithful : (modulesSpecToSheaf (R := R)).FullyFaithful where
56+
preimage {M N} f := ⟨fun U ↦ ModuleCat.ofHom ⟨(f.1.app U).hom.toAddHom, by
57+
intro t m
58+
apply TopCat.Presheaf.IsSheaf.section_ext (modulesSpecToSheaf.obj N).2
59+
intro x hxU
60+
obtain ⟨a, ⟨_, ⟨r, rfl⟩, rfl⟩, hxr, hrU : basicOpen _ ≤ _⟩ :=
61+
PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU U.unop.2
62+
refine ⟨_, hrU, hxr, ?_⟩
63+
refine Eq.trans ?_ (N.val.map_smul (homOfLE hrU).op t _).symm
64+
change N.1.map (homOfLE hrU).op (f.1.app _ _) = _ • N.1.map (homOfLE hrU).op (f.1.app _ _)
65+
have (x : _) :
66+
f.1.app _ (M.1.map (homOfLE hrU).op _) = N.1.map (homOfLE hrU).op (f.1.app _ x) :=
67+
congr($(f.1.naturality (homOfLE hrU).op).hom x)
68+
rw [← this, ← this, M.val.map_smul]
69+
generalize (Spec R).ringCatSheaf.val.map (homOfLE hrU).op t = t
70+
letI := Module.compHom (R := Γ(Spec R, basicOpen r)) Γ(M, basicOpen r)
71+
(algebraMap R Γ(Spec R, basicOpen r))
72+
haveI : IsScalarTower R Γ(Spec R, basicOpen r) Γ(M, basicOpen r) :=
73+
.of_algebraMap_smul fun _ _ ↦ rfl
74+
letI := Module.compHom Γ(N, basicOpen r) (algebraMap R Γ(Spec R, basicOpen r))
75+
haveI : IsScalarTower R Γ(Spec R, basicOpen r) Γ(N, basicOpen r) :=
76+
.of_algebraMap_smul fun _ _ ↦ rfl
77+
exact (IsLocalization.linearMap_compatibleSMul (.powers (M := R) r)
78+
Γ(Spec R, basicOpen r) Γ(M, basicOpen r) Γ(N, basicOpen r)).map_smul
79+
(f.val.app _).hom _ _⟩, fun i ↦ by ext x; exact congr($(f.1.naturality i).hom x)⟩
80+
map_preimage f := rfl
81+
preimage_map f := rfl
3682

3783
/--
3884
`M^~` as a sheaf of `𝒪_{Spec R}`-modules
3985
-/
40-
noncomputable def tilde : (Spec <| .of R).Modules where
86+
def tilde : (Spec R).Modules where
4187
val := moduleStructurePresheaf R M
4288
isSheaf := (TopCat.Presheaf.isSheaf_iff_isSheaf_comp (forget AddCommGrpCat) _).2
4389
(structureSheafInType R M).2
4490

45-
/--
46-
This is `M^~` as a sheaf of `R`-modules.
47-
-/
48-
noncomputable def tildeInModuleCat :
49-
TopCat.Presheaf (ModuleCat R) (PrimeSpectrum.Top R) :=
50-
structurePresheafInModuleCat R M
51-
52-
namespace Tilde
53-
54-
@[simp]
55-
theorem res_apply (U V : Opens (PrimeSpectrum.Top R)) (i : V ⟶ U)
56-
(s : (tildeInModuleCat M).obj (op U)) (x : V) :
57-
((tildeInModuleCat M).map i.op s).1 x = (s.1 (i x) :) :=
58-
rfl
59-
60-
lemma smul_section_apply (r : R) (U : Opens (PrimeSpectrum.Top R))
61-
(s : (tildeInModuleCat M).obj (op U)) (x : U) :
62-
(r • s).1 x = r • (s.1 x) := rfl
63-
64-
lemma smul_stalk_no_nonzero_divisor {x : PrimeSpectrum R}
65-
(r : x.asIdeal.primeCompl) (st : (tildeInModuleCat M).stalk x) (hst : r.1 • st = 0) :
66-
st = 0 :=
67-
Limits.Concrete.colimit_no_zero_smul_divisor _ _ _
68-
⟨op ⟨PrimeSpectrum.basicOpen r.1, r.2⟩, fun U i s hs ↦ Subtype.ext <| funext fun pt ↦
69-
LocalizedModule.eq_zero_of_smul_eq_zero _ (i.unop pt).2 _
70-
(by simpa [← smul_section_apply] using congr(($hs).1 pt))⟩ _ hst
91+
namespace tilde
7192

72-
/--
73-
If `U` is an open subset of `Spec R`, this is the morphism of `R`-modules from `M` to
74-
`M^~(U)`.
75-
-/
76-
noncomputable def toOpen (U : Opens (PrimeSpectrum.Top R)) :
77-
ModuleCat.of R M ⟶ (tildeInModuleCat M).obj (op U) :=
78-
ModuleCat.ofHom (StructureSheaf.toOpenₗ R M U)
93+
/-- (Implementation). The image of `tilde` under `modulesSpecToSheaf` is isomorphic to
94+
`structurePresheafInModuleCat`. They are defeq as types but the `Smul` instance are not defeq. -/
95+
noncomputable
96+
def modulesSpecToSheafIso :
97+
(modulesSpecToSheaf.obj (tilde M)).1 ≅ structurePresheafInModuleCat R M :=
98+
NatIso.ofComponents (fun U ↦ LinearEquiv.toModuleIso
99+
(X₁ := (modulesSpecToSheaf.obj (tilde M)).presheaf.obj _)
100+
{ __ := AddEquiv.refl _,
101+
map_smul' r m := IsScalarTower.algebraMap_smul (M := ((structureSheafInType R M).val.obj U))
102+
((structureSheafInType R R).val.obj U) r m }) fun _ ↦ rfl
79103

104+
/-- The map from `M` to `Γ(M, U)`. This is a localiation map when `U = D(f)`. -/
105+
def toOpen (U : (Spec R).Opens) : M ⟶ (modulesSpecToSheaf.obj (tilde M)).presheaf.obj (.op U) :=
106+
ModuleCat.ofHom (StructureSheaf.toOpenₗ R M U) ≫ ((modulesSpecToSheafIso M).app _).inv
80107

81-
@[simp]
108+
@[reassoc (attr := simp)]
82109
theorem toOpen_res (U V : Opens (PrimeSpectrum.Top R)) (i : V ⟶ U) :
83-
toOpen M U ≫ (tildeInModuleCat M).map i.op = toOpen M V :=
110+
toOpen M U ≫ (modulesSpecToSheaf.obj (tilde M)).presheaf.map i.op = toOpen M V :=
84111
rfl
85112

113+
instance (f : R) : IsLocalizedModule (.powers f) (toOpen M (basicOpen f)).hom :=
114+
.of_linearEquiv (.powers f) (StructureSheaf.toOpenₗ R M (basicOpen f))
115+
((modulesSpecToSheafIso M).app _).toLinearEquiv.symm
116+
86117
noncomputable
87-
instance (x : PrimeSpectrum.Top R) : Module R ↑(TopCat.Presheaf.stalk M.tilde.presheaf x) :=
118+
instance (x : PrimeSpectrum.Top R) : Module R ((tilde M).presheaf.stalk x) :=
88119
inferInstanceAs (Module R ↑(TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x))
89120

90121
/--
91122
If `x` is a point of `Spec R`, this is the morphism of `R`-modules from `M` to the stalk of
92123
`M^~` at `x`.
93124
-/
94125
noncomputable def toStalk (x : PrimeSpectrum.Top R) :
95-
ModuleCat.of R M ⟶ ModuleCat.of R ↑(TopCat.Presheaf.stalk M.tilde.presheaf x) :=
126+
ModuleCat.of R M ⟶ ModuleCat.of R ((tilde M).presheaf.stalk x) :=
96127
ModuleCat.ofHom (StructureSheaf.toStalkₗ ..)
97128

98129
instance (x : PrimeSpectrum.Top R) :
99130
IsLocalizedModule x.asIdeal.primeCompl (toStalk M x).hom :=
100131
inferInstanceAs (IsLocalizedModule x.asIdeal.primeCompl (StructureSheaf.toStalkₗ ..))
101132

102-
instance (f : R) : IsLocalizedModule (.powers f) (toOpen M (PrimeSpectrum.basicOpen f)).hom :=
103-
inferInstanceAs (IsLocalizedModule (.powers f) (StructureSheaf.toOpenₗ ..))
133+
/-- The tilde construction is functorial. -/
134+
protected noncomputable def map {M N : ModuleCat R} (f : M ⟶ N) : tilde M ⟶ tilde N :=
135+
SpecModulesToSheafFullyFaithful.preimage ⟨(modulesSpecToSheafIso M).hom ≫
136+
{ app U := ModuleCat.ofHom (StructureSheaf.comapₗ f.hom _ _ .rfl) } ≫
137+
(modulesSpecToSheafIso N).inv⟩
138+
139+
@[reassoc (attr := simp)]
140+
lemma toOpen_map_app {M N : ModuleCat R} (f : M ⟶ N)
141+
(U : TopologicalSpace.Opens (PrimeSpectrum R)) :
142+
toOpen M U ≫ (modulesSpecToSheaf.map (tilde.map f)).1.app _ =
143+
f ≫ toOpen N U := by
144+
ext x; exact Subtype.ext (funext fun y ↦ IsLocalizedModule.map_apply y.1.asIdeal.primeCompl
145+
(LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
146+
(LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N) _ x)
147+
148+
variable (R) in
149+
/-- Tilde as a functor -/
150+
@[simps] protected noncomputable def functor : ModuleCat R ⥤ (Spec (.of R)).Modules where
151+
obj := tilde
152+
map := tilde.map
153+
map_id M := by
154+
ext p x
155+
exact Subtype.ext (funext fun y ↦ DFunLike.congr_fun (LocalizedModule.map_id _) _)
156+
map_comp {M N P} f g := by
157+
ext p x
158+
exact Subtype.ext (funext
159+
fun y ↦ DFunLike.congr_fun (IsLocalizedModule.map_comp' y.1.asIdeal.primeCompl
160+
(LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
161+
(LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N)
162+
(LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl P) _ _) _)
163+
164+
instance isIso_toOpen_top {M : ModuleCat R} : IsIso (toOpen M ⊤) := by
165+
rw [toOpen, isIso_comp_right_iff, ConcreteCategory.isIso_iff_bijective]
166+
exact StructureSheaf.toOpenₗ_top_bijective
167+
168+
/-- The isomorphism between the global sections of `M^~` and `M`. -/
169+
@[simps! hom]
170+
noncomputable def isoTop (M : ModuleCat R) :
171+
M ≅ (modulesSpecToSheaf.obj (tilde M)).presheaf.obj (.op ⊤) :=
172+
asIso (toOpen M ⊤)
173+
174+
open PrimeSpectrum in
175+
lemma isUnit_algebraMap_end_basicOpen (M : (Spec (.of R)).Modules) (f : R) :
176+
IsUnit (algebraMap R (Module.End R
177+
((modulesSpecToSheaf.obj M).presheaf.obj (.op (basicOpen f)))) f) := by
178+
rw [Module.End.isUnit_iff]
179+
change Function.Bijective (algebraMap Γ(Spec R, basicOpen f)
180+
(Module.End Γ(Spec R, basicOpen f) Γ(M, basicOpen f)) (algebraMap R _ f))
181+
rw [← Module.End.isUnit_iff]
182+
exact (IsLocalization.Away.algebraMap_isUnit _).map _
183+
184+
end tilde
185+
186+
/-- This is the counit of the tilde-Gamma adjunction. -/
187+
noncomputable def Scheme.Modules.fromTildeΓ (M : (Spec (.of R)).Modules) :
188+
tilde ((modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)) ⟶ M :=
189+
SpecModulesToSheafFullyFaithful.preimage
190+
⟨TopCat.Sheaf.restrictHomEquivHom _ _ isBasis_basic_opens
191+
{ app (f : Rᵒᵖ) := by
192+
refine (ModuleCat.ofHom (IsLocalizedModule.lift (.powers (M := R) f.unop)
193+
(tilde.toOpen _ (PrimeSpectrum.basicOpen f.unop)).hom
194+
((modulesSpecToSheaf.obj M).val.map (homOfLE le_top).op).hom ?_):)
195+
rw [Subtype.forall]
196+
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
197+
simp only [inducedFunctor_obj, Submonoid.powers_le, Submonoid.mem_comap]
198+
exact tilde.isUnit_algebraMap_end_basicOpen M f.unop
199+
naturality {f g : Rᵒᵖ} i := by
200+
letI N := (modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)
201+
ext1
202+
apply IsLocalizedModule.ext (.powers (M := R) f.unop)
203+
(tilde.toOpen _ (PrimeSpectrum.basicOpen (R := R) f.unop)).hom
204+
· rw [Subtype.forall]
205+
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
206+
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
207+
obtain ⟨n, a, e⟩ : ∃ n, f.unop ∣ g.unop ^ n := by
208+
simpa only [Ideal.mem_radical_iff, Ideal.mem_span_singleton] using
209+
(basicOpen_le_basicOpen_iff _ _).mp (i.1.hom.le)
210+
refine ((Commute.isUnit_mul_iff (b := algebraMap R _ a) (.map (.all _ _) _)).mp ?_).1
211+
rw [← map_mul, ← e, map_pow]
212+
exact (tilde.isUnit_algebraMap_end_basicOpen M g.unop).pow n
213+
· dsimp [← ModuleCat.hom_comp]
214+
rw [tilde.toOpen_res_assoc]
215+
ext x
216+
dsimp
217+
simp only [IsLocalizedModule.lift_apply, ← ModuleCat.comp_apply, ← Functor.map_comp]
218+
rfl }⟩
219+
220+
@[reassoc]
221+
lemma Scheme.Modules.toOpen_fromTildeΓ_app (M : (Spec (.of R)).Modules) (U) :
222+
tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)) U ≫
223+
(modulesSpecToSheaf.map M.fromTildeΓ).1.app (.op U) =
224+
(modulesSpecToSheaf.obj M).1.map (homOfLE le_top).op := by
225+
wlog hU : U = PrimeSpectrum.basicOpen 1 generalizing U
226+
· rw [← tilde.toOpen_res _ (PrimeSpectrum.basicOpen 1) _ (homOfLE (by simp)), Category.assoc,
227+
NatTrans.naturality, ← Category.assoc, this, ← Functor.map_comp, ← op_comp, homOfLE_comp]
228+
simp
229+
subst hU
230+
simp only [fromTildeΓ, inducedFunctor_obj,
231+
homOfLE_leOfHom, Functor.FullyFaithful.map_preimage, TopCat.Sheaf.extend_hom_app]
232+
ext x
233+
refine (IsLocalizedModule.lift_apply (.powers (M := R) 1)
234+
(tilde.toOpen _ (PrimeSpectrum.basicOpen (R := R) 1)).hom
235+
((modulesSpecToSheaf.obj M).val.map (homOfLE le_top).op).hom (by simp) x)
236+
237+
/-- This is the counit of the tilde-Gamma adjunction. -/
238+
noncomputable def Scheme.Modules.fromTildeΓNatTrans :
239+
moduleSpecΓFunctor (R := R) ⋙ tilde.functor (R := R) ⟶ 𝟭 _ where
240+
app := fromTildeΓ
241+
naturality {M N} f := by
242+
apply SpecModulesToSheafFullyFaithful.map_injective
243+
apply CategoryTheory.Sheaf.hom_ext
244+
apply (TopCat.Sheaf.restrictHomEquivHom _ _ PrimeSpectrum.isBasis_basic_opens).symm.injective
245+
ext r : 3
246+
apply IsLocalizedModule.ext (.powers (M := R) r.unop)
247+
(tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤))
248+
(PrimeSpectrum.basicOpen (R := R) r.unop)).hom
249+
· rw [Subtype.forall]
250+
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
251+
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
252+
exact tilde.isUnit_algebraMap_end_basicOpen ..
253+
dsimp [TopCat.Sheaf.restrictHomEquivHom, Functor.IsCoverDense.restrictHomEquivHom,
254+
moduleSpecΓFunctor, Sheaf.forget]
255+
simp only [← ModuleCat.hom_comp, Functor.map_comp]
256+
rw [CategoryTheory.Sheaf.comp_val, CategoryTheory.Sheaf.comp_val]
257+
congr 1
258+
simp only [NatTrans.comp_app]
259+
rw [tilde.toOpen_map_app_assoc, toOpen_fromTildeΓ_app N (PrimeSpectrum.basicOpen r.unop),
260+
toOpen_fromTildeΓ_app_assoc M (PrimeSpectrum.basicOpen r.unop),
261+
← (modulesSpecToSheaf.map f).val.naturality]
262+
263+
/-- `tilde.isoTop` bundled as a natural isomorphism.
264+
This is the unit of the tilde-Gamma adjunction. -/
265+
def tilde.toTildeΓNatIso : 𝟭 _ ≅ tilde.functor R ⋙ moduleSpecΓFunctor :=
266+
NatIso.ofComponents tilde.isoTop fun f ↦ (tilde.toOpen_map_app f _).symm
267+
268+
open Scheme.Modules in
269+
/-- The tilde-Gamma adjuntion. -/
270+
def tilde.adjunction : tilde.functor R ⊣ moduleSpecΓFunctor where
271+
unit := toTildeΓNatIso.hom
272+
counit := fromTildeΓNatTrans
273+
left_triangle_components M := by
274+
apply SpecModulesToSheafFullyFaithful.map_injective
275+
apply CategoryTheory.Sheaf.hom_ext
276+
apply (TopCat.Sheaf.restrictHomEquivHom _ _ PrimeSpectrum.isBasis_basic_opens).symm.injective
277+
ext r : 3
278+
apply IsLocalizedModule.ext (.powers (M := R) r.unop)
279+
(toOpen _ (PrimeSpectrum.basicOpen (R := R) r.unop)).hom
280+
· rw [Subtype.forall]
281+
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
282+
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
283+
exact isUnit_algebraMap_end_basicOpen ..
284+
dsimp [toTildeΓNatIso, isoTop,
285+
TopCat.Sheaf.restrictHomEquivHom, Functor.IsCoverDense.restrictHomEquivHom,
286+
fromTildeΓNatTrans, moduleSpecΓFunctor, Sheaf.forget, sheafToPresheaf]
287+
simp only [← ModuleCat.hom_comp, Functor.map_comp]
288+
congr 1
289+
rw [CategoryTheory.Sheaf.comp_val]
290+
dsimp
291+
rw [toOpen_map_app_assoc, toOpen_fromTildeΓ_app]
292+
rfl
293+
right_triangle_components M := by
294+
dsimp [toTildeΓNatIso, fromTildeΓNatTrans, tilde.isoTop, moduleSpecΓFunctor, Sheaf.forget]
295+
rw [toOpen_fromTildeΓ_app]
296+
exact (modulesSpecToSheaf.obj M).val.map_id _
297+
298+
instance : IsIso (tilde.adjunction (R := R)).unit := by
299+
dsimp [tilde.adjunction]; infer_instance
300+
301+
/-- The tilde functor is fully faithful. We will later show that the essential image is
302+
exactly quasi-coherent modules. -/
303+
def tilde.fullyFaithfulFunctor : (tilde.functor R).FullyFaithful :=
304+
tilde.adjunction.fullyFaithfulLOfIsIsoUnit
305+
306+
instance : (tilde.functor (R := R)).Full := tilde.fullyFaithfulFunctor.full
307+
instance : (tilde.functor (R := R)).Faithful :=
308+
tilde.fullyFaithfulFunctor.faithful
309+
instance : (tilde.functor (R := R)).IsLeftAdjoint := tilde.adjunction.isLeftAdjoint
310+
311+
end AlgebraicGeometry
312+
313+
namespace ModuleCat
104314

105-
end Tilde
315+
@[deprecated (since := "2026-02-11")] noncomputable alias tilde := AlgebraicGeometry.tilde
316+
@[deprecated (since := "2026-02-11")] noncomputable alias Tilde.toOpen := tilde.toOpen
317+
@[deprecated (since := "2026-02-11")] alias Tilde.toOpen_res := tilde.toOpen_res
318+
@[deprecated (since := "2026-02-11")] noncomputable alias Tilde.toStalk := tilde.toStalk
106319

107320
end ModuleCat

0 commit comments

Comments
 (0)