Def AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection

Modification history

2026-09-04 11:59
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …
Modified AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSectionView on Github →
2024-12-13 13:44
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
refactor(Algebra/Category/Ring): make morphisms a structure (#19757) …
Modified AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSectionView on Github →
2024-06-11 06:47
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): morphism of locally ringed space $\mathrm{Proj}|_{D(f)} -> \mathrm{Spec} A^0_f$ (#13689) …
Added AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSectionView on Github →