File tree Expand file tree Collapse file tree
Mathlib/AlgebraicGeometry Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -47,8 +47,8 @@ which is a special case where the conditions are easier to check.
4747
4848 ## Implementation details
4949
50- All the hard work is done in `AlgebraicGeometry/ PresheafedSpace/Gluing.lean` where we glue
51- presheafed spaces, sheafed spaces, and locally ringed spaces.
50+ All the hard work is done in `Mathlib/Geometry/RingedSpace/ PresheafedSpace/Gluing.lean` where we
51+ glue presheafed spaces, sheafed spaces, and locally ringed spaces.
5252
5353-/
5454
Original file line number Diff line number Diff line change @@ -13,8 +13,8 @@ public import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
1313/-!
1414# The structure sheaf on `ProjectiveSpectrum 𝒜`.
1515
16- In `Mathlib/AlgebraicGeometry/Topology.lean`, we have given a topology on `ProjectiveSpectrum 𝒜`; in
17- this file we will construct a sheaf on `ProjectiveSpectrum 𝒜`.
16+ In `Mathlib/AlgebraicGeometry/ProjectiveSpectrum/ Topology.lean`, we have given a topology on
17+ `ProjectiveSpectrum 𝒜`; in this file we will construct a sheaf on `ProjectiveSpectrum 𝒜`.
1818
1919## Notation
2020- `A` is a commutative ring;
You can’t perform that action at this time.
0 commit comments