Commit 2024-07-12 13:34 d9e0e06d

View on Github →

feat(AlgebraicGeometry/Modules/Tilde): construct the tilde sheaf associated to a module (#14231) This PR was done during the AIM workshop Formalizing Algebraic Geometry.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Modules/Tilde.lean

added def ModuleCat.Tilde.isFraction

added def ModuleCat.Tilde.isFractionPrelocal

added def ModuleCat.Tilde.isLocallyFraction

added theorem ModuleCat.Tilde.isLocallyFraction_pred

added def ModuleCat.Tilde.sectionsSubmodule

added theorem ModuleCat.Tilde.sections_smul_localizations_def

added def ModuleCat.preTildeInAddCommGrp

added def ModuleCat.tildeInAddCommGrp

added def ModuleCat.tildeInType