Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
# Nonsingular points and the group law in Jacobian coordinates

Let `W` be a Weierstrass curve over a field `F`. The nonsingular Jacobian points of `W` can be
endowed with an group law, which is uniquely determined by the formulae in
endowed with a group law, which is uniquely determined by the formulae in
`Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean` and follows from an equivalence with
the nonsingular points `W⟮F⟯` in affine coordinates.

Expand Down Expand Up @@ -42,9 +42,9 @@ the nonsingularity condition already implies `(x, y, z) ≠ (0, 0, 0)`, so a non
point on `W` can be given by `[x : y : z]` and the nonsingular condition on any representative.

A nonsingular Jacobian point representative can be converted to a nonsingular point in affine
coordinates using `WeiestrassCurve.Jacobian.Point.toAffine`, which lifts to a map on nonsingular
Jacobian points using `WeiestrassCurve.Jacobian.Point.toAffineLift`. Conversely, a nonsingular point
in affine coordinates can be converted to a nonsingular Jacobian point using
coordinates using `WeierstrassCurve.Jacobian.Point.toAffine`, which lifts to a map on nonsingular
Jacobian points using `WeierstrassCurve.Jacobian.Point.toAffineLift`. Conversely, a nonsingular
point in affine coordinates can be converted to a nonsingular Jacobian point using
`WeierstrassCurve.Jacobian.Point.fromAffine` or `WeierstrassCurve.Affine.Point.toJacobian`.

Whenever possible, all changes to documentation and naming of definitions and theorems should be
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
# Nonsingular points and the group law in projective coordinates

Let `W` be a Weierstrass curve over a field `F`. The nonsingular projective points of `W` can be
endowed with an group law, which is uniquely determined by the formulae in
endowed with a group law, which is uniquely determined by the formulae in
`Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean` and follows from an equivalence
with the nonsingular points `W⟮F⟯` in affine coordinates.

Expand Down Expand Up @@ -42,8 +42,8 @@ the nonsingularity condition already implies `(x, y, z) ≠ (0, 0, 0)`, so a non
point on `W` can be given by `[x : y : z]` and the nonsingular condition on any representative.

A nonsingular projective point representative can be converted to a nonsingular point in affine
coordinates using `WeiestrassCurve.Projective.Point.toAffine`, which lifts to a map on nonsingular
projective points using `WeiestrassCurve.Projective.Point.toAffineLift`. Conversely, a nonsingular
coordinates using `WeierstrassCurve.Projective.Point.toAffine`, which lifts to a map on nonsingular
projective points using `WeierstrassCurve.Projective.Point.toAffineLift`. Conversely, a nonsingular
point in affine coordinates can be converted to a nonsingular projective point using
`WeierstrassCurve.Projective.Point.fromAffine` or `WeierstrassCurve.Affine.Point.toProjective`.

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

In this file we define a constructor `affineAnd Q` for affine target morphism properties of schemes
from a property of ring homomorphisms `Q`: A morphism `f : X ⟶ Y` with affine target satisfies
`affineAnd Q` if it is an affine morphim (i.e. `X` is affine) and the induced ring map on global
`affineAnd Q` if it is an affine morphism (i.e. `X` is affine) and the induced ring map on global
sections satisfies `Q`.

`affineAnd Q` inherits most stability properties of `Q` and is local at the target if `Q` is local
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ which we call an `AffineTargetMorphismProperty`. In this file, we provide API le
local at the target, and special support for those properties whose `AffineTargetMorphismProperty`
takes on a more simple form. We also provide API lemmas for properties local at the target.
The main interfaces of the API are the typeclasses `IsLocalAtTarget`, `IsLocalAtSource` and
`HasAffineProperty`, which we describle in detail below.
`HasAffineProperty`, which we describe in detail below.

## `IsZariskiLocalAtTarget`

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ properties:
`MorphismProperty.targetAffineLocally_toAffineTargetMorphismProperty_eq_of_isZariskiLocalAtTarget`
- `MorphismProperty.topologically`: Given a property `P` of maps of topological spaces,
`(topologically P) f` holds if `P` holds for the underlying continuous map of `f`.
- `MorphismProperty.stalkwise`: Given a property `P` of ring homs,
- `MorphismProperty.stalkwise`: Given a property `P` of ring homomorphisms,
`(stalkwise P) f` holds if `P` holds for all stalk maps.

