AffineGeometry.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Scheme-theoretic meaning of the coordinate-ring formulation

An algebra equivalence with a polynomial ring yields an isomorphism to affine space over the coefficient field. The quotient presentation also supplies a closed immersion, so neither assertion is encoded by a bare bijection of points.

def OAI.StableCoordinate.AffineGeometry.algebraSpec line 28
Source documentation
The spectrum of a k-algebra, viewed as a scheme over Spec k.
```
def algebraSpec (k A : Type u) [CommRing k] [CommRing A] [Algebra k A] :
    Over (Spec (CommRingCat.of k)) :=
…
```
def OAI.StableCoordinate.AffineGeometry.specIsoOfAlgEquiv line 33
Source documentation
Contravariance takes an algebra equivalence to an actual scheme isomorphism.
```
def specIsoOfAlgEquiv (e : A ≃ₐ[k] B) :
    Spec (CommRingCat.of B) ≅ Spec (CommRingCat.of A) :=
…
```
theorem OAI.StableCoordinate.AffineGeometry.specIsoOfAlgEquiv_hom_over line 38
Source documentation
This scheme isomorphism respects the coefficient base scheme.
```
theorem specIsoOfAlgEquiv_hom_over (e : A ≃ₐ[k] B) :
    (specIsoOfAlgEquiv e).hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k A)) =
      Spec.map (CommRingCat.ofHom (algebraMap k B)) := by
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.specIsoOfAlgEquiv
def OAI.StableCoordinate.AffineGeometry.algebraSpecIso line 48
Source documentation
The stronger isomorphism in the category of schemes over Spec k.
```
def algebraSpecIso (e : A ≃ₐ[k] B) : algebraSpec k B ≅ algebraSpec k A :=
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.algebraSpec
def OAI.StableCoordinate.AffineGeometry.ringEquivOfSpecIso line 52
Source documentation
Full faithfulness of Spec recovers the ring map from every affine scheme isomorphism.
```
def ringEquivOfSpecIso
    (e : Spec (CommRingCat.of B) ≅ Spec (CommRingCat.of A)) : A ≃+* B :=
…
```
theorem OAI.StableCoordinate.AffineGeometry.ringEquivOfSpecIso_apply line 57
Source documentation
The recovered ring equivalence is exactly the pullback of the original morphism.
```
theorem ringEquivOfSpecIso_apply
    (e : Spec (CommRingCat.of B) ≅ Spec (CommRingCat.of A)) (a : A) :
    ringEquivOfSpecIso e a = Spec.preimage e.hom a := rfl
```
Mentions: OAI.StableCoordinate.AffineGeometry.ringEquivOfSpecIso
def OAI.StableCoordinate.AffineGeometry.algEquivOfSpecIso line 63
Source documentation
Every affine scheme isomorphism over the coefficient base induces an algebra isomorphism. Thus algebra automorphisms do not omit any ambient automorphisms.
```
def algEquivOfSpecIso
    (e : Spec (CommRingCat.of B) ≅ Spec (CommRingCat.of A))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k A)) =
      Spec.map (CommRingCat.ofHom (algebraMap k B))) : A ≃ₐ[k] B :=
…
```
def OAI.StableCoordinate.AffineGeometry.algEquivOfAlgebraSpecIso line 75
Source documentation
In particular, every automorphism in the category of schemes over Spec k is accounted for by an algebra automorphism.
```
def algEquivOfAlgebraSpecIso (e : algebraSpec k B ≅ algebraSpec k A) : A ≃ₐ[k] B :=
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.algebraSpec
theorem OAI.StableCoordinate.AffineGeometry.specIsoOfAlgEquiv_algEquivOfSpecIso line 79
Source documentation
Recovering the algebra map and applying Spec returns the given isomorphism.
```
theorem specIsoOfAlgEquiv_algEquivOfSpecIso
    (e : Spec (CommRingCat.of B) ≅ Spec (CommRingCat.of A))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k A)) =
      Spec.map (CommRingCat.ofHom (algebraMap k B))) :
    specIsoOfAlgEquiv (algEquivOfSpecIso e he) = e := by
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.specIsoOfAlgEquiv, OAI.StableCoordinate.AffineGeometry.algEquivOfSpecIso
theorem OAI.StableCoordinate.AffineGeometry.nonempty_algEquiv_iff_algebraSpecIso line 89
Source documentation
The ring and scheme-over-base existence formulations are equivalent.
```
theorem nonempty_algEquiv_iff_algebraSpecIso :
    Nonempty (A ≃ₐ[k] B) ↔ Nonempty (algebraSpec k B ≅ algebraSpec k A) :=
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.algebraSpec
theorem OAI.StableCoordinate.AffineGeometry.specIso_image_zeroLocus_of_ideal_map line 95
Source documentation
Transporting a defining ideal transports its closed subset by the associated ambient scheme isomorphism (with the contravariant direction made explicit).
```
theorem specIso_image_zeroLocus_of_ideal_map
    (e : A ≃ₐ[k] B) (I : Ideal A) (J : Ideal B)
    (h : I.map e.toRingHom = J) :
    (specIsoOfAlgEquiv e.symm).hom ''
        PrimeSpectrum.zeroLocus (I : Set A) = PrimeSpectrum.zeroLocus (J : Set B) := by
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.specIsoOfAlgEquiv

theorem OAI.StableCoordinate.AffineGeometry.ideal_map_of_specIso_image_zeroLocus line 108

Source documentation

Conversely, equality of the closed subsets under any ambient scheme isomorphism over the base recovers equality of their radical defining ideals.

theorem ideal_map_of_specIso_image_zeroLocus
    (I : Ideal B) (J : Ideal A) (hI : I.IsRadical) (hJ : J.IsRadical)
    (e : Spec (CommRingCat.of B) ≅ Spec (CommRingCat.of A))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k A)) =
      Spec.map (CommRingCat.ofHom (algebraMap k B)))
    (h : e.hom '' PrimeSpectrum.zeroLocus (I : Set B) =
      PrimeSpectrum.zeroLocus (J : Set A)) :
    I.map (algEquivOfSpecIso e he).symm.toRingHom = J := by
…

Mentions: OAI.StableCoordinate.AffineGeometry.algEquivOfSpecIso

theorem OAI.StableCoordinate.AffineGeometry.ideal_transport_iff_scheme_transport line 135

Source documentation

For radical defining ideals, the algebraic orbit condition is equivalent to the geometric orbit condition under all ambient automorphisms over the base.

theorem ideal_transport_iff_scheme_transport (I J : Ideal A)
    (hI : I.IsRadical) (hJ : J.IsRadical) :
    (∃ e : A ≃ₐ[k] A, I.map e.toRingHom = J) ↔
      ∃ e : Spec (CommRingCat.of A) ≅ Spec (CommRingCat.of A),
        (e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k A)) =
          Spec.map (CommRingCat.ofHom (algebraMap k A))) ∧
        e.hom '' PrimeSpectrum.zeroLocus (I : Set A) =
          PrimeSpectrum.zeroLocus (J : Set A) := by
…

def OAI.StableCoordinate.AffineGeometry.affineSpaceIsoOfAlgEquiv line 153
Source documentation
A polynomial-ring algebra presentation gives affine space as a scheme, not just its underlying collection of rational points.
```
def affineSpaceIsoOfAlgEquiv {σ : Type u} (e : A ≃ₐ[k] MvPolynomial σ k) :
    Spec (CommRingCat.of A) ≅ AffineSpace σ (Spec (CommRingCat.of k)) :=
…
```

theorem OAI.StableCoordinate.AffineGeometry.affineSpaceIsoOfAlgEquiv_hom_over line 158

Source documentation

The polynomial presentation isomorphism is an isomorphism over Spec k.

theorem affineSpaceIsoOfAlgEquiv_hom_over {σ : Type u}
    (e : A ≃ₐ[k] MvPolynomial σ k) :
    (affineSpaceIsoOfAlgEquiv e).hom ≫
      (AffineSpace σ (Spec (CommRingCat.of k)) ↘ Spec (CommRingCat.of k)) =
      Spec.map (CommRingCat.ofHom (algebraMap k A)) := by
…

Mentions: OAI.StableCoordinate.AffineGeometry.affineSpaceIsoOfAlgEquiv

def OAI.StableCoordinate.AffineGeometry.affineSpaceOverIsoOfAlgEquiv line 168
Source documentation
Scheme-over-base version of polynomial-ring coordinates.
```
def affineSpaceOverIsoOfAlgEquiv {σ : Type u}
    (e : A ≃ₐ[k] MvPolynomial σ k) :
    algebraSpec k A ≅ Over.mk
      (AffineSpace σ (Spec (CommRingCat.of k)) ↘ Spec (CommRingCat.of k)) :=
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.algebraSpec
def OAI.StableCoordinate.AffineGeometry.quotientEmbedding line 175
Source documentation
The natural map from the spectrum of a quotient into the ambient affine scheme.
```
def quotientEmbedding (I : Ideal A) :
    Spec (CommRingCat.of (A ⧸ I)) ⟶ Spec (CommRingCat.of A) :=
…
```
instance OAI.StableCoordinate.AffineGeometry.quotientEmbedding_isClosedImmersion line 180
Source documentation
This is genuinely a closed immersion.
```
instance quotientEmbedding_isClosedImmersion (I : Ideal A) :
    IsClosedImmersion (quotientEmbedding I) :=
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.quotientEmbedding
theorem OAI.StableCoordinate.AffineGeometry.quotientEmbedding_range line 185
Source documentation
The embedded image is exactly the closed subset defined by the ideal.
```
theorem quotientEmbedding_range (I : Ideal A) :
    Set.range (quotientEmbedding I) = PrimeSpectrum.zeroLocus (I : Set A) := by
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.quotientEmbedding

def OAI.StableCoordinate.AffineGeometry.hypersurfaceIsoOfAlgEquiv line 193

Source documentation

In particular every algebra equivalence of a hypersurface coordinate ring with a polynomial algebra gives the required affine-space isomorphism.

def hypersurfaceIsoOfAlgEquiv {σ τ : Type u}
    (p : MvPolynomial σ k)
    (e : (MvPolynomial σ k ⧸ Ideal.span {p}) ≃ₐ[k] MvPolynomial τ k) :
    Spec (CommRingCat.of (MvPolynomial σ k ⧸ Ideal.span {p})) ≅
      AffineSpace τ (Spec (CommRingCat.of k)) :=
…