Commit 2026-02-12 07:09 134bd660

View on Github →

feat(AlgebraicGeometry): tilde-Gamma adjunction (#35123)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

added theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app

added def AlgebraicGeometry.SpecModulesToSheafFullyFaithful

added def AlgebraicGeometry.moduleSpecΓFunctor

added def AlgebraicGeometry.modulesSpecToSheaf

added def AlgebraicGeometry.tilde.adjunction

added def AlgebraicGeometry.tilde.fullyFaithfulFunctor

added theorem AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen

added def AlgebraicGeometry.tilde.modulesSpecToSheafIso

added def AlgebraicGeometry.tilde.toOpen

added theorem AlgebraicGeometry.tilde.toOpen_map_app

added theorem AlgebraicGeometry.tilde.toOpen_res

added def AlgebraicGeometry.tilde.toTildeΓNatIso

added def AlgebraicGeometry.tilde

deleted theorem ModuleCat.Tilde.res_apply

deleted theorem ModuleCat.Tilde.smul_section_apply

deleted theorem ModuleCat.Tilde.smul_stalk_no_nonzero_divisor

deleted theorem ModuleCat.Tilde.toOpen_res