Also provides API for showing the standard locality and stability properties for these
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,8 @@ of quasi-compact open sets are quasi-compact.
-/
@[mk_iff]
class QuasiCompact (f : X ⟶ Y) : Prop where
/-- Preimage of compact open set under a quasi-compact morphism between schemes is compact. -/
/-- The preimage of a compact open set under a quasi-compact morphism between schemes is
compact. -/
isCompact_preimage : ∀ U : Set Y, IsOpen U → IsCompact U → IsCompact (f ⁻¹' U)

variable {f} in
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

# Separated morphisms

A morphism of schemes is separated if its diagonal morphism is a closed immmersion.
A morphism of schemes is separated if its diagonal morphism is a closed immersion.

## Main definitions
- `AlgebraicGeometry.IsSeparated`: The class of separated morphisms.
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/OpenImmersion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ def opensFunctor : X.Opens ⥤ Y.Opens :=
LocallyRingedSpace.IsOpenImmersion.opensFunctor f.toLRSHom

/-- `f ''ᵁ U` is notation for the image (as an open set) of `U` under an open immersion `f`.
The prefered name in lemmas is `image` and it should be treated as an infix. -/
The preferred name in lemmas is `image` and it should be treated as an infix. -/
scoped[AlgebraicGeometry] notation3:90 f:91 " ''ᵁ " U:90 => (Scheme.Hom.opensFunctor f).obj U

@[simp] lemma coe_image {U : X.Opens} : f ''ᵁ U = f '' U := rfl
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/PointsPi.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Immersion
# `Π Rᵢ`-Points of Schemes

We show that the canonical map `X(Π Rᵢ) ⟶ Π X(Rᵢ)` (`AlgebraicGeometry.pointsPi`)
is injective and surjective under various assumptions
is injective and surjective under various assumptions.

-/

Expand Down
5 changes: 3 additions & 2 deletions Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,13 @@ structure sheaf so that `Proj` is a locally ringed space. In this file we will p
equipped with this structure sheaf is a scheme. We achieve this by using an affine cover by basic
open sets in `Proj`, more specifically:

1. We prove that `Proj` can be covered by basic open sets at homogeneous element of positive degree.
1. We prove that `Proj` can be covered by basic open sets at homogeneous elements of positive
degree.
2. We prove that for any homogeneous element `f : A` of positive degree `m`, `Proj.T | (pbo f)` is
homeomorphic to `Spec.T A⁰_f`:
- forward direction `toSpec`:
for any `x : pbo f`, i.e. a relevant homogeneous prime ideal `x`, send it to
`A⁰_f ∩ span {g / 1 | g ∈ x}` (see `ProjIsoSpecTopComponent.IoSpec.carrier`). This ideal is
`A⁰_f ∩ span {g / 1 | g ∈ x}` (see `ProjIsoSpecTopComponent.ToSpec.carrier`). This ideal is
prime, the proof is in `ProjIsoSpecTopComponent.ToSpec.toFun`. The fact that this function
is continuous is found in `ProjIsoSpecTopComponent.toSpec`
- backward direction `fromSpec`:
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/QuasiAffine.lean
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ private lemma IsQuasiAffine.of_isOpenImmersion [CompactSpace X]
simp [toSpecΓ_naturality]
· infer_instance

/-- Any quasicompact locally closed subscheme of an quasi-affine scheme is quasi-affine. -/
/-- Any quasicompact locally closed subscheme of a quasi-affine scheme is quasi-affine. -/
@[stacks 0BCK]
lemma IsQuasiAffine.of_isImmersion
[Y.IsQuasiAffine] [IsImmersion f] [CompactSpace X] : X.IsQuasiAffine := by
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/Scheme.lean
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ instance : Category Scheme where
comp f g := Hom.mk (f.toLRSHom ≫ g.toLRSHom)

/-- `f ⁻¹ᵁ U` is notation for `(Opens.map f.base).obj U`, the preimage of an open set `U` under `f`.
The prefered name in lemmas is `preimage` and it should be treated as an infix. -/
The preferred name in lemmas is `preimage` and it should be treated as an infix. -/
scoped[AlgebraicGeometry] notation3:90 f:91 " ⁻¹ᵁ " U:90 =>
@Functor.obj (Scheme.Opens _) _ (Scheme.Opens _) _
(Opens.map (f : Scheme.Hom _ _).base) U
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ import Mathlib.RingTheory.Valuation.LocalSubring
it is quasi-separated and satisfies the uniqueness part of the valuative criterion.
- `AlgebraicGeometry.IsProper.eq_valuativeCriterion`:
A morphism is proper if and only if
it is qcqs and of fintite type and satisfies the valuative criterion.
it is qcqs and of finite type and satisfies the valuative criterion.

## Future projects
Show that it suffices to check discrete valuation rings when the base is Noetherian.
Expand Down