Commit 2026-06-01 16:49 c6da5183

View on Github →

chore(AlgebraicGeometry): API for Scheme.Modules.restrict (#40057) In particular, we add an isomorphism Γ(M.restrict f, U) ≅ Γ(M, f ''ᵁ U), defined by Iso.refl _. Previously, we had a simp (!) lemma Γ(M.restrict f, U) = Γ(M, f ''ᵁ U). Since this is a non-reducible equality of objects, it caused many complications while working on #40052.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

added theorem AlgebraicGeometry.Scheme.Modules.map_comp_smul

added theorem AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom

added def AlgebraicGeometry.Scheme.Modules.restrictAppIso

added theorem AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map

modified theorem AlgebraicGeometry.Scheme.Modules.restrict_map

modified theorem AlgebraicGeometry.Scheme.Modules.restrict_obj

added def AlgebraicGeometry.Scheme.Modules.smul

added theorem AlgebraicGeometry.Scheme.Modules.smul_apply

added theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom

added theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

added theorem AlgebraicGeometry.Scheme.Modules.Scheme.Modules.restrictAppIso_smul_Spec

added theorem AlgebraicGeometry.Scheme.Modules.isSMulRegular_of_le_basicOpen

added theorem AlgebraicGeometry.Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen

added theorem AlgebraicGeometry.Scheme.Modules.map_smul_Spec

added theorem AlgebraicGeometry.Scheme.Modules.smul_Spec_def

deleted theorem AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen