10.24 Glueing functions to 10.43 Geometrically reduced…

Section10.24 Glueing functions#

Section 10.24 of the Stacks Project, Tag 00EI. 5 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00EK, a lemma

Tag 00EK in the Stacks Project.

IsLocalizedModule.Away.injective_pi_and_exact_of_span_range_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Localization/Exactness.lean, line 294.

Let R be a commutative semiring, let f : ι → R be a family of elements generating the unit ideal and let M be an R-module. Let Mf i be the localization of M away from f i, with localization map g i, and let Mff i j be the localization of M away from f i * f j, reached from Mf i by l i j and from Mf j by r i j. Then the sequence 0 → M → ∏ i, Mf i → ∏ (i, j), Mff i j is exact, the first map being m ↦ (g i m) and the second (m i) ↦ (l i j (m i) - r i j (m j)).

public theorem injective_pi_and_exact_of_span_range_eq_top
    (hf : Ideal.span (Set.range f) = ⊤)
    (hlr : ∀ i j, (l i j).comp (g i) = (r i j).comp (g j)) :
    Function.Injective (LinearMap.pi g) ∧
      Function.Exact (LinearMap.pi g) (LinearMap.pi fun p : ι × ι ↦
        (l p.1 p.2).comp (LinearMap.proj p.1) - (r p.1 p.2).comp (LinearMap.proj p.2))
Tag 00EJ, a lemma

Tag 00EJ in the Stacks Project.

alphaLin_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/Functions.lean, line 125. The attribute's comment: “exactness at R, i.e. injectivity of α”.

If f generates the unit ideal, then α is injective.

theorem alphaLin_injective (hf : Ideal.span (Set.range f) = ⊤) :
    Function.Injective (alphaLin R n f)

ker_betaLin_eq_range_alphaLin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/Functions.lean, line 234. The attribute's comment: “exactness at the middle term, i.e. ker β = im α”.

If f generates the unit ideal, then the kernel of β equals the range of α.

theorem ker_betaLin_eq_range_alphaLin (hf : Ideal.span (Set.range f) = ⊤) :
    LinearMap.ker (betaLin R n f) = LinearMap.range (alphaLin R n f)
Tag 00EM, a lemma

Tag 00EM in the Stacks Project.

PrimeSpectrum.exists_ringEquiv_prod_of_isOpen_of_isCompl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/ConnectedComponents.lean, line 538.

A disjoint open cover of Spec R yields a product decomposition of R.

Let R be a commutative ring with Spec(R) = U ⊔ V for two open subsets U, V. Then there is an idempotent e ∈ R such that, setting R₁ := R⧸(1-e) and R₂ := R⧸e:

  • the canonical ring map φ := RingHom.quotientProdOneSub e : R →+* R₁ × R₂ lifts to a ring isomorphism R ≃+* R₁ × R₂;
  • Spec(R₁) is homeomorphic to U (as a subspace of Spec R) and Spec(R₂) is homeomorphic to V, with both homeomorphisms realised by the canonical maps of the product decomposition, i.e. via PrimeSpectrum.primeSpectrumProdHomeo;
  • each factor is simultaneously a quotient and a localization of R: the quotient maps make R₁ a localization at e and R₂ a localization at 1 - e.
theorem PrimeSpectrum.exists_ringEquiv_prod_of_isOpen_of_isCompl
    {R : Type*} [CommRing R]
    {U V : Set (PrimeSpectrum R)}
    (hU : IsOpen U) (hV : IsOpen V)
    (h : IsCompl U V) :
    ∃ e : R, IsIdempotentElem e ∧
      ∃ φ : R ≃+* (R ⧸ Ideal.span ({1 - e} : Set R)) ×
                  (R ⧸ Ideal.span ({e} : Set R)),
        (φ : R →+* (R ⧸ Ideal.span ({1 - e} : Set R)) ×
                   (R ⧸ Ideal.span ({e} : Set R))) = RingHom.quotientProdOneSub e ∧
        (∃ eU : PrimeSpectrum (R ⧸ Ideal.span ({1 - e} : Set R)) ≃ₜ U,
          ∀ p, (eU p).1 =
            PrimeSpectrum.comap
              (φ : R →+* (R ⧸ Ideal.span ({1 - e} : Set R)) ×
                         (R ⧸ Ideal.span ({e} : Set R)))
              (PrimeSpectrum.primeSpectrumProdHomeo.symm (Sum.inl p))) ∧
        (∃ eV : PrimeSpectrum (R ⧸ Ideal.span ({e} : Set R)) ≃ₜ V,
          ∀ p, (eV p).1 =
            PrimeSpectrum.comap
              (φ : R →+* (R ⧸ Ideal.span ({1 - e} : Set R)) ×
                         (R ⧸ Ideal.span ({e} : Set R)))
              (PrimeSpectrum.primeSpectrumProdHomeo.symm (Sum.inr p))) ∧
        IsLocalization.Away e (R ⧸ Ideal.span ({1 - e} : Set R)) ∧
        IsLocalization.Away (1 - e) (R ⧸ Ideal.span ({e} : Set R))
Tag 0565, a lemma

Tag 0565 in the Stacks Project.

bigLambda_injective_iff_bigPhi_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/Functions.lean, line 429.

The map Λ : M → ⨁_i M_{f_i}, m ↦ (m/1, ..., m/1), is injective if and only if the map Φ : M → ⨁_i M, m ↦ (f_1 m, ..., f_n m), is injective.

theorem bigLambda_injective_iff_bigPhi_injective
    (n : ℕ) (f : Fin n → R) :
    Function.Injective (bigLambda (M := M) n f) ↔ Function.Injective (bigPhi (M := M) n f)
Tag 00EQ, a lemma

Tag 00EQ in the Stacks Project.

ModuleGluingData.psi_apply_of_mem_gluedModule, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/Modules.lean, line 272. The attribute's comment: “moreover clause: ψ i j (m/1) = m/1 for m in the glued module”.

For m ∈ gluedModule, the gluing relation holds: ψ i j (m_i/1) = m_j/1.

lemma psi_apply_of_mem_gluedModule
    (D : ModuleGluingData ι f) (m : D.gluedModule) (i j : ι) :
    D.ψ i j (LocalizedModule.mkLinearMap (Submonoid.powers (f j))
              (D.M i) ((m : D.DirectSumM) i)) =
      LocalizedModule.mkLinearMap (Submonoid.powers (f i)) (D.M j) ((m : D.DirectSumM) j)

ModuleGluingData.proj_isLocalizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/Modules.lean, line 452. The attribute's comment: “localization comparison”.

Stacks 00EQ (localization comparison). For finite module gluing data, projection to the i-th component is the localization map at the powers of f i. Thus the induced canonical map from the localization of the glued module to D.M i is an isomorphism.

theorem proj_isLocalizedModule (D : ModuleGluingData ι f) (i : ι) :
    IsLocalizedModule (Submonoid.powers (f i)) (D.proj i)
Sources
LeanIsLocalizedModule.Away.injective_pi_and_exact_of_span_range_eq_top · alphaLin_injective · ker_betaLin_eq_range_alphaLin · PrimeSpectrum.exists_ringEquiv_prod_of_isOpen_of_isCompl · bigLambda_injective_iff_bigPhi_injective · ModuleGluingData.psi_apply_of_mem_gluedModule · ModuleGluingData.proj_isLocalizedModule

Section10.25 Zerodivisors and total rings of fractions#

Section 10.25 of the Stacks Project, Tag 02LV. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00EU, a lemma

Tag 00EU in the Stacks Project.

Declarations registered for the tag:

Tag 00EW, a lemma

Tag 00EW in the Stacks Project.

isField_localizationAtPrime_of_minimal, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MinimalPrimes/Reduced.lean, line 112. The attribute's comment: “2, the factors are fields”. References: EGA 0 (1.5.8), “reduced ring”; EGA IV (20.1.3.1), “field-stalk clause”.

The localization of a reduced ring at a minimal prime is a field.

lemma isField_localizationAtPrime_of_minimal (R : Type*) [CommRing R] [IsReduced R]
    (p : Ideal R) (hp : p ∈ minimalPrimes R) :
    haveI : p.IsPrime := hp.isPrime
    IsField (Localization.AtPrime p)

localizationProdMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MinimalPrimes/Reduced.lean, line 154. The attribute's comment: “2, injectivity; the factors are fields by isField_localizationAtPrime_of_minimal”.

The map R → ∏_{p minimal} R_p from a reduced commutative ring to the product of localizations at minimal primes is injective.

theorem localizationProdMap_injective (R : Type*) [CommRing R] [IsReduced R] :
    Function.Injective (localizationProdMap R)

exists_injective_ringHom_pi_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MinimalPrimes/Reduced.lean, line 166. The attribute's comment: “1”.

A reduced commutative ring embeds into a product of fields, indexed by a type in the universe of R.

theorem exists_injective_ringHom_pi_field.{u} {R : Type u} [CommRing R]
    [IsReduced R] :
    ∃ (ι : Type u) (K : ι → Type u) (_ : ∀ i, Field (K i))
      (f : R →+* (∀ i, K i)), Function.Injective f

iUnion_minimalPrimes_eq_zeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MinimalPrimes/Reduced.lean, line 205. The attribute's comment: “3”. References: EGA IV (20.1.3.1), “special case”.

The union of the minimal primes of a reduced commutative ring equals its set of zero divisors.

theorem iUnion_minimalPrimes_eq_zeroDivisors (R : Type*) [CommRing R] [IsReduced R] :
    (⋃ p ∈ minimalPrimes R, (p : Set R)) = zeroDivisorSet R
Tag 02LW, a lemma

Tag 02LW in the Stacks Project.

fractionRing_equiv_fractionRing_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/FractionRing.lean, line 54.

The total ring of fractions of R is isomorphic (as a ring) to the total ring of fractions of S⁻¹R, whenever S is a multiplicative subset of R consisting of nonzerodivisors.

theorem fractionRing_equiv_fractionRing_localization
    (R : Type*) [CommRing R] (S : Submonoid R) (hS : S ≤ nonZeroDivisors R) :
    Nonempty (FractionRing R ≃+* FractionRing (Localization S))

fractionRing_equiv_fractionRing_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/FractionRing.lean, line 71.

The total ring of fractions of R is isomorphic to the total ring of fractions of its own total ring of fractions: Q(R) ≅ Q(Q(R)).

theorem fractionRing_equiv_fractionRing_fractionRing
    (R : Type*) [CommRing R] :
    Nonempty (FractionRing R ≃+* FractionRing (FractionRing R))
Tag 02LX, a lemma

Tag 02LX in the Stacks Project.

total_fraction_ring_isoProd_localization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/FractionRing.lean, line 183. References: EGA II (6.4.7), “partial”.

Let R be a commutative ring whose set of minimal primes is finite and enumerated without repetition as q_1, ..., q_t (encoded by an injective family q : Fin t → Ideal R of minimal primes; the zerodivisor hypothesis forces it to enumerate every minimal prime). Assume moreover that the union of the minimal primes equals the set of zerodivisors of R. Then the total ring of fractions Q(R) = FractionRing R is isomorphic, as an R-algebra, to the finite product of the localizations R_{q_i}.

(An R-algebra isomorphism between these localizations is automatically the canonical map induced by the universal property, since it must commute with the structure maps from R.)

theorem total_fraction_ring_isoProd_localization_atPrime
    {R : Type*} [CommRing R] (t : ℕ) (q : Fin t → Ideal R)
    (hmin : ∀ i, q i ∈ minimalPrimes R)
    (hinj : Function.Injective q)
    (hzd : zeroDivisorsSet R = ⋃ i, (q i : Set R)) :
    haveI : ∀ i, (q i).IsPrime := fun i => (hmin i).isPrime
    Nonempty (FractionRing R ≃ₐ[R] (∀ i, Localization.AtPrime (q i)))
Sources
LeanRing.KrullDimLE.of_isLocalization · Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal · Ring.KrullDimLE.isField_of_isReduced · isField_localizationAtPrime_of_minimal · localizationProdMap_injective · exists_injective_ringHom_pi_field · iUnion_minimalPrimes_eq_zeroDivisors · fractionRing_equiv_fractionRing_localization

Section10.26 Irreducible components of spectra#

Section 10.26 of the Stacks Project, Tag 00ER. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 090M, a lemma

Tag 090M in the Stacks Project.

Declarations registered for the tag:

Tag 00ET, a lemma

Tag 00ET in the Stacks Project.

PrimeSpectrum.irreducibleClosedThroughEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/IrreducibleComponents.lean, line 53. The attribute's comment: “(1)”.

Part (1): The irreducible closed subsets of Spec(R) passing through 𝔭 correspond to the prime ideals of any localization S of R at 𝔭.

def irreducibleClosedThroughEquiv :
    irreducibleClosedThrough R 𝔭 ≃ { q : Ideal S // q.IsPrime }

PrimeSpectrum.irreducibleComponentsThroughEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/IrreducibleComponents.lean, line 149. The attribute's comment: “(2)”. References: EGA IV (5.1.12), “special case”.

Part (2): The irreducible components of Spec(R) passing through 𝔭 correspond to the minimal prime ideals of any localization S of R at 𝔭.

def irreducibleComponentsThroughEquiv :
    irreducibleComponentsThrough R 𝔭 ≃ minimalPrimes S
Tag 00EV, a lemma

Tag 00EV in the Stacks Project.

PrimeSpectrum.exists_disjoint_basicOpen_of_mem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MinimalPrimes/Reduced.lean, line 290.

Let 𝔭 be a minimal prime of R and let W ⊆ Spec R be a quasi-compact open not containing 𝔭. Then some f ∉ 𝔭 has D(f) disjoint from W.

theorem PrimeSpectrum.exists_disjoint_basicOpen_of_mem_minimalPrimes
    {R : Type*} [CommSemiring R]
    {𝔭 : Ideal R} (h𝔭min : 𝔭 ∈ minimalPrimes R)
    {W : TopologicalSpace.Opens (PrimeSpectrum R)}
    (hW : IsCompact (W : Set (PrimeSpectrum R)))
    (h𝔭W : (⟨𝔭, h𝔭min.isPrime⟩ : PrimeSpectrum R) ∉ W) :
    ∃ f ∉ 𝔭,
      Disjoint (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum R))
        (W : Set (PrimeSpectrum R))
Tag 04MG, a lemma

Tag 04MG in the Stacks Project.

spec_profinite_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Profinite.lean, line 184.

For a ring R the following are equivalent: Spec R is profinite; Spec R is Hausdorff; Spec R is totally disconnected; every quasi-compact open of Spec R is closed; there are no nontrivial inclusions between primes of R; every prime of R is maximal; every prime of R is a minimal prime; every basic open D(f) is closed.

theorem spec_profinite_tfae (R : Type*) [CommRing R] :
    [ -- (1) X is profinite: compact, Hausdorff, and totally disconnected
      CompactSpace (PrimeSpectrum R) ∧ T2Space (PrimeSpectrum R) ∧
        TotallyDisconnectedSpace (PrimeSpectrum R),
      -- (2) X is Hausdorff
      T2Space (PrimeSpectrum R),
      -- (3) X is totally disconnected
      TotallyDisconnectedSpace (PrimeSpectrum R),
      -- (4) every quasi-compact open subset of X is closed
      ∀ U : Set (PrimeSpectrum R), IsOpen U → IsCompact U → IsClosed U,
      -- (5) no nontrivial inclusions between prime ideals
      ∀ p q : Ideal R, p.IsPrime → q.IsPrime → p ≤ q → p = q,
      -- (6) every prime ideal is maximal
      ∀ p : Ideal R, p.IsPrime → p.IsMaximal,
      -- (7) every prime ideal is a minimal prime
      ∀ p : Ideal R, p.IsPrime → p ∈ minimalPrimes R,
      -- (8) every standard open D(f) is closed
      ∀ f : R, IsClosed (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum R)) ].TFAE
Sources
LeanPrimeSpectrum.instSpectralSpace · PrimeSpectrum.irreducibleClosedThroughEquiv · PrimeSpectrum.irreducibleComponentsThroughEquiv · PrimeSpectrum.exists_disjoint_basicOpen_of_mem_minimalPrimes · spec_profinite_tfae

Section10.27 Examples of spectra of rings#

Section 10.27 of the Stacks Project, Tag 00EX. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00EY, an example

Tag 00EY in the Stacks Project.

IntXSqSubFour.isPrime_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 178.

Classification of Spec(R) (Stacks Tag 00EY). An ideal p of R = ℤ[x]/(x² - 4) is prime if and only if it is one of the listed ideals: (2, x̄), or (q, x̄ - 2)/(q, x̄ + 2) for some odd prime q, or one of the two generic primes (x̄ - 2), (x̄ + 2).

A prime contains x̄ - 2 or x̄ + 2, since their product is 0. The evaluations R → ℤ, x̄ ↦ ±2, are surjective with kernels (x̄ ∓ 2), so the primes containing x̄ ∓ 2 are the preimages of the primes (0) and (q) of ℤ; for q = 2 both preimages are (2, x̄).

theorem isPrime_iff (p : Ideal IntXSqSubFour) :
    p.IsPrime ↔
      (p = p2 ∨
       (∃ q : ℕ, q.Prime ∧ Odd q ∧ (p = pMinus q ∨ p = pPlus q)) ∨
       p = gMinus ∨ p = gPlus)
Tag 00EZ, an example

Tag 00EZ in the Stacks Project.

Polynomial.isPrime_int_trichotomy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 303.

Stacks Tag 00EZ (Description of Spec(ℤ[x])).

Every prime ideal 𝔭 of ℤ[x] has one of the following forms: * 𝔭 = (0); * 𝔭 = (f) with f irreducible in ℤ[x]; this covers the nonzero primes with 𝔭 ∩ ℤ = (0) and the primes (q) (take f = q) for a prime number q; * 𝔭 = (q, f) for a prime number q and f irreducible in ℤ[x] whose reduction modulo q is irreducible in (ℤ/qℤ)[x].

The Stacks text omits the primes (q), which lie over (q) without being of the third form.

theorem Polynomial.isPrime_int_trichotomy
    (𝔭 : Ideal ℤ[X]) (h𝔭 : 𝔭.IsPrime) :
    𝔭 = ⊥ ∨
    (∃ f : ℤ[X], Irreducible f ∧ 𝔭 = Ideal.span {f}) ∨
    (∃ (q : ℕ) (f : ℤ[X]), q.Prime ∧
        Irreducible f ∧
        Irreducible (f.map (Int.castRingHom (ZMod q))) ∧
        𝔭 = Ideal.span {(C (q : ℤ)), f})
Tag 00F0, an example

Tag 00F0 in the Stacks Project.

Polynomial.isPrime_iff_eq_bot_or_eq_span_or_eq_span_pair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Polynomial.lean, line 312. The attribute's comment: “for R[X] over any principal ideal domain R; the tag is the case R = k[x]”.

Stacks 00F0, both directions: the prime ideals of R[X], for R a principal ideal domain. The tag is the case R = k[x] for a field k.

theorem isPrime_iff_eq_bot_or_eq_span_or_eq_span_pair [IsDomain R] [IsPrincipalIdealRing R]
    (P : Ideal R[X]) :
    P.IsPrime ↔ P = ⊥ ∨ (∃ f : R[X], Irreducible f ∧ P = span {f}) ∨
      (∃ (p : R) (f : R[X]), Irreducible p ∧
        Irreducible (Ideal.Quotient.mk (span {C p}) f) ∧ P = span {C p, f})
Tag 00F1, an example

Tag 00F1 in the Stacks Project.

NodalCubicAffineOpen.quotientSpanAlgEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 615. The attribute's comment: “R ≅ ℚ[A, B]/(A³ - B² + AB)”.

The isomorphism ℚ[A, B] / (A³ - B² + A·B) ≃ₐ[ℚ] R induced by φ.

def quotientSpanAlgEquiv :
    (MvPolynomial (Fin 2) ℚ ⧸ Ideal.span {((MvPolynomial.X 0 : MvPolynomial (Fin 2) ℚ) ^ 3 -
      MvPolynomial.X 1 ^ 2 + MvPolynomial.X 0 * MvPolynomial.X 1)}) ≃ₐ[ℚ] R

NodalCubicAffineOpen.isOpenEmbedding_comap_inclRToRa, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 792. The attribute's comment: “θ : Spec R_a → Spec R is an open embedding”.

The inclusion R ↪ R_a induces an open embedding θ : Spec R_a → Spec R.

theorem isOpenEmbedding_comap_inclRToRa (a : ℚ)
    (ha0 : a ≠ 0) (ha1 : a ≠ 1) :
    Topology.IsOpenEmbedding
      (PrimeSpectrum.comap (inclRToRa a ha0 ha1).toRingHom)

NodalCubicAffineOpen.range_comap_inclRToRa, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 806. The attribute's comment: “the image of θ is Spec R ∖ {𝔪_a}”.

The image of θ : Spec R_a → Spec R is exactly the complement of the closed point 𝔪_a in Spec R.

theorem range_comap_inclRToRa (a : ℚ)
    (ha0 : a ≠ 0) (ha1 : a ≠ 1) :
    Set.range (PrimeSpectrum.comap (inclRToRa a ha0 ha1).toRingHom) =
      {p : PrimeSpectrum R | p ≠ mRPoint a}

NodalCubicAffineOpen.range_comap_inclRToRa_ne_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 847.

Headline. The image of θ : Spec R_a → Spec R is not the basic open D(f) of any element f ∈ R. Hence Spec R_a ⊂ Spec R is an affine open which is not standard / principal.

theorem range_comap_inclRToRa_ne_basicOpen (a : ℚ)
    (ha0 : a ≠ 0) (ha1 : a ≠ 1) (ha12 : a ≠ 1 / 2) (f : R) :
    Set.range (PrimeSpectrum.comap (inclRToRa a ha0 ha1).toRingHom) ≠
      (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum R))

NodalCubicAffineOpen.not_exists_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Examples.lean, line 892. The attribute's comment: “R_a is not a localization of R”.

R_a is not a localization of R: there is no submonoid S ⊆ R for which R_a becomes the localization S⁻¹ R via inclRToRa.

theorem not_exists_isLocalization (a : ℚ)
    (ha0 : a ≠ 0) (ha1 : a ≠ 1) (ha12 : a ≠ 1 / 2) :
    let _ : Algebra R (Ra a ha0 ha1) := (inclRToRa a ha0 ha1).toAlgebra
    ¬ ∃ (S : Submonoid R), IsLocalization S (Ra a ha0 ha1)
Sources
LeanIntXSqSubFour.isPrime_iff · Polynomial.isPrime_int_trichotomy · Polynomial.isPrime_iff_eq_bot_or_eq_span_or_eq_span_pair · NodalCubicAffineOpen.quotientSpanAlgEquiv · NodalCubicAffineOpen.isOpenEmbedding_comap_inclRToRa · NodalCubicAffineOpen.range_comap_inclRToRa · NodalCubicAffineOpen.range_comap_inclRToRa_ne_basicOpen · NodalCubicAffineOpen.not_exists_isLocalization

Section10.28 A meta-observation about prime ideals#

Section 10.28 of the Stacks Project, Tag 05K7. 8 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 9 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05K8, a lemma

Tag 05K8 in the Stacks Project.

ideal_eq_mul_colon_of_isPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Colon.lean, line 29.

For a commutative ring R, a principal ideal J and an ideal I with I ≤ J, the ideal I factors as the product of J with the colon ideal (I : J).

theorem ideal_eq_mul_colon_of_isPrincipal {R : Type*} [CommRing R]
    (I J : Ideal R) (hJ : J.IsPrincipal) (hIJ : I ≤ J) :
    I = J * (I.colon J)
Tag 05KA, an example

Tag 05KA in the Stacks Project.

isOkaFamilyUniversal_meetsSubmonoidFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/OkaFamily.lean, line 93.

Stacks Tag 05KA. For a commutative semiring R and a multiplicative subset S of R, the family of ideals meeting S is an Oka family.

theorem isOkaFamilyUniversal_meetsSubmonoidFamily {R : Type*} [CommSemiring R]
    (S : Submonoid R) : IsOkaFamilyUniversal (meetsSubmonoidFamily S)
Tag 05KB, an example

Tag 05KB in the Stacks Project.

Declarations registered for the tag:

Tag 05KC, an example

Tag 05KC in the Stacks Project.

Declarations registered for the tag:

Tag 05KF, a lemma

Tag 05KF in the Stacks Project.

Declarations registered for the tag:

Tag 05KG, a lemma

Tag 05KG in the Stacks Project.

Declarations registered for the tag:

Tag 05KH, a lemma

Tag 05KH in the Stacks Project.

Declarations registered for the tag:

Tag 05KI, a lemma

Tag 05KI in the Stacks Project.

Ideal.isPrime_of_maximal_disjoint_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/MaximalCriteriaForPrime.lean, line 64. The attribute's comment: “(1)”.

An ideal maximal among the ideals which do not contain a nonzerodivisor is prime.

theorem Ideal.isPrime_of_maximal_disjoint_nonZeroDivisors {R : Type*} [CommSemiring R]
    (I : Ideal R) (hI : Maximal (fun J : Ideal R ↦ Disjoint (J : Set R) (R⁰ : Set R)) I) :
    I.IsPrime

isDomain_of_forall_nonzero_prime_containsNonZeroDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/MaximalCriteriaForPrime.lean, line 74. The attribute's comment: “(2)”.

(Characterization of a domain.) If R is nonzero and every nonzero prime ideal of R contains a nonzerodivisor, then R is a domain.

theorem isDomain_of_forall_nonzero_prime_containsNonZeroDivisor [Nontrivial R]
    (h : ∀ P : Ideal R, P.IsPrime → P ≠ ⊥ →
      ¬ Disjoint (P : Set R) (nonZeroDivisors R : Set R)) :
    IsDomain R
Sources
Leanideal_eq_mul_colon_of_isPrincipal · isOkaFamilyUniversal_meetsSubmonoidFamily · Ideal.isOka_fg · Ideal.isOka_isPrincipal · Ideal.isPrime_of_maximally_disjoint · Ideal.IsOka.isPrime_of_maximal_not · IsNoetherianRing.of_prime · isNoetherianRing_iff_ideal_fg

Section10.29 Images of ring maps of finite presentation#

Section 10.29 of the Stacks Project, Tag 00F5. 10 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 16 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00F6, a lemma

Tag 00F6 in the Stacks Project.

Declarations registered for the tag:

Tag 00F7, a lemma

Tag 00F7 in the Stacks Project.

PrimeSpectrum.isCompact_preimage_comap_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/Chevalley.lean, line 76. The attribute's comment: “(1)”.

Stacks 00F7 (first assertion): for a ring map φ : R → S, the induced continuous map Spec(S) → Spec(R) is quasi-compact, i.e. the preimage of every quasi-compact open of Spec(R) is quasi-compact in Spec(S).

theorem PrimeSpectrum.isCompact_preimage_comap_of_isOpen
    {R S : Type*} [CommSemiring R] [CommSemiring S] (φ : R →+* S)
    (V : Set (PrimeSpectrum R)) (hV : IsOpen V) (hVc : IsCompact V) :
    IsCompact ((PrimeSpectrum.comap φ) ⁻¹' V)

PrimeSpectrum.isConstructible_preimage_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/Chevalley.lean, line 91. The attribute's comment: “(2)”.

Stacks 00F7 (second assertion): for a ring map φ : R → S and any constructible subset E ⊆ Spec(R), the preimage (comap φ)⁻¹(E) is constructible in Spec(S).

theorem PrimeSpectrum.isConstructible_preimage_comap
    {R S : Type*} [CommSemiring R] [CommSemiring S] (φ : R →+* S)
    (E : Set (PrimeSpectrum R)) (hE : Topology.IsConstructible E) :
    Topology.IsConstructible ((PrimeSpectrum.comap φ) ⁻¹' E)
Tag 0G1P, a lemma

Tag 0G1P in the Stacks Project.

Declarations registered for the tag:

Tag 00F8, a lemma

Tag 00F8 in the Stacks Project.

PrimeSpectrum.exists_range_eq_of_isConstructible_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/Image.lean, line 31.

Stacks 00F8. Every constructible subset of Spec R is the image of Spec S for a finitely presented R-algebra S.

theorem exists_range_eq_of_isConstructible_finitePresentation {R : Type u} [CommRing R]
    {s : Set (PrimeSpectrum R)} (hs : IsConstructible s) :
    ∃ (S : Type u) (_ : CommRing S) (f : R →+* S),
      f.FinitePresentation ∧ Set.range (comap f) = s
Tag 00F9, a lemma

Tag 00F9 in the Stacks Project.

Declarations registered for the tag:

Tag 00FA, a lemma

Tag 00FA in the Stacks Project.

Declarations registered for the tag:

Tag 00FB, a lemma

Tag 00FB in the Stacks Project.

Polynomial.image_comap_C_basicOpen_eq_biUnion_basicOpen_coeffs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Polynomial.lean, line 103. The attribute's comment: “Second part”.

Stacks 00FB, second part. Let R be a ring and f ∈ R[x]. The image of the standard open D(f) ⊆ Spec(R[x]) under the map Spec(R[x]) → Spec(R) is the union of the standard opens D(a), a running over the coefficients of f; in particular it is a quasi-compact open.

public theorem image_comap_C_basicOpen_eq_biUnion_basicOpen_coeffs {R : Type*} [CommRing R]
    (f : R[X]) :
    PrimeSpectrum.comap (C : R →+* R[X]) '' (basicOpen f : Set (PrimeSpectrum R[X])) =
      ⋃ a ∈ f.coeffs, (basicOpen a : Set (PrimeSpectrum R))
Tag 00FC, a lemma

Tag 00FC in the Stacks Project.

PrimeSpectrum.isNilpotent_baseChange_mulLeft_iff_mem_zeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/Chevalley.lean, line 190.

For A free of rank n over R and f : A, the set of primes p at which multiplication by f becomes nilpotent over the residue field is the zero locus of the first n coefficients of the characteristic polynomial of multiplication by f.

theorem PrimeSpectrum.isNilpotent_baseChange_mulLeft_iff_mem_zeroLocus
    {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
    (n : ℕ) (e : A ≃ₗ[R] (Fin n → R))
    (f : A) (p : PrimeSpectrum R) :
    IsNilpotent
        (LinearMap.baseChange p.asIdeal.ResidueField
          (LinearMap.mulLeft R f)) ↔
      p ∈ PrimeSpectrum.zeroLocus
        ((fun i : Fin n =>
            (charPolyOfEquiv e (LinearMap.mulLeft R f)).coeff i) '' Set.univ)
Tag 00FD, a lemma

Tag 00FD in the Stacks Project.

image_comap_C_basicOpen_inter_zeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/Chevalley.lean, line 216.

Stacks Tag 00FD. Let R be a ring and f, g ∈ R[x] polynomials whose leading coefficient of g is a unit of R. Then the image of D(f) ∩ V(g) under the structure map Spec(R[x]) → Spec(R) is a finite union of standard opens: there exist r_1, …, r_n ∈ R with image = ⋃ᵢ D(rᵢ).

Since the leading coefficient of g is a unit, g is associate to the monic polynomial g' = (leadingCoeff g)⁻¹ • g, so V(g) = V(g'). For monic g', R[x]/(g') is finite free over R, and Mathlib's Polynomial.exists_image_comap_of_monic produces a finite set t ⊆ R with image = (V(t))ᶜ = ⋃_{r ∈ t} D(r), which we reindex by Fin n.

theorem image_comap_C_basicOpen_inter_zeroLocus
    {R : Type*} [CommRing R] (f g : R[X]) (hg : IsUnit g.leadingCoeff) :
    ∃ (n : ℕ) (r : Fin n → R),
      comap (C : R →+* R[X]) ''
          ((basicOpen f : Set (PrimeSpectrum R[X])) ∩ zeroLocus {g}) =
        ⋃ i, (basicOpen (r i) : Set (PrimeSpectrum R))
Tag 00FE, a theorem

Tag 00FE in the Stacks Project.

Declarations registered for the tag:

Sources
LeanQuasiSeparatedSpace.isRetrocompact_iff_isCompact · PrimeSpectrum.isCompact_isOpen_iff · PrimeSpectrum.isCompact_isOpen_iff_ideal · PrimeSpectrum.isCompact_preimage_comap_of_isOpen · PrimeSpectrum.isConstructible_preimage_comap · PrimeSpectrum.exists_constructibleSetData_iff · PrimeSpectrum.BasicConstructibleSetData · PrimeSpectrum.BasicConstructibleSetData.toSet

Section10.30 More on images#

Section 10.30 of the Stacks Project, Tag 00FF. 6 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00FG, a lemma

Tag 00FG in the Stacks Project.

GenericFinitePresentation.generic_finite_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/GenericFinitePresentation/AwayMapMul.lean, line 662.

Generic finite presentation. An inclusion of domains of finite type admits nonzero f ∈ R and g ∈ S such that R[1/f] → S[1/(fg)] is of finite presentation. The domain hypothesis on R follows from injectivity.

theorem GenericFinitePresentation.generic_finite_presentation
    {R S : Type*} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S]
    [Algebra.FiniteType R S] (hinj : Function.Injective (algebraMap R S)) :
    ∃ (f : R) (g : S), f ≠ 0 ∧ g ≠ 0 ∧ (awayMapMul f g).FinitePresentation
Tag 00FH, a lemma

Tag 00FH in the Stacks Project.

image_constructible_contains_open_dense_in_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/GenericFinitePresentation/ConstructibleImage.lean, line 650.

Stacks 00FH (Lemma 10.30.2). Let φ : R →+* S be a ring map of finite type, let E ⊆ Spec S be constructible, and let ξ ∈ Spec R lie in the image f(E) of E under f = PrimeSpectrum.comap φ. Then closure {ξ} ∩ f(E) contains a subset D that is open and dense in the subspace closure {ξ}.

theorem image_constructible_contains_open_dense_in_closure
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (hφ : φ.FiniteType)
    (E : Set (PrimeSpectrum S)) (hE : Topology.IsConstructible E)
    (ξ : PrimeSpectrum R)
    (hξ : ξ ∈ PrimeSpectrum.comap φ '' E) :
    ∃ D : Set (closure {ξ} : Set (PrimeSpectrum R)),
      IsOpen D ∧ Dense D ∧
      (Subtype.val '' D) ⊆ closure {ξ} ∩ (PrimeSpectrum.comap φ '' E)
Tag 00FI, a lemma

Tag 00FI in the Stacks Project.

main_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Surjective.lean, line 112.

Main equivalence: conditions (1), (2), (3), (4) are equivalent.

theorem main_equivalence
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) :
    (SpecSurjective φ ↔ RadicalContractionEq φ) ∧
    (RadicalContractionEq φ ↔ RadicalIdealContractionEq φ) ∧
    (RadicalIdealContractionEq φ ↔ PrimeContractionEq φ) ∧
    (PrimeContractionEq φ ↔ SpecSurjective φ)
Tag 00FJ, a lemma

Tag 00FJ in the Stacks Project.

domain_image_dense_set_points_generic_point_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Surjective.lean, line 306. References: EGA 0 (2.1.5), “special case”; EGA I (1.2.7), “special case”.

Let R be a domain and φ : R →+* S a ring map. Then the following are equivalent: 1. φ is injective. 2. The range of the induced map PrimeSpectrum.comap φ is dense in PrimeSpectrum R. 3. There exists a prime q of S whose preimage under φ is the zero ideal of R.

theorem domain_image_dense_set_points_generic_point_tfae :
    List.TFAE
      [ Function.Injective φ
      , Dense (Set.range (PrimeSpectrum.comap φ))
      , ∃ q : PrimeSpectrum S, (PrimeSpectrum.comap φ q).asIdeal = ⊥ ]
Tag 0CAN, a lemma

Tag 0CAN in the Stacks Project.

Declarations registered for the tag:

Tag 0H7L, a lemma

Tag 0H7L in the Stacks Project.

contraction_ne_bot_of_algebraic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/ContractionNeBot.lean, line 46. The attribute's comment: “first sentence”.

Algebraic core (Stacks 0H7L). Let A ⊆ B be an inclusion of integral domains, modeled by an injective algebraMap A B. Let K = Frac(A) and L = Frac(B) be their fields of fractions, with the induced field embedding K ↪ L (encoded by the algebra structure Algebra K L and the scalar towers A → K → L, A → B → L). Assume the extension K ⊆ L is algebraic. If J is a nonzero ideal of B, then its contraction A ∩ J = comap (algebraMap A B) J is a nonzero ideal of A.

theorem contraction_ne_bot_of_algebraic
    (A B K L : Type*)
    [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [Algebra A B] (hinj : Function.Injective (algebraMap A B))
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra B L] [IsFractionRing B L]
    [Algebra A L] [Algebra K L]
    [IsScalarTower A B L] [IsScalarTower A K L]
    [Algebra.IsAlgebraic K L]
    (J : Ideal B) (hJ : J ≠ ⊥) :
    Ideal.comap (algebraMap A B) J ≠ ⊥

PrimeSpectrum.not_dense_image_comap_of_isAlgebraic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/ContractionNeBot.lean, line 67. The attribute's comment: “second sentence”.

Let A → B be an algebraic ring map from a reduced ring into a domain. Then the image in Spec A of a proper closed subset of Spec B is not dense.

theorem PrimeSpectrum.not_dense_image_comap_of_isAlgebraic {A B : Type*} [CommRing A]
    [CommRing B] [IsReduced A] [IsDomain B] [Algebra A B] [Algebra.IsAlgebraic A B]
    {Z : Set (PrimeSpectrum B)} (hZ : IsClosed Z) (hZ' : Z ≠ Set.univ) :
    ¬ Dense (PrimeSpectrum.comap (algebraMap A B) '' Z)
Sources
LeanGenericFinitePresentation.generic_finite_presentation · image_constructible_contains_open_dense_in_closure · main_equivalence · domain_image_dense_set_points_generic_point_tfae · Ideal.exists_minimalPrimes_comap_eq · contraction_ne_bot_of_algebraic · PrimeSpectrum.not_dense_image_comap_of_isAlgebraic

Section10.31 Noetherian rings#

Section 10.31 of the Stacks Project, Tag 00FM. 10 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00FN, a lemma

Tag 00FN in the Stacks Project.

Declarations registered for the tag:

Tag 0306, a lemma

Tag 0306 in the Stacks Project.

mvPowerSeries_fin_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPowerSeries/Noetherian.lean, line 165.

The formal power series ring in n variables over a Noetherian commutative ring is Noetherian.

theorem mvPowerSeries_fin_isNoetherianRing
    (R : Type*) [CommRing R] [IsNoetherianRing R] (n : ℕ) :
    IsNoetherianRing (MvPowerSeries (Fin n) R)
Tag 00FO, a lemma

Tag 00FO in the Stacks Project.

Declarations registered for the tag:

  • Algebra.FiniteType.isNoetherianRing registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 138 (StacksFrontier): “over any Noetherian base; fields and ℤ are Noetherian”. References: EGA 0 (22.3.1), “Noetherianity of A”; EGA 0 (23.2.5), “Noetherian clause”; EGA II (2.1.5), “sufficiency”; EGA IV (1.4.1), “more general”; EGA IV (1.5.3), “affine case”; SGA 3 VIB (10.10), “more general”; SGA 5 V (5.1.4), “special case”.
Tag 00FP, a lemma

Tag 00FP in the Stacks Project.

Declarations registered for the tag:

Tag 00FQ, a lemma

Tag 00FQ in the Stacks Project.

Declarations registered for the tag:

Tag 00FR, a lemma

Tag 00FR in the Stacks Project.

Declarations registered for the tag:

Tag 0CY6, a lemma

Tag 0CY6 in the Stacks Project.

noetherian_base_change_finite_type, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/Spec.lean, line 100. References: EGA I (6.3.8), “affine case”; EGA IV (1.5.5), “affine case”; EGA I (10.13.5), “(ii)”; EGA I (6.6.7), “affine case”; EGA II (2.1.5), “sufficiency”; EGA IV (1.3.5), “affine schemes”; EGA IV (6.7.1.1), “special case”; SGA 1 III (1.4), “partial”; SGA 5 V (5.1.4), “special case”; SGA 5 V (5.1.5), “special case”; SGA 6 X (7.15), “special case”; SGA 6 X (7.17), “special case”.

If R → R' is of finite type and S is a Noetherian R-algebra, then the base change R' ⊗[R] S is a Noetherian ring.

The proof transports the result along the commutativity isomorphism S ⊗[R] R' ≃ R' ⊗[R] S, after observing that base change preserves finite type and applying the Hilbert basis theorem.

theorem noetherian_base_change_finite_type
    (R R' S : Type*) [CommRing R] [CommRing R'] [CommRing S]
    [Algebra R R'] [Algebra R S]
    [Algebra.FiniteType R R'] [IsNoetherianRing S] :
    IsNoetherianRing (TensorProduct R R' S)
Tag 045I, a lemma

Tag 045I in the Stacks Project.

tensorProduct_isNoetherianRing_of_finitelyGenerated_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/TensorProduct.lean, line 73. References: EGA IV (4.7.3), “(i), special case”; EGA IV (6.7.1), “Affine X, special case”; EGA IV (6.7.1.1), “more general”; SGA 1 III (1.4), “special case”; SGA 5 V (5.1.5), “special case”.

Stacks Tag 045I. Let k be a field and R a Noetherian commutative k-algebra. If K/k is a finitely generated field extension (finitely generated as a field, expressed by (⊤ : IntermediateField k K).FG), then the k-algebra K ⊗[k] R is Noetherian.

theorem tensorProduct_isNoetherianRing_of_finitelyGenerated_fieldExtension
    (k : Type*) [Field k]
    (R : Type*) [CommRing R] [Algebra k R] [IsNoetherianRing R]
    (K : Type*) [Field K] [Algebra k K]
    (hK : (⊤ : IntermediateField k K).FG) :
    IsNoetherianRing (K ⊗[k] R)
Tag 0BX1, a lemma

Tag 0BX1 in the Stacks Project.

exists_injective_localizationAwayToAtPrime_of_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/AwayToAtPrime.lean, line 93. The attribute's comment: “(1)”.

Case (1): R an integral domain. There exists f ∉ p such that the canonical map R_f → R_p is injective. (One may take f = 1.)

theorem exists_injective_localizationAwayToAtPrime_of_isDomain
    {R : Type*} [CommRing R] [IsDomain R] (p : Ideal R) [p.IsPrime] :
    ∃ f : R, ∃ hf : f ∉ p, Function.Injective (localizationAwayToAtPrime f p hf)

exists_injective_localizationAwayToAtPrime_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/AwayToAtPrime.lean, line 103. The attribute's comment: “(2)”.

Case (2): R Noetherian. There exists f ∉ p such that the canonical map R_f → R_p is injective.

theorem exists_injective_localizationAwayToAtPrime_of_isNoetherianRing
    {R : Type*} [CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] :
    ∃ f : R, ∃ hf : f ∉ p, Function.Injective (localizationAwayToAtPrime f p hf)

exists_injective_localizationAwayToAtPrime_of_isReduced_finite_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/AwayToAtPrime.lean, line 135. The attribute's comment: “(3)”.

Case (3): R reduced with finitely many minimal primes not contained in p. There exists f ∉ p such that the canonical map R_f → R_p is injective.

The hypothesis is weaker than the (minimalPrimes R).Finite of 0BX1 (3), which implies it by Set.Finite.subset _ (Set.sep_subset _ _).

theorem exists_injective_localizationAwayToAtPrime_of_isReduced_finite_minimalPrimes
    {R : Type*} [CommRing R] [IsReduced R] (p : Ideal R) [p.IsPrime]
    (hfin : {q ∈ minimalPrimes R | ¬ q ≤ p}.Finite) :
    ∃ f : R, ∃ hf : f ∉ p, Function.Injective (localizationAwayToAtPrime f p hf)
Tag 06RN, a lemma

Tag 06RN in the Stacks Project.

surjective_endomorphism_noetherian_isomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/Endomorphism.lean, line 68.

The bijective endomorphism above is genuinely a ring isomorphism: there is a RingEquiv e : R ≃+* R that agrees with φ on every element.

theorem surjective_endomorphism_noetherian_isomorphism
    (R : Type*) [CommRing R] [IsNoetherianRing R] (φ : R →+* R)
    (hφ : Function.Surjective φ) : ∃ e : R ≃+* R, ∀ x, e x = φ x
Sources
LeanAlgebra.FiniteType.isNoetherianRing · IsLocalization.isNoetherianRing · mvPowerSeries_fin_isNoetherianRing · Module.finitePresentation_of_finite · Submodule.FG.of_le · Algebra.FinitePresentation.of_finiteType · PrimeSpectrum.instNoetherianSpace · minimalPrimes.finite_of_isNoetherianRing

Section10.32 Locally nilpotent ideals#

Section 10.32 of the Stacks Project, Tag 0AMF. 7 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00IL, a definition

Tag 00IL in the Stacks Project.

Ideal.LocallyNilpotent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Ideal.lean, line 91. The attribute's comment: “locally nilpotent”. References: SGA 6 VI (6.1).

An ideal I ⊂ R is locally nilpotent if every element of I is nilpotent, i.e. for every x ∈ I there exists n ∈ ℕ with x ^ n = 0.

def LocallyNilpotent (I : Ideal R) : Prop

Ideal.Nilpotent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Ideal.lean, line 97. The attribute's comment: “nilpotent”.

An ideal I ⊂ R is nilpotent if there exists n ∈ ℕ with I ^ n = 0, where 0 = ⊥ is the zero ideal.

def Nilpotent (I : Ideal R) : Prop
Tag 0EGG, an example

Tag 0EGG in the Stacks Project.

Stacks.LocallyNilpotentNotNilpotent.idealJ_le_nilradical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Ideal.lean, line 188.

J ≤ nilradical S, i.e. every element of J is nilpotent.

theorem idealJ_le_nilradical : idealJ k ≤ nilradical (S_ring k)

Stacks.LocallyNilpotentNotNilpotent.not_isNilpotent_idealJ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Ideal.lean, line 215.

J is not nilpotent: there is no m with J ^ m = 0.

theorem not_isNilpotent_idealJ : ¬ IsNilpotent (idealJ k)
Tag 0544, a lemma

Tag 0544 in the Stacks Project.

Ideal.IsLocallyNilpotent0544.map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Ideal.lean, line 141. References: EGA III (5.4.6), “more general”.

If R → R' is a ring map and I ⊂ R is a locally nilpotent ideal, then the extended ideal IR' = I.map f is locally nilpotent in R'.

theorem Ideal.IsLocallyNilpotent0544.map
    {R R' : Type*} [CommRing R] [CommRing R']
    (f : R →+* R') (I : Ideal R)
    (hI : Ideal.IsLocallyNilpotent0544 I) :
    Ideal.IsLocallyNilpotent0544 (I.map f)
Tag 0AMG, a lemma

Tag 0AMG in the Stacks Project.

Stacks.NilpotentIdeal.PowerMap.isUnit_quotient_mk_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Lifting.lean, line 145. References: EGA 0 (19.10.3), “more general”; EGA 0 (7.1.12), “special case”.

Units are detected modulo a locally nilpotent ideal.

theorem isUnit_quotient_mk_iff (hI : ∀ x ∈ I, IsNilpotent x) {x : R} :
    IsUnit x ↔ IsUnit ((Ideal.Quotient.mk I) x)
Tag 00IM, a lemma

Tag 00IM in the Stacks Project.

Declarations registered for the tag:

Tag 05BU, a lemma

Tag 05BU in the Stacks Project.

exists_isIdempotentElem_add_sq_sub_mul_sum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Idempotents/IntegerPolynomial.lean, line 72.

Let A be a possibly noncommutative ring and let e ∈ A be such that x = e ^ 2 - e is nilpotent. Then there is an idempotent of the form e + x * (∑ a i j • (e ^ i * x ^ j)) with integer coefficients a i j.

theorem exists_isIdempotentElem_add_sq_sub_mul_sum {e : A} (he : IsNilpotent (e ^ 2 - e)) :
    ∃ (N : ℕ) (a : ℕ → ℕ → ℤ), IsIdempotentElem (e + (e ^ 2 - e) *
      ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N, a i j • (e ^ i * (e ^ 2 - e) ^ j))
Tag 0CAP, a lemma

Tag 0CAP in the Stacks Project.

Stacks.NilpotentIdeal.PowerMap.powMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Lifting.lean, line 229. The attribute's comment: “(1)”.

If I is locally nilpotent and n ≥ 1 is invertible in R/I, then the nth power map 1 + x ↦ (1 + x)^n on 1 + I is a bijection.

theorem powMap_bijective
    (hI : ∀ x ∈ I, IsNilpotent x) {n : ℕ} (hn : 1 ≤ n)
    (hnu : IsUnit ((n : R ⧸ I))) :
    Function.Bijective (powMap I n)

Stacks.NilpotentIdeal.PowerMap.isUnit_pow_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Lifting.lean, line 238. The attribute's comment: “(2)”.

If I is locally nilpotent and n ≥ 1 is invertible in R/I, then a unit u ∈ Rˣ is an nth power in R if and only if its image in R/I is an nth power (as a unit) in R/I.

theorem isUnit_pow_iff
    (hI : ∀ x ∈ I, IsNilpotent x) {n : ℕ} (hn : 1 ≤ n)
    (hnu : IsUnit ((n : R ⧸ I))) (u : Rˣ) :
    (∃ v : Rˣ, u = v ^ n) ↔
      (∃ w : (R ⧸ I)ˣ, (Ideal.Quotient.mk I (u : R) : R ⧸ I) = (w : R ⧸ I) ^ n)
Sources
LeanIdeal.LocallyNilpotent · Ideal.Nilpotent · Stacks.LocallyNilpotentNotNilpotent.idealJ_le_nilradical · Stacks.LocallyNilpotentNotNilpotent.not_isNilpotent_idealJ · Ideal.IsLocallyNilpotent0544.map · Stacks.NilpotentIdeal.PowerMap.isUnit_quotient_mk_iff · Ideal.exists_pow_le_of_le_radical_of_fg · Ideal.fg_of_isNoetherianRing

Section10.33 Curiosity#

Section 10.33 of the Stacks Project, Tag 02JG. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02JH, a lemma

Tag 02JH in the Stacks Project.

localization_isClosed_range_comap_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/ClosedImage.lean, line 89.

Let S be a multiplicative subset of a ring R. If the image of Spec(S⁻¹R) → Spec(R) is closed, then S⁻¹R is isomorphic to a quotient R ⧸ I for some ideal I ⊆ R.

theorem localization_isClosed_range_comap_isClosed
    (R : Type*) [CommRing R] (S : Submonoid R)
    (hclosed :
      IsClosed (Set.range (PrimeSpectrum.comap (algebraMap R (Localization S))))) :
    ∃ I : Ideal R, Nonempty (Localization S ≃+* (R ⧸ I))
Tag 02JI, a lemma

Tag 02JI in the Stacks Project.

IsLocalization.exists_ringEquiv_prod_of_isClosed_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/ClosedImage.lean, line 286.

Let S ⊆ R be a multiplicative subset such that the image of Spec(S⁻¹R) → Spec R is closed. If R is Noetherian, or Spec R is a Noetherian topological space, or S is finitely generated as a monoid, then R ≅ S⁻¹R × R' for some ring R'.

theorem exists_ringEquiv_prod_of_isClosed_range
    (hclosed : IsClosed (Set.range (comap (algebraMap R A))))
    (h : IsNoetherianRing R ∨ NoetherianSpace (PrimeSpectrum R) ∨ S.FG) :
    ∃ (R' : Type u) (_ : CommRing R'), Nonempty (R ≃+* A × R')
Sources
Leanlocalization_isClosed_range_comap_isClosed · IsLocalization.exists_ringEquiv_prod_of_isClosed_range

Section10.34 Hilbert Nullstellensatz#

Section 10.34 of the Stacks Project, Tag 00FS. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00FV, a theorem

Tag 00FV in the Stacks Project.

Stacks.HilbertNullstellensatz.module_finite_quotient_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/HilbertNullstellensatz.lean, line 54. The attribute's comment: “part (1), for an arbitrary finite type algebra over the field”. References: EGA IV (10.4.5), “a⇒b′ over a field”.

Hilbert Nullstellensatz, part (1), for a finite type algebra: if A is a k-algebra of finite type over a field k and 𝔪 ⊆ A is a maximal ideal, then the residue field κ(𝔪) = A ⧸ 𝔪 is a finite extension of k.

The quotient A ⧸ 𝔪 is a field by Ideal.Quotient.field, and it is of finite type over k because A is, so Zariski's lemma over the Jacobson ring k applies.

public theorem module_finite_quotient_of_finiteType (k A : Type*) [Field k] [CommRing A]
    [Algebra k A] [Algebra.FiniteType k A] (𝔪 : Ideal A) [𝔪.IsMaximal] :
    Module.Finite k (A ⧸ 𝔪)

Stacks.HilbertNullstellensatz.eq_sInf_isMaximal_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/HilbertNullstellensatz.lean, line 68. The attribute's comment: “part (2), for an arbitrary finite type algebra over the field”. References: EGA IV (10.4.6), “partial”.

Hilbert Nullstellensatz, part (2), for a finite type algebra: a radical ideal I of a k-algebra A of finite type over a field k is the infimum of the maximal ideals of A containing I.

A finite type algebra over a field is a Jacobson ring, and in a Jacobson ring a radical ideal equals its Jacobson radical, which is by definition that infimum.

public theorem eq_sInf_isMaximal_of_finiteType (k A : Type*) [Field k] [CommRing A] [Algebra k A]
    [Algebra.FiniteType k A] (I : Ideal A) (hI : I.IsRadical) :
    I = sInf {J : Ideal A | I ≤ J ∧ J.IsMaximal}

Stacks.HilbertNullstellensatz.module_finite_quotient_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/HilbertNullstellensatz.lean, line 88. The attribute's comment: “part (1)”.

Hilbert Nullstellensatz, part (1): for a field k, finitely many variables ι and a maximal ideal 𝔪 of the polynomial ring k[x_i : i ∈ ι], the residue field κ(𝔪) = k[x_i : i ∈ ι] ⧸ 𝔪 is a finite extension of k.

public theorem module_finite_quotient_mvPolynomial (k : Type*) [Field k] (ι : Type*) [Finite ι]
    (𝔪 : Ideal (MvPolynomial ι k)) [𝔪.IsMaximal] :
    Module.Finite k (MvPolynomial ι k ⧸ 𝔪)

Stacks.HilbertNullstellensatz.eq_sInf_isMaximal_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/HilbertNullstellensatz.lean, line 97. The attribute's comment: “part (2)”.

Hilbert Nullstellensatz, part (2): for a field k and finitely many variables ι, a radical ideal I of the polynomial ring k[x_i : i ∈ ι] is the infimum of the maximal ideals containing I.

public theorem eq_sInf_isMaximal_mvPolynomial (k : Type*) [Field k] (ι : Type*) [Finite ι]
    (I : Ideal (MvPolynomial ι k)) (hI : I.IsRadical) :
    I = sInf {J : Ideal (MvPolynomial ι k) | I ≤ J ∧ J.IsMaximal}

Stacks.HilbertNullstellensatz.coe_eq_iInter_isMaximal_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/HilbertNullstellensatz.lean, line 106. The attribute's comment: “part (2), as an intersection of the underlying sets”.

Hilbert Nullstellensatz, part (2), as an equality of sets: a radical ideal I of the polynomial ring k[x_i : i ∈ ι] over a field k in finitely many variables is, as a subset of the polynomial ring, the intersection of the maximal ideals containing I.

public theorem coe_eq_iInter_isMaximal_mvPolynomial (k : Type*) [Field k] (ι : Type*) [Finite ι]
    (I : Ideal (MvPolynomial ι k)) (hI : I.IsRadical) :
    (I : Set (MvPolynomial ι k)) =
      ⋂ J ∈ {J : Ideal (MvPolynomial ι k) | I ≤ J ∧ J.IsMaximal},
        (J : Set (MvPolynomial ι k))

Declarations registered for the tag:

Tag 00FY, a lemma

Tag 00FY in the Stacks Project.

exists_isField_localizationAway_and_finite_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Nullstellensatz.lean, line 108.

Let R ⊂ K with K a field and K of finite type over R as an R-algebra. Then there exists f ∈ R such that the localization R_f is a field, and K is a finite extension of R_f.

theorem exists_isField_localizationAway_and_finite_of_finiteType (R K : Type*)
    [CommRing R] [Field K]
    [Algebra R K] (hRK : Function.Injective (algebraMap R K))
    [Algebra.FiniteType R K] :
    ∃ f : R, IsField (Localization.Away f) ∧
      ∃ (_ : Algebra (Localization.Away f) K)
        (_ : IsScalarTower R (Localization.Away f) K),
        Module.Finite (Localization.Away f) K
Sources
LeanStacks.HilbertNullstellensatz.module_finite_quotient_of_finiteType · Stacks.HilbertNullstellensatz.eq_sInf_isMaximal_of_finiteType · Stacks.HilbertNullstellensatz.module_finite_quotient_mvPolynomial · Stacks.HilbertNullstellensatz.eq_sInf_isMaximal_mvPolynomial · Stacks.HilbertNullstellensatz.coe_eq_iInter_isMaximal_mvPolynomial · finite_of_finite_type_of_isJacobsonRing · MvPolynomial.isJacobsonRing · exists_isField_localizationAway_and_finite_of_finiteType

Section10.35 Jacobson rings#

Section 10.35 of the Stacks Project, Tag 00FZ. 22 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00G0, a definition

Tag 00G0 in the Stacks Project.

Declarations registered for the tag:

Tag 00G1, a lemma

Tag 00G1 in the Stacks Project.

Declarations registered for the tag:

Tag 00G2, a lemma

Tag 00G2 in the Stacks Project.

Declarations registered for the tag:

Tag 00G3, a lemma

Tag 00G3 in the Stacks Project.

Declarations registered for the tag:

Tag 034J, a lemma

Tag 034J in the Stacks Project.

exists_prime_vCapD_singleton_isField_of_not_isJacobsonRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Constructions.lean, line 488. The attribute's comment: “(1)”. References: EGA IV (10.4.5), “b) => a)”.

(Non-Jacobson direction, Stacks 034J (1).) If R is not a Jacobson ring, then there exist a prime ideal p and an element f such that p is not maximal, f ∉ p, V(p) ∩ D(f) = {p}, and (R/p)_f is a field.

theorem exists_prime_vCapD_singleton_isField_of_not_isJacobsonRing {R : Type*} [CommRing R]
    (hR : ¬ IsJacobsonRing R) :
    ∃ (p : PrimeSpectrum R) (f : R),
      (¬ p.asIdeal.IsMaximal) ∧
      (f ∉ p.asIdeal) ∧
      (vCapD p f = {p}) ∧
      IsField (Localization.Away (Ideal.Quotient.mk p.asIdeal f))

vCapD_infinite_of_isJacobsonRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Constructions.lean, line 596. The attribute's comment: “(2)”. References: EGA IV (10.4.5), “a) => b)”.

(Jacobson direction, Stacks 034J (2).) If R is a Jacobson ring, then for every prime ideal p that is not maximal and every element f ∉ p, the set V(p) ∩ D(f) is infinite.

theorem vCapD_infinite_of_isJacobsonRing {R : Type*} [CommRing R]
    (hR : IsJacobsonRing R) (p : PrimeSpectrum R) (f : R)
    (hp : ¬ p.asIdeal.IsMaximal) (hf : f ∉ p.asIdeal) :
    (vCapD p f).Infinite
Tag 00G4, a lemma

Tag 00G4 in the Stacks Project.

isJacobsonRing_of_domain_noetherian_dim_le_one_infinite_maximalSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 180. References: EGA IV (10.4.3), “principal ideal ring”; EGA IV (10.5.2), “special case”; EGA IV (10.7.1), “partial”.

A Noetherian domain in which every nonzero prime ideal is maximal and which has infinitely many maximal ideals is a Jacobson ring.

theorem isJacobsonRing_of_domain_noetherian_dim_le_one_infinite_maximalSpectrum
    (R : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R]
    (hdim : ∀ I : Ideal R, I.IsPrime → I ≠ ⊥ → I.IsMaximal)
    (hinf : Infinite (MaximalSpectrum R)) :
    IsJacobsonRing R

int_isJacobsonRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 218. References: EGA IV (10.4.3), “example ℤ”.

The ring ℤ is a Jacobson ring.

theorem int_isJacobsonRing : IsJacobsonRing ℤ
Tag 02CC, an example

Tag 02CC in the Stacks Project.

prod_field_isJacobsonRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 508.

Let A be an infinite type and (k α) a family of fields. Then the product ring ∀ α, k α is a Jacobson ring.

theorem prod_field_isJacobsonRing
    (A : Type*) [Infinite A] (k : A → Type*) [∀ α, Field (k α)] :
    IsJacobsonRing (∀ α, k α)
Tag 00G5, an example

Tag 00G5 in the Stacks Project.

isField_of_isDomain_finite_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 236. References: EGA IV (10.7.1), “partial”.

A Jacobson domain with finitely many maximal ideals is a field.

theorem isField_of_isDomain_finite_maximalIdeal
    {R : Type*} [CommRing R] [IsDomain R] [IsJacobsonRing R]
    (hfin : {m : Ideal R | m.IsMaximal}.Finite) :
    IsField R
Tag 00GA, a lemma

Tag 00GA in the Stacks Project.

isMaximal_of_isAlgebraic_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Constructions.lean, line 139.

Stacks tag 00GA: if q ⊆ S is a prime lying over a maximal ideal m ⊆ R and the residue field extension κ(q)/κ(m) is algebraic, then q is maximal.

theorem isMaximal_of_isAlgebraic_residueField
    {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    {m : Ideal R} [m.IsMaximal] {q : Ideal S} [q.IsPrime]
    (hlies : m = q.comap f)
    [Algebra m.ResidueField q.ResidueField]
    (hcompat : (algebraMap m.ResidueField q.ResidueField) =
      Ideal.ResidueField.map m q f hlies)
    [Algebra.IsAlgebraic m.ResidueField q.ResidueField] :
    q.IsMaximal
Tag 00FT, a lemma

Tag 00FT in the Stacks Project.

exists_monic_aeval_not_bijective_of_rank_lt_card, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Nullstellensatz.lean, line 155.

Let k be a field and V a nonzero k-vector space with dim_k V < |k| (as cardinals). Then for every k-linear operator T : V → V there is a monic polynomial P of degree ≥ 1 such that P(T) is not bijective (i.e. not invertible).

theorem exists_monic_aeval_not_bijective_of_rank_lt_card
    {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V]
    [Nontrivial V]
    (h : Cardinal.lift.{u} (Module.rank k V) < Cardinal.lift.{v} (Cardinal.mk k))
    (T : V →ₗ[k] V) :
    ∃ P : k[X], P.Monic ∧ 1 ≤ P.natDegree ∧ ¬ Function.Bijective (aeval T P)
Tag 00FU, a theorem

Tag 00FU in the Stacks Project.

Algebra.isAlgebraic_quotient_of_adjoin_eq_top_of_card_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Nullstellensatz.lean, line 471. The attribute's comment: “(1)”.

The residue fields of an algebra generated by fewer than #k elements are algebraic over the field k.

theorem Algebra.isAlgebraic_quotient_of_adjoin_eq_top_of_card_lt {k : Type u} {S : Type v}
    {I : Type w} [Field k] [CommRing S] [Algebra k S] (x : I → S)
    (hgen : Algebra.adjoin k (Set.range x) = ⊤) (hI : lift.{u} #I < lift.{w} #k)
    (m : Ideal S) [m.IsMaximal] : Algebra.IsAlgebraic k (S ⧸ m)

isJacobsonRing_of_adjoin_eq_top_of_card_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Nullstellensatz.lean, line 483. The attribute's comment: “(2)”.

An algebra generated by fewer than #k elements over a field k is a Jacobson ring.

theorem isJacobsonRing_of_adjoin_eq_top_of_card_lt {k : Type u} {S : Type v} {I : Type w}
    [Field k] [CommRing S] [Algebra k S] (x : I → S)
    (hgen : Algebra.adjoin k (Set.range x) = ⊤) (hI : lift.{u} #I < lift.{w} #k) :
    IsJacobsonRing S
Tag 046V, a lemma

Tag 046V in the Stacks Project.

Algebra.isAlgebraic_tensorProduct_quotient_of_card_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Nullstellensatz.lean, line 404. The attribute's comment: “(1)”.

Every residue field of K ⊗[k] S is algebraic over K when #S < #K.

theorem Algebra.isAlgebraic_tensorProduct_quotient_of_card_lt (k : Type t) [CommSemiring k]
    (S : Type v) [CommRing S] [Algebra k S] (K : Type w) [Field K] [Algebra k K]
    (hcard : lift.{w} #S < lift.{v} #K) (m : Ideal (K ⊗[k] S)) [m.IsMaximal] :
    Algebra.IsAlgebraic K ((K ⊗[k] S) ⧸ m)

isJacobsonRing_tensorProduct_of_card_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Nullstellensatz.lean, line 412. The attribute's comment: “(2)”.

The base change K ⊗[k] S is Jacobson when #S < #K.

theorem isJacobsonRing_tensorProduct_of_card_lt (k : Type t) [CommSemiring k]
    (S : Type v) [CommRing S] [Algebra k S] (K : Type w) [Field K] [Algebra k K]
    (hcard : lift.{w} #S < lift.{v} #K) : IsJacobsonRing (K ⊗[k] S)
Tag 00G6, a lemma

Tag 00G6 in the Stacks Project.

Declarations registered for the tag:

Tag 00G7, an example

Tag 00G7 in the Stacks Project.

nonempty_ringEquiv_rat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 373.

ℤ_{(2)}[1/2] is isomorphic to ℚ as a ring.

theorem nonempty_ringEquiv_rat : Nonempty (StacksR_at_2 ≃+* ℚ)
Tag 00G8, an example

Tag 00G8 in the Stacks Project.

specMapZQ_specQPoint_eq_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 478.

The inclusion ℤ → ℚ sends the unique point of Spec(ℚ) to the generic point (0) of Spec(ℤ).

theorem specMapZQ_specQPoint_eq_genericPoint :
    specMapZQ specQPoint = specZGenericPoint
Tag 00G9, a lemma

Tag 00G9 in the Stacks Project.

jacobson_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Constructions.lean, line 92.

Let R be a Jacobson ring and I ⊆ R an ideal. Then R ⧸ I is Jacobson, and maximal ideals of R ⧸ I correspond (via Ideal.comap (Ideal.Quotient.mk I)) to maximal ideals of R containing I.

theorem jacobson_quotient
    {R : Type*} [CommRing R] [IsJacobsonRing R] (I : Ideal R) :
    IsJacobsonRing (R ⧸ I) ∧
      ∃ e : {M : Ideal (R ⧸ I) // M.IsMaximal} ≃
            {J : Ideal R // J.IsMaximal ∧ I ≤ J},
        ∀ (M : {M : Ideal (R ⧸ I) // M.IsMaximal}),
          (e M).1 = Ideal.comap (Ideal.Quotient.mk I) M.1
Tag 0CY7, a lemma

Tag 0CY7 in the Stacks Project.

Algebra.ker_algebraMap_isMaximal_of_finiteType_of_isJacobsonRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/FiniteType.lean, line 86. References: EGA IV (10.4.6), “preimage of max ideal”.

Stacks 0CY7. Let R be a Jacobson ring and let K be a field which is of finite type as an R-algebra. Then RingHom.ker (algebraMap R K) is a maximal ideal of R. In particular, if R is a subring of K then R is a field; that K is then finite over R is finite_of_finite_type_of_isJacobsonRing.

public theorem Algebra.ker_algebraMap_isMaximal_of_finiteType_of_isJacobsonRing
    (R K : Type*) [CommRing R] [Field K] [Algebra R K] [IsJacobsonRing R]
    [Algebra.FiniteType R K] :
    (RingHom.ker (algebraMap R K)).IsMaximal
Tag 00GB, a proposition

Tag 00GB in the Stacks Project.

Declarations registered for the tag:

Tag 00GC, a lemma

Tag 00GC in the Stacks Project.

isJacobsonRing_of_finiteType_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Examples.lean, line 229.

A finite type algebra over ℤ is a Jacobson ring.

theorem isJacobsonRing_of_finiteType_int (B : Type*) [CommRing B] [Algebra ℤ B]
    [Algebra.FiniteType ℤ B] : IsJacobsonRing B
Tag 00GD, a lemma

Tag 00GD in the Stacks Project.

stacks00GD_closedPoints_inter_image_subset_subspaceClosedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Constructions.lean, line 266. The attribute's comment: “Only the trivial inclusion X₀ ∩ f(E) ⊆ f(E)₀ of part (1), for an arbitrary ring map and arbitrary E. The Jacobson, finite-type and constructibility content of 00GD, the reverse inclusion and part (2) are not formalized.”.

Stacks 00GD, trivial inclusion of part (1) (X₀ ∩ f(E) ⊆ f(E)₀).

Let φ : R →+* S be any ring map and let E ⊆ Spec S be any subset; write f = Spec(φ) : Spec S → Spec R. Any closed point of Spec R lying in the image f(E) is closed in the subspace topology on f(E).

This is the inclusion the Stacks proof of Tag 00GD describes as "trivial". The full statement of Tag 00GD requires the Jacobson and finite-type hypotheses (used in the reverse inclusion and the harder part (2)).

theorem stacks00GD_closedPoints_inter_image_subset_subspaceClosedPoints
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (E : Set (PrimeSpectrum S)) :
    closedPoints (PrimeSpectrum R) ∩ (PrimeSpectrum.comap φ '' E)
      ⊆ subspaceClosedPoints (PrimeSpectrum.comap φ '' E)
Tag 00GE, a lemma

Tag 00GE in the Stacks Project.

PrimeSpectrum.isConstructible_comap_image_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Constructible/Chevalley.lean, line 269. The attribute's comment: “first step of the proof only: images of constructible sets are constructible”. References: SGA 1 IV (6.2), “affine source and target”.

The first step in Stacks 00GE: for a finite-type map out of a Noetherian ring, the image of a constructible set is constructible. The closed-point square of 00GE is not formalized here.

theorem PrimeSpectrum.isConstructible_comap_image_of_finiteType
    {R S : Type*} [CommRing R] [CommRing S] [IsNoetherianRing R]
    (φ : R →+* S) (hφ : φ.FiniteType)
    {E : Set (PrimeSpectrum S)} (hE : Topology.IsConstructible E) :
    Topology.IsConstructible (PrimeSpectrum.comap φ '' E)
Tag 00GG, an example

Tag 00GG in the Stacks Project.

idempotent_matrices_classified_by_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/Idempotent.lean, line 114. The attribute's comment: “linear-algebra part: idempotents are classified by rank”.

Stacks Tag 00GG (example of idempotent matrices).

Let K be a field and consider the affine scheme of n × n idempotent matrices, i.e. the spectrum of R = K[{t_{ij}}] / 𝔞 where 𝔞 is the ideal generated by the entries of T² - T. Its K-points are exactly the matrices M with M * M = M.

The example asserts that, by linear algebra, each idempotent matrix M is conjugate (under the GLₙ-action g, T ↦ g T g⁻¹) to a diagonal matrix diag(1, …, 1, 0, …, 0) with r = rank M ones, and that an idempotent is classified up to conjugation by its rank. Consequently distinct ranks give distinct conjugation orbits — these are precisely the irreducible components of the scheme, and orbits of different rank are disjoint.

We record the linear-algebra heart of the example: for idempotent M, N,

  • M and N are conjugate iff they have the same rank (classification by rank, which makes distinct-rank orbits disjoint), and
  • M is conjugate to the standard idempotent diag(1, …, 1, 0, …, 0) carrying rank M ones (existence of the diagonal normal form).

This holds over every commutative local ring; the field in the example is a special case.

Here IsConj M N unfolds to ∃ g : (Matrix (Fin n) (Fin n) K)ˣ, g * M = N * g, i.e. g * M * g⁻¹ = N, which is exactly the GLₙ-conjugation action of the statement.

theorem idempotent_matrices_classified_by_rank
    (M N : Matrix (Fin n) (Fin n) K) (hM : M * M = M) (hN : N * N = N) :
    (IsConj M N ↔ M.rank = N.rank) ∧
      IsConj M (Matrix.diagonal (fun i : Fin n => if (i : ℕ) < M.rank then (1 : K) else 0))

Matrix.trace_eq_rank_of_isIdempotentElem, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/Idempotent.lean, line 128. The attribute's comment: “the trace separates the orbits in characteristic 0”.

The trace of an idempotent matrix over a commutative local ring is its rank, cast to the ring. In characteristic zero, distinct ranks therefore give distinct traces.

lemma Matrix.trace_eq_rank_of_isIdempotentElem (M : Matrix (Fin n) (Fin n) K)
    (hM : IsIdempotentElem M) : M.trace = (M.rank : K)
Sources
LeanIsJacobsonRing · isJacobsonRing_iff · isJacobsonRing_of_finiteType · isJacobsonRing_iff_prime_eq · PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace · exists_prime_vCapD_singleton_isField_of_not_isJacobsonRing · vCapD_infinite_of_isJacobsonRing · isJacobsonRing_of_domain_noetherian_dim_le_one_infinite_maximalSpectrum

Section10.36 Finite and integral ring extensions#

Section 10.36 of the Stacks Project, Tag 00GH. 23 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 24 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00GI, a definition

Tag 00GI in the Stacks Project.

Declarations registered for the tag:

Tag 052I, a lemma

Tag 052I in the Stacks Project.

isIntegral_of_fg_stable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/AwayExactSequence.lean, line 183.

General determinant-trick lemma: if M is a finitely-generated R-submodule of an R-algebra B that contains 1 and is stable under multiplication by α, then α is integral over R.

theorem isIntegral_of_fg_stable
    {R B : Type*} [CommRing R] [Ring B] [Algebra R B]
    (M : Submodule R B) (hMfg : M.FG) (h1 : (1 : B) ∈ M)
    (α : B) (hstable : ∀ z ∈ M, α * z ∈ M) :
    IsIntegral R α
Tag 00GM, a lemma

Tag 00GM in the Stacks Project.

Declarations registered for the tag:

Tag 02JJ, a lemma

Tag 02JJ in the Stacks Project.

Algebra.finite_iff_exists_finset_adjoin_eq_top_and_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Basic.lean, line 369. References: EGA II (6.1.2), “more general”.

An algebra is module-finite if and only if it is generated as an algebra by a finite set of integral elements.

theorem Algebra.finite_iff_exists_finset_adjoin_eq_top_and_isIntegral
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] :
    Module.Finite R S ↔
      ∃ (s : Finset S), Algebra.adjoin R (s : Set S) = ⊤ ∧ ∀ x ∈ s, IsIntegral R x

Declarations registered for the tag:

Tag 00GN, a lemma

Tag 00GN in the Stacks Project.

Declarations registered for the tag:

Tag 00GO, a lemma

Tag 00GO in the Stacks Project.

Declarations registered for the tag:

Tag 0CY8, a lemma

Tag 0CY8 in the Stacks Project.

isIntegral_pi_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Pi.lean, line 66.

Stacks Tag 0CY8 (finite product integral). Let ι be a finite index type and let φ_i : R_i → S_i be ring maps (recorded as the Algebra (R i) (S i) instances). For the product rings ∏ R_i = ∀ i, R i and ∏ S_i = ∀ i, S i with the product algebra structure, an element s = (s_i)_i of ∏ S_i is integral over ∏ R_i if and only if each component s_i is integral over R_i.

theorem isIntegral_pi_iff (ι : Type*) [Finite ι] (R : ι → Type*) (S : ι → Type*)
    [∀ i, CommRing (R i)] [∀ i, CommRing (S i)] [∀ i, Algebra (R i) (S i)]
    (s : ∀ i, S i) :
    IsIntegral (∀ i, R i) s ↔ ∀ i, IsIntegral (R i) (s i)
Tag 00GP, a definition

Tag 00GP in the Stacks Project.

Declarations registered for the tag:

Tag 0CY9, a lemma

Tag 0CY9 in the Stacks Project.

IsIntegralClosure.pi_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Basic.lean, line 203.

Stacks 0CY9. Let R i → S i be a finite family of ring maps and let S' i be an algebra whose canonical map to S i identifies it with the integral closure of R i in S i. Then ∏ i, S' i is the integral closure of ∏ i, R i in ∏ i, S i, and conversely. Taking S' = R this says that ∏ i, R i → ∏ i, S i is integrally closed if and only if each R i → S i is.

public theorem IsIntegralClosure.pi_iff {ι : Type*} [Finite ι] {R S S' : ι → Type*}
    [∀ i, CommRing (R i)] [∀ i, CommRing (S i)] [∀ i, CommSemiring (S' i)]
    [∀ i, Algebra (R i) (S i)] [∀ i, Algebra (S' i) (S i)] :
    IsIntegralClosure (∀ i, S' i) (∀ i, R i) (∀ i, S i) ↔
      ∀ i, IsIntegralClosure (S' i) (R i) (S i)
Tag 0307, a lemma

Tag 0307 in the Stacks Project.

Stacks.IntegralClosureLocalization.isLocalization_integralClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MinimalPrimeResidueLocalization/IntegralClosure.lean, line 88.

Integral closure commutes with localization: if Rf is the localization of R at M and Sf the localization of S at the image of M, then integralClosure Rf Sf is the localization of integralClosure R S at the image of M.

public theorem isLocalization_integralClosure (M : Submonoid R) [IsLocalization M Rf]
    [IsLocalization (Algebra.algebraMapSubmonoid S M) Sf] :
    letI := integralClosureAlgebra R S Rf Sf
    IsLocalization (Algebra.algebraMapSubmonoid ↥(integralClosure R S) M)
      ↥(integralClosure Rf Sf)
Tag 034K, a lemma

Tag 034K in the Stacks Project.

isIntegral_iff_isIntegral_localization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Localization.lean, line 137.

Stacks Tag 034K. Let φ : R → S be a ring map and x ∈ S. Then x is integral over R if and only if, for every maximal ideal p ⊆ R, the image x_p of x in S_p is integral over R_p (where R_p, S_p are the localizations at p as above, and S_p is regarded as an R_p-algebra via the induced map φ_p : R_p → S_p). Only the maximal ideals are needed; for the all-primes equivalence as the tag states it, which this implies, see isIntegral_iff_forall_isPrime.

theorem isIntegral_iff_isIntegral_localization_atPrime
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] (x : S) :
    IsIntegral R x ↔
      ∀ (p : Ideal R) [p.IsMaximal], IsIntegral (Localization.AtPrime p)
        (algebraMap S (Localization (Algebra.algebraMapSubmonoid S p.primeCompl)) x)

isIntegral_iff_forall_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Localization.lean, line 172.

Stacks Tag 034K, as the tag states it. Let φ : R → S be a ring map and x ∈ S. Then x is integral over R if and only if, for every prime ideal p ⊆ R, the image x_p of x in S_p is integral over R_p.

The substantive direction is isIntegral_iff_isIntegral_localization_atPrime, which needs the hypothesis only at the maximal ideals; integrality at an arbitrary prime follows from integrality over R by base change.

theorem isIntegral_iff_forall_isPrime (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (x : S) :
    IsIntegral R x ↔ ∀ (p : Ideal R) [p.IsPrime], IsIntegral (Localization.AtPrime p)
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S p.primeCompl)) x)
Tag 02JK, a lemma

Tag 02JK in the Stacks Project.

Declarations registered for the tag:

Tag 02JL, a lemma

Tag 02JL in the Stacks Project.

Declarations registered for the tag:

Tag 02JM, a lemma

Tag 02JM in the Stacks Project.

Declarations registered for the tag:

Tag 0308, a lemma

Tag 0308 in the Stacks Project.

integral_closure_transitive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Basic.lean, line 346.

Stacks Tag 0308 (transitivity of integral closure): the integral closure of B' in C equals the integral closure of A in C, as subrings of C.

theorem integral_closure_transitive (f : A →+* B) (g : B →+* C) :
    Cprime f g = Dsub f g
Tag 00GQ, a lemma

Tag 00GQ in the Stacks Project.

integral_overring_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Integral.lean, line 71. References: EGA IV (6.15.5), “special case”.

Lying over: if f : R →+* S is an injective integral ring map, then the induced map Spec S → Spec R is surjective.

theorem integral_overring_surjective
    {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : f.IsIntegral) (hinj : Function.Injective f) :
    Function.Surjective (PrimeSpectrum.comap f)
Tag 00GR, a lemma

Tag 00GR in the Stacks Project.

Declarations registered for the tag:

Tag 00GS, a lemma

Tag 00GS in the Stacks Project.

Algebra.IsIntegral.isMaximal_of_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/GoingUp.lean, line 41. The attribute's comment: “(3) If S is integral over k then every prime of S is a maximal ideal.”.

Stacks 00GS (3). Every prime ideal of an integral algebra over a field is maximal: its contraction to the field is the zero ideal, which is maximal.

theorem Algebra.IsIntegral.isMaximal_of_isPrime {k S : Type*} [Field k] [CommRing S] [Algebra k S]
    [Algebra.IsIntegral k S] (P : Ideal S) [P.IsPrime] : P.IsMaximal

Declarations registered for the tag:

Tag 00GT, a lemma

Tag 00GT in the Stacks Project.

not_le_and_not_le_of_comap_eq_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Integral.lean, line 101.

In an integral extension there are no inclusions between distinct primes with the same contraction: if q ≠ q' are primes of S with equal contractions along algebraMap R S, then neither contains the other.

theorem not_le_and_not_le_of_comap_eq_of_ne
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
    (q q' : Ideal S) [q.IsPrime] [q'.IsPrime]
    (hcomap : q.comap (algebraMap R S) = q'.comap (algebraMap R S))
    (hne : q ≠ q') : ¬ q ≤ q' ∧ ¬ q' ≤ q
Tag 05DR, a lemma

Tag 05DR in the Stacks Project.

Declarations registered for the tag:

Tag 00GU, a lemma

Tag 00GU in the Stacks Project.

Declarations registered for the tag:

Tag 0564, a lemma

Tag 0564 in the Stacks Project.

Module.FinitePresentation.restrictScalars_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Basic.lean, line 133.

Stacks 0564. Let R → S be a finite and finitely presented ring map and let M be an S-module, regarded as an R-module by restriction of scalars. Then M is finitely presented as an R-module if and only if M is finitely presented as an S-module.

public theorem restrictScalars_iff (R S M : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite R S] [Algebra.FinitePresentation R S] :
    Module.FinitePresentation R M ↔ Module.FinitePresentation S M
Tag 052J, a lemma

Tag 052J in the Stacks Project.

shortExact_fmap_gmap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/AwayExactSequence.lean, line 351.

Stacks Tag 052J. Under the hypothesis that R is integrally closed in R_x or in R_y, the sequence 0 → R → R[x/y] ⊕ R[y/x] → R[x/y, y/x] → 0 is a short exact sequence of R-modules: 1. f is injective; 2. im f = ker g; 3. g is surjective.

theorem shortExact_fmap_gmap
    (hx : x ∈ R⁰) (hy : y ∈ R⁰)
    (hint : (∀ α : Localization.Away x, IsIntegral R α → α ∈ (⊥ : Subalgebra R (Localization.Away
        x))) ∨
            (∀ α : Localization.Away y, IsIntegral R α → α ∈ (⊥ : Subalgebra R (Localization.Away
                y)))) :
    Function.Injective (fmap x y) ∧
    LinearMap.range (fmap x y) = LinearMap.ker (gmap x y) ∧
    Function.Surjective (gmap x y)
Sources
LeanRingHom.IsIntegralElem · isIntegral_of_fg_stable · Algebra.finite_adjoin_of_finite_of_isIntegral · IsIntegral.of_mem_of_fg · Algebra.finite_iff_exists_finset_adjoin_eq_top_and_isIntegral · Algebra.finite_iff_isIntegral_and_finiteType · RingHom.IsIntegral.trans · integralClosure

Section10.37 Normal rings#

Section 10.37 of the Stacks Project, Tag 037B. 14 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0309, a definition

Tag 0309 in the Stacks Project.

Declarations registered for the tag:

Tag 034L, a lemma

Tag 034L in the Stacks Project.

integralClosure_isNormalDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Stability.lean, line 151. References: EGA II (6.3.7), “special case”; EGA II (6.3.8), “special case”; EGA II (6.3.9), “special case”; EGA IV (14.5.5), “partial”.

Stacks Tag 034L. If S is a normal domain, then the integral closure of R in S is a normal domain.

theorem integralClosure_isNormalDomain
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    (hS : IsNormalDomain S) :
    IsNormalDomain (integralClosure R S)
Tag 00GW, a definition

Tag 00GW in the Stacks Project.

isAlmostIntegral_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/AlmostIntegral.lean, line 71. The attribute's comment: “(1)”.

For a domain R, an element g of the fraction field is almost integral over R if and only if there is a nonzero r ∈ R with r • g ^ n in the image of R for all n.

theorem isAlmostIntegral_iff (g : FractionRing R) :
    IsAlmostIntegral R g ↔
      ∃ r : R, r ≠ 0 ∧ ∀ n, r • g ^ n ∈ (algebraMap R (FractionRing R)).range

IsCompletelyNormal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/AlmostIntegral.lean, line 79. The attribute's comment: “(2)”.

A domain R is completely normal if every almost integral element of its fraction field lies in the image of R.

def IsCompletelyNormal (R : Type*) [CommRing R] [IsDomain R] : Prop
Tag 00GY, a lemma

Tag 00GY in the Stacks Project.

Declarations registered for the tag:

Tag 00GZ, a lemma

Tag 00GZ in the Stacks Project.

Declarations registered for the tag:

Tag 0BI0, a lemma

Tag 0BI0 in the Stacks Project.

PowerSeries.instIsIntegrallyClosed, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PowerSeries/IntegrallyClosed.lean, line 312. References: EGA IV (21.13.9), “(iv)”.

The formal power series ring R⟦X⟧ over a Noetherian normal domain R is a normal domain: it is integrally closed in its fraction field. Together with PowerSeries.instIsNoetherianRing and PowerSeries.instIsDomain this says that R⟦X⟧ is a Noetherian normal domain.

public instance instIsIntegrallyClosed {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [IsIntegrallyClosed R] : IsIntegrallyClosed R⟦X⟧
Tag 030B, a lemma

Tag 030B in the Stacks Project.

Declarations registered for the tag:

Tag 00GV, a definition

Tag 00GV in the Stacks Project.

IsNormalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Defs.lean, line 28. References: EGA IV (5.13.5); EGA IV (5.13.6).

A commutative ring R is normal if for every prime ideal p the localization R_p is an integrally closed integral domain.

def IsNormalRing (R : Type*) [CommRing R] : Prop
Tag 034M, a lemma

Tag 034M in the Stacks Project.

IsNormalRing.isIntegrallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Defs.lean, line 201. References: EGA IV (6.14.1.1), “(i) necessity”.

A normal ring R is integrally closed in its total ring of fractions Q(R) = FractionRing R.

theorem IsNormalRing.isIntegrallyClosed
    {R : Type*} [CommRing R] (hR : IsNormalRing R) :
    IsIntegrallyClosed R
Tag 037C, a lemma

Tag 037C in the Stacks Project.

IsNormalRing.isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Defs.lean, line 74.

A localization of a normal ring is a normal ring.

theorem IsNormalRing.isLocalization {R : Type*} [CommRing R] (h : IsNormalRing R)
    (M : Submonoid R) (S : Type*) [CommRing S] [Algebra R S] [IsLocalization M S] :
    IsNormalRing S
Tag 00H1, a lemma

Tag 00H1 in the Stacks Project.

polynomial_ring_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Polynomial.lean, line 60.

Stacks Lemma 10.37.14: if R is a normal ring, then the polynomial ring R[x] (Polynomial R) is a normal ring.

theorem polynomial_ring_normal (R : Type*) [CommRing R] (hR : IsNormalRing R) :
    IsNormalRing (Polynomial R)
Tag 0CYA, a lemma

Tag 0CYA in the Stacks Project.

isNormalRing_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Stability.lean, line 277.

A finite product of normal rings is normal. (Stacks Lemma 10.37.16, tag 0CYA.)

theorem isNormalRing_pi
    {ι : Type*} [Finite ι] {R : ι → Type*} [∀ i, CommRing (R i)]
    (h : ∀ i, IsNormalRing (R i)) :
    IsNormalRing (∀ i, R i)
Tag 030C, a lemma

Tag 030C in the Stacks Project.

isIntegrallyClosed_tfae_of_finite_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/ProductOfDomains.lean, line 256. References: EGA IV (5.13.5), “Noeth ⇒ product of doms”; EGA IV (6.14.1.1), “(i)”.

Stacks 030C. Let R be a reduced ring with finitely many minimal primes. Then the following are equivalent: (1) R is a normal ring, i.e. all its localizations at primes are normal domains; (2) R is integrally closed in its total ring of fractions; (3) R is a finite product of normal domains; (4) the canonical map from R to the product of the quotients R/𝔭 by its minimal primes is bijective and each such quotient is integrally closed.

theorem isIntegrallyClosed_tfae_of_finite_minimalPrimes {R : Type u} [CommRing R]
    [IsReduced R] (hR : (minimalPrimes R).Finite) :
    List.TFAE
      [ ∀ (p : Ideal R) [p.IsPrime],
          IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p),
        IsIntegrallyClosed R,
        ∃ (n : ℕ) (A : Fin n → Type u) (_ : ∀ i, CommRing (A i)),
          (∀ i, IsDomain (A i)) ∧ (∀ i, IsIntegrallyClosed (A i)) ∧
            Nonempty (R ≃+* ∀ i, A i),
        (∀ p ∈ minimalPrimes R, IsIntegrallyClosed (R ⧸ p)) ∧
          Function.Bijective
            (RingHom.pi fun p : minimalPrimes R => Ideal.Quotient.mk (p : Ideal R)) ]
Tag 037D, a lemma

Tag 037D in the Stacks Project.

directLimit_isNormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Defs.lean, line 488. References: EGA IV (5.13.6), “more general”.

Let (ι, ≤) be a directed nonempty preorder, let (G_i) be a family of commutative rings, and let φ_{ij} : G_i →+* G_j (for i ≤ j) be ring homomorphisms forming a directed system of rings. If every G_i is a normal ring, then the directed colimit Ring.DirectLimit G φ is a normal ring.

theorem directLimit_isNormalRing
    (hdir : DirectedSystem G (fun i j h => φ i j h))
    (hnormal : ∀ i, IsNormalRing (G i)) :
    IsNormalRing (Ring.DirectLimit G (fun i j h => φ i j h))
Sources
LeanIsIntegrallyClosed · isIntegrallyClosed_iff · integralClosure_isNormalDomain · isAlmostIntegral_iff · IsCompletelyNormal · IsLocalization.isDomain_of_le_nonZeroDivisors · isIntegrallyClosed_of_isLocalization · PrincipalIdealRing.to_uniqueFactorizationMonoid

Section10.38 Going down for integral over normal#

Section 10.38 of the Stacks Project, Tag 037E. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00H2, a definition

Tag 00H2 in the Stacks Project.

RingHom.IsIntegralElemOverIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/OverIdeal.lean, line 67.

An element g ∈ S is integral over the ideal I ⊂ R with respect to the ring map φ : R →+* S if there exists a monic polynomial P ∈ R[X] of degree d such that every coefficient P.coeff j lies in I ^ (d - j), and P evaluated at g via φ is zero in S.

Since P is monic with d = P.natDegree, the leading coefficient P.coeff d equals 1 ∈ I ^ 0 = ⊤, and the coefficients above the degree vanish, so the condition ∀ j, P.coeff j ∈ I ^ (d - j) is exactly the Stacks requirement on the non-leading coefficients a_j ∈ I ^ (d - j) for j < d.

def IsIntegralElemOverIdeal {R S : Type*} [CommRing R] [Ring S]
    (φ : R →+* S) (I : Ideal R) (g : S) : Prop
Tag 00H3, a lemma

Tag 00H3 in the Stacks Project.

isIntegralElem_of_isIntegralOverIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/OverIdeal.lean, line 226. The attribute's comment: “Forward implication only: integral over I implies C s * X integral over reesAlgebra I. The converse half of the equivalence is not formalized.”.

If s : S is integral over the ideal I ⊂ R (with respect to φ : R →+* S), then C s · X ∈ S[X] is integral over the Rees subalgebra reesAlgebra I viewed inside S[X] via the coefficient-wise extension of φ.

theorem isIntegralElem_of_isIntegralOverIdeal (φ : R →+* S) (I : Ideal R) (s : S)
    (h : IsIntegralOverIdeal φ I s) :
    (reesToPolyS φ I).IsIntegralElem (C s * X)

isIntegralElem_of_isIntegralElemOverIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/OverIdealIntegrallyClosed.lean, line 92. The attribute's comment: “Forward implication only: integral over I implies C s * X integral over reesAlgebra I. The converse half of the equivalence is not formalized.”.

[Stacks, Tag 00H3], the forward implication. If s : S is integral over the ideal I ⊆ R with respect to φ : R →+* S, then C s · X ∈ S[X] is integral over the Rees subalgebra reesAlgebra I, viewed inside S[X] along the coefficientwise extension of φ.

A monic witness of degree zero is 1, whose vanishing at s makes s = 0, and then C s · X is zero and X is a witness; otherwise forwardWitness multiplies the i-th coefficient by X ^ (n - i) to land in the Rees algebra.

theorem isIntegralElem_of_isIntegralElemOverIdeal (φ : R →+* S) (I : Ideal R) (s : S)
    (h : φ.IsIntegralElemOverIdeal I s) :
    (reesToPolyS φ I).IsIntegralElem (C s * X)
Tag 00H4, a lemma

Tag 00H4 in the Stacks Project.

zero_isIntegralElemOverIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/OverIdeal.lean, line 264. The attribute's comment: “Partial: only that 0 is integral over I. Closure under addition, and hence the submodule conclusion of 00H4, is not formalized.”.

The zero element of S is integral over any ideal I ⊂ R, witnessed by the polynomial X. (Partial component of Stacks 00H4.)

theorem zero_isIntegralElemOverIdeal
    {R : Type*} {S : Type*} [CommRing R] [Ring S]
    (φ : R →+* S) (I : Ideal R) :
    RingHom.IsIntegralElemOverIdeal φ I (0 : S)

mul_left_isIntegralElemOverIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/OverIdeal.lean, line 290. The attribute's comment: “Partial: only closure under R-scalar multiplication. Closure under addition, and hence the submodule conclusion of 00H4, is not formalized.”.

If g ∈ S is integral over the ideal I and r ∈ R, then φ r * g is integral over I. (Partial component of Stacks 00H4: closure under R-scalar multiplication, with the action expressed through the ring map φ.)

theorem mul_left_isIntegralElemOverIdeal
    {R : Type*} {S : Type*} [CommRing R] [CommRing S]
    (φ : R →+* S) (I : Ideal R) (r : R) (g : S)
    (h : RingHom.IsIntegralElemOverIdeal φ I g) :
    RingHom.IsIntegralElemOverIdeal φ I (φ r * g)
Tag 00H5, a lemma

Tag 00H5 in the Stacks Project.

Declarations registered for the tag:

Tag 00H7, a lemma

Tag 00H7 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanRingHom.IsIntegralElemOverIdeal · isIntegralElem_of_isIntegralOverIdeal · isIntegralElem_of_isIntegralElemOverIdeal · zero_isIntegralElemOverIdeal · mul_left_isIntegralElemOverIdeal · Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map · minpoly.isIntegrallyClosed_eq_field_fractions

Section10.39 Flat modules and flat ring maps#

Section 10.39 of the Stacks Project, Tag 00H9. 18 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 19 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00HB, a definition

Tag 00HB in the Stacks Project.

Declarations registered for the tag:

Tag 0BBY, a lemma

Tag 0BBY in the Stacks Project.

ideal_smul_top_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ShortExact.lean, line 208. References: EGA 0 (6.1.3), “second formula”.

Stacks Tag 0BBY: for a flat module M, IM ∩ JM = (I ∩ J) M.

theorem ideal_smul_top_inf (R : Type*) [CommRing R] (I J : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Flat R M] :
    (I • (⊤ : Submodule R M)) ⊓ (J • (⊤ : Submodule R M))
      = (I ⊓ J) • (⊤ : Submodule R M)
Tag 05UT, a lemma

Tag 05UT in the Stacks Project.

colimit_flat_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DirectLimit.lean, line 757. References: EGA 0 (6.1.2); EGA 0 (6.2.3), “constant ring system”; EGA 0 (6.3.4), “partial”; SGA 3 V (4.1.2), “partial”; SGA 4 V (1.2), “special case”; SGA 4 VI (8.6.4), “special case”; SGA 4 XVII (5.5.1.2), “partial”; SGA 4 XVII (5.5.6.3), “partial”.

Stacks 05UT: the direct limit (colimit) of a directed system of flat \(R\)-modules is flat.

theorem colimit_flat_of_flat
    {R : Type*} [CommRing R]
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] [DecidableEq ι]
    (G : ι → Type*) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)]
    (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G (fun i j h => f i j h)]
    [∀ i, Module.Flat R (G i)] :
    Module.Flat R (Module.DirectLimit G f)
Tag 00HC, a lemma

Tag 00HC in the Stacks Project.

Declarations registered for the tag:

  • RingHom.Flat.comp registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 54 (StacksFrontier): “a composition of flat ring maps is flat”. References: EGA 0 (6.7.5), “Affine schemes”; EGA IV (11.3.10.2), “1°, special case”; EGA IV (2.1.6), “special case”; EGA IV (7.3.5), “special case”; EGA 0 (6.6.4), “flat maps compose”; SGA 3 VIIB (1.3.3), “(i), special case”; SGA 6 III (3.4), “special case”.
  • RingHom.FaithfullyFlat.stableUnderComposition registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 62 (StacksFrontier): “a composition of faithfully flat ring maps is faithfully flat”. References: EGA IV (2.2.13), “(iii)”; EGA 0 (6.6.4), “ff maps compose”.
  • Module.Flat.trans registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 66 (StacksFrontier): “a flat module over a flat algebra is flat over the base”. References: EGA 0 (10.2.5), “(a)”; EGA 0 (6.2.1), “more general”; EGA 0 (6.7.5), “special case”; EGA IV (11.3.10.2), “1°”; EGA IV (2.1.5), “special case”; EGA IV (2.1.6), “special case”; EGA IV (2.2.11), “(iii), special case”; EGA IV (7.3.5), “special case”; EGA 0 (6.6.4), “necessity, flat case”; SGA 1 IV (5.9), “(i)”; SGA 3 VIIB (1.3.3), “(i), special case”.
  • Module.FaithfullyFlat.trans registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 78 (StacksFrontier): “a faithfully flat module over a faithfully flat algebra is faithfully flat”. References: EGA IV (11.3.10.2), “1°, special case”; EGA IV (2.2.10), “special case”; EGA IV (2.2.11), “special case”; EGA IV (2.2.13), “(iii)”; EGA 0 (6.6.4), “necessity, ff case”.
Tag 00HD, a lemma

Tag 00HD in the Stacks Project.

Declarations registered for the tag:

Tag 05UU, a lemma

Tag 05UU in the Stacks Project.

StacksColimitRingsFlat.flat_of_forall_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DirectLimit.lean, line 195. The attribute's comment: “(1)”. References: EGA 0 (6.2.3), “special case”.

If M is an R-module that is flat as an R_i-module for every i (via the structure map R_i → R), then M is flat as an R-module.

theorem flat_of_forall_flat
    [Nonempty ι] [IsDirected ι (· ≤ ·)] [DirectedSystem G (fun i j h => (φ i j h : G i → G j))]
    (M : Type*) [AddCommGroup M] [Module (ColimitRing G φ) M]
    (hflat : ∀ i : ι, @Module.Flat (G i) M _ _ (Module.compHom M (structHom G φ i))) :
    Module.Flat (ColimitRing G φ) M

StacksColimitRingsFlat.colimitModule_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DirectLimit.lean, line 469. The attribute's comment: “(2)”. References: EGA 0 (6.1.2), “more general”; EGA 0 (6.2.3); SGA 4 VI (8.6.4), “special case”.

If each M_i is a flat R_i-module and the f_{ii'} are a compatible system of φ_{ii'}-semilinear maps, then the colimit M = colim_i M_i is a flat R-module.

theorem colimitModule_flat
    [Nonempty ι] [IsDirected ι (· ≤ ·)] [DecidableEq ι]
    [DirectedSystem G (fun i j h => (φ i j h : G i → G j))]
    (M : ι → Type*) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module (G i) (M i)]
    (hflat : ∀ i : ι, Module.Flat (G i) (M i))
    (f : (i j : ι) → (h : i ≤ j) → M i →ₛₗ[φ i j h] M j)
    (hf_id : ∀ (i : ι) (x : M i), f i i le_rfl x = x)
    (hf_comp : ∀ (i j k : ι) (hij : i ≤ j) (hjk : j ≤ k) (x : M i),
      f j k hjk (f i j hij x) = f i k (hij.trans hjk) x) :
    Module.Flat (ColimitRing G φ) (ColimitModule M f)
Tag 00HI, a lemma

Tag 00HI in the Stacks Project.

Declarations registered for the tag:

  • Module.Flat.baseChange registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 88 (StacksFrontier): “flat base change”. References: EGA 0 (6.2.1), “more general”; EGA 0 (6.6.3), “necessity”; EGA III (7.4.1), “partial”; EGA III (7.7.2), “special case”; EGA III (7.9.7), “special case”; EGA IV (11.2.6.1), “(ii), sufficiency”; EGA IV (11.3.10.2), “1°”; EGA IV (2.1.4), “special case”; EGA IV (2.1.5), “special case”; EGA IV (2.2.10), “special case”; EGA IV (20.6.9), “partial”; EGA IV (21.15.9), “partial”; SGA 3 III (0.13), “special case”; SGA 3 V (7.4), “(i), special case”; SGA 3 VIB (10.1), “special case”; SGA 3 VIB (11.1), “special case”; SGA 3 VIB (2.1.2), “special case”; SGA 3 VIIB (1.2.1), “partial”; SGA 3 VIIB (1.3.3), “(iii), special case”; SGA 3 XIX (2.1), “special case”; SGA 3 XV (3.8), “partial”; SGA 4 V (1.7.1), “special case”; SGA 4 V (8.2.9), “special case”; SGA 6 III (3.5.2), “Affine case”; SGA 6 IV (3.1.1), “special case”; SGA 6 XII (2.3), “(a)”; SGA 7 VII (1.3.8), “flatness clause”.
  • Module.FaithfullyFlat.instTensorProduct registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 116 (StacksFrontier): “faithfully flat base change”. References: EGA 0 (6.6.3), “necessity”; EGA IV (11.9.14), “affine case”; EGA IV (2.2.10), “special case”; EGA IV (2.2.11), “(i), affine case”; EGA IV (2.2.13), “(i) for affine schemes”; EGA IV (2.2.2), “partial”; EGA IV (2.5.1), “special case”; EGA IV (2.5.8.8), “partial”; EGA 0 (6.4.5), “first assertion”; EGA 0 (6.4.4), “last assertion”.
Tag 00HJ, a lemma

Tag 00HJ in the Stacks Project.

Declarations registered for the tag:

  • Module.Flat.iff_flat_tensorProduct registered with add_to_stacks in StacksFrontier/RingTheory/Flat/Basic.lean, line 131 (StacksFrontier): “flatness descends along a faithfully flat base change”. References: EGA 0 (6.6.3); EGA IV (2.2.11), “(iii), special case”; EGA IV (2.5.1), “flat part, affine”; SGA 3 XIX (2.1), “special case”; SGA 4½ Arcata (1.4.2), “more general”; SGA 6 I (5.7), “a), special case”.
Tag 0584, a lemma

Tag 0584 in the Stacks Project.

Module.Flat.tensorProduct_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BaseChangeAlongFlatAlgebra.lean, line 74. The attribute's comment: “(1)”. References: EGA 0 (6.2.1), “M⊗_A N is B-flat”.

Stacks 0584 (1): if S → S' is a flat map of R-algebras and M is an S-module that is flat over R, then S' ⊗_S M is flat over R.

theorem tensorProduct_of_flat [Module.Flat S S'] [Module.Flat R M] :
    Module.Flat R (S' ⊗[S] M)

Module.Flat.tensorProduct_iff_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BaseChangeAlongFlatAlgebra.lean, line 84. The attribute's comment: “(2)”.

Stacks 0584 (2): if S → S' is a faithfully flat map of R-algebras, then an S-module M is flat over R if and only if S' ⊗_S M is flat over R.

theorem tensorProduct_iff_of_faithfullyFlat {R S S' M : Type*} [CommRing R] [CommRing S]
    [CommRing S'] [Algebra R S] [Algebra R S'] [Algebra S S'] [IsScalarTower R S S']
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.FaithfullyFlat S S'] :
    Module.Flat R (S' ⊗[S] M) ↔ Module.Flat R M
Tag 039V, a lemma

Tag 039V in the Stacks Project.

Stacks.Flatness.NilpotentFibreCriterion.flat_of_flat_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FibrewiseCriterion.lean, line 412. References: EGA 0 (6.6.4), “sufficiency, flat case”.

Flat permanence. If an S-module M is flat over R and faithfully flat over S, then S is flat over R.

theorem flat_of_flat_of_faithfullyFlat
    (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Flat R M] [Module.FaithfullyFlat S M] : Module.Flat R S
Tag 00HL, a lemma

Tag 00HL in the Stacks Project.

tensor_flat_quotient_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatTensorShortExact.lean, line 121. References: EGA 0 (6.1.2), “exactness”; EGA IV (2.1.8), “(i), affine case”; EGA 0 (15.1.17), “more general”; EGA IV (2.1.10), “special case”; SGA 1 IV (1.1), “(i)”; SGA 3 III (4.6.4), “more general”; SGA 4 XVII (4.1.1), “(ii), special case”.

Let 0 → F'' → F' → F → 0 be a short exact sequence of modules over a commutative ring R: a : F'' → F' is injective, the sequence is exact at F' and b : F' → F is surjective. If F is flat, then for every R-module G the tensored sequence 0 → F'' ⊗ G → F' ⊗ G → F ⊗ G → 0 is short exact: a ⊗ 1 is injective, the sequence is exact at F' ⊗ G, and b ⊗ 1 is surjective.

theorem tensor_flat_quotient_shortExact
    {R : Type*} [CommRing R]
    {F'' F' F : Type*} [AddCommGroup F''] [AddCommGroup F'] [AddCommGroup F]
    [Module R F''] [Module R F'] [Module R F]
    (a : F'' →ₗ[R] F') (b : F' →ₗ[R] F)
    (ha : Function.Injective a) (hexact : Function.Exact a b)
    (hb : Function.Surjective b)
    (hFflat : Module.Flat R F)
    (G : Type*) [AddCommGroup G] [Module R G] :
    Function.Injective (LinearMap.rTensor G a) ∧
      Function.Exact (LinearMap.rTensor G a) (LinearMap.rTensor G b) ∧
      Function.Surjective (LinearMap.rTensor G b)

flat_tor_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ShortExact.lean, line 310. References: EGA IV (2.1.8), “(i), affine case”; EGA 0 (15.1.17), “more general”; EGA 0 (6.1.2); SGA 1 IV (1.1); SGA 3 XV (2.10), “partial”; SGA 4 XVII (4.1.1), “(ii), special case”.

If 0 → M'' → M' → M → 0 is a short exact sequence of R-modules whose quotient term M is flat, then tensoring with an arbitrary R-module N leaves the sequence short exact.

theorem flat_tor_zero
    {R : Type*} [CommRing R]
    {M'' M' M N : Type*}
    [AddCommGroup M''] [AddCommGroup M'] [AddCommGroup M] [AddCommGroup N]
    [Module R M''] [Module R M'] [Module R M] [Module R N]
    [Module.Flat R M]
    (f : M'' →ₗ[R] M') (g : M' →ₗ[R] M)
    (hf : Function.Injective f)
    (hfg : Function.Exact f g)
    (hg : Function.Surjective g) :
    Function.Injective (LinearMap.lTensor N f) ∧
    Function.Exact (LinearMap.lTensor N f) (LinearMap.lTensor N g) ∧
    Function.Surjective (LinearMap.lTensor N g)
Tag 00HM, a lemma

Tag 00HM in the Stacks Project.

flat_of_flat_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ShortExact.lean, line 236. References: EGA 0 (6.4.3), “M is flat”; EGA 0 (6.1.2), “M' flat implies M flat”; EGA III (6.5.10), “special case”; EGA IV (2.1.8), “(ii)”; SGA 1 IV (1.1), “(ii)”.

Part 1: In a short exact sequence 0 → M' → M → M'' → 0 of R-modules, if M' and M'' are flat, then M is flat.

theorem flat_of_flat_of_flat
    {R : Type*} [CommRing R]
    {M' M M'' : Type*}
    [AddCommGroup M'] [AddCommGroup M] [AddCommGroup M'']
    [Module R M'] [Module R M] [Module R M'']
    (f : M' →ₗ[R] M) (g : M →ₗ[R] M'')
    (hf : Function.Injective f)
    (hfg : Function.Exact f g)
    (hg : Function.Surjective g)
    [Module.Flat R M'] [Module.Flat R M''] :
    Module.Flat R M

flat_of_flat_of_flat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ShortExact.lean, line 277. References: EGA 0 (20.6.21), “more general”; EGA 0 (6.1.2), “M flat implies M' flat”; EGA IV (2.1.10), “Affine case”; EGA IV (2.1.8), “(ii)”; SGA 1 IV (1.1), “(ii)”; SGA 4 XVII (4.1.1), “(i), special case”; SGA 6 I (5.1.1), “special case”.

Part 2: In a short exact sequence 0 → M' → M → M'' → 0 of R-modules, if M and M'' are flat, then M' is flat.

theorem flat_of_flat_of_flat_quotient
    {R : Type*} [CommRing R]
    {M' M M'' : Type*}
    [AddCommGroup M'] [AddCommGroup M] [AddCommGroup M'']
    [Module R M'] [Module R M] [Module R M'']
    (f : M' →ₗ[R] M) (g : M →ₗ[R] M'')
    (hf : Function.Injective f)
    (hfg : Function.Exact f g)
    (hg : Function.Surjective g)
    [Module.Flat R M] [Module.Flat R M''] :
    Module.Flat R M'
Tag 00HO, a lemma

Tag 00HO in the Stacks Project.

Declarations registered for the tag:

Tag 00HP, a lemma

Tag 00HP in the Stacks Project.

faithfullyFlat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Basic.lean, line 90. References: EGA 0 (6.4.1), “(a) ⇔ (b), (a) ⇔ (d)”; EGA IV (2.2.1), “affine case, a)<=>b)”; EGA IV (2.2.7), “special case”; EGA IV (2.5.8.8), “partial”; SGA 1 IV (2.1), “(i bis) <=> (i ter)”.

For a flat R-module M, faithful flatness is equivalent to each of: M ⊗[R] N is nonzero for every nonzero R-module N; M ⊗[R] κ(𝔭) is nonzero for every prime 𝔭; M ⊗[R] κ(𝔪) is nonzero for every maximal ideal 𝔪.

theorem faithfullyFlat_tfae [Module.Flat R M] :
    [ FaithfullyFlat R M,
      ∀ (N : Type (max u v)) [AddCommGroup N] [Module R N],
        Nontrivial N → Nontrivial (M ⊗[R] N),
      ∀ (p : Ideal R) [p.IsPrime], Nontrivial (M ⊗[R] p.ResidueField),
      ∀ (m : Ideal R) [m.IsMaximal], Nontrivial (M ⊗[R] m.ResidueField) ].TFAE
Tag 00HQ, a lemma

Tag 00HQ in the Stacks Project.

faithfullyFlat_tfae00HQ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Basic.lean, line 168. References: EGA IV (2.2.2), “a)<=>b'), affine F=O_X”; EGA IV (2.2.3), “M = B with A → B flat”; EGA IV (2.2.5), “special case”; EGA IV (2.2.6), “special case”; SGA 1 IV (2.6), “(i) ⇔ (ii) ⇔ (ii bis)”; SGA 1 IV (2.3), “M = B”; SGA 3 V (4.1.1), “Faithful flatness clause”; SGA 4½ Arcata (1.4.1), “special case”.

For a flat ring map f : R →+* S, faithful flatness is equivalent to surjectivity of Spec(S) → Spec(R), and to every closed point of Spec(R) lying in the image of that map.

theorem faithfullyFlat_tfae00HQ
    {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) (hf : RingHom.Flat f) :
    List.TFAE
      [ RingHom.FaithfullyFlat f,
        Function.Surjective (PrimeSpectrum.comap f),
        ∀ x : PrimeSpectrum R, IsClosed ({x} : Set (PrimeSpectrum R)) →
          x ∈ Set.range (PrimeSpectrum.comap f) ]
Tag 00HR, a lemma

Tag 00HR in the Stacks Project.

Declarations registered for the tag:

Tag 00HT, a lemma

Tag 00HT in the Stacks Project.

flat_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Localization.lean, line 65. The attribute's comment: “part1”. References: SGA 1 IV (1.2), “M = B = A”.

The localisation S⁻¹R is a flat R-algebra.

theorem flat_of_isLocalization
    {R : Type*} [CommRing R] (S : Submonoid R)
    (Rs : Type*) [CommRing Rs] [Algebra R Rs] [IsLocalization S Rs] :
    Module.Flat R Rs

flat_iff_flat_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Localization.lean, line 73. The attribute's comment: “part2”. References: SGA 1 IV (1.2), “(i) 2nd assertion”.

For an S⁻¹R-module M, flatness over R is equivalent to flatness over S⁻¹R.

theorem flat_iff_flat_localization
    {R : Type*} [CommRing R] (S : Submonoid R)
    (Rs : Type*) [CommRing Rs] [Algebra R Rs] [IsLocalization S Rs]
    (M : Type*) [AddCommGroup M] [Module R M] [Module Rs M] [IsScalarTower R Rs M] :
    Module.Flat R M ↔ Module.Flat Rs M

flat_iff_forall_flat_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Localization.lean, line 91. The attribute's comment: “part3”. References: SGA 1 IV (1.2), “B = A, primes”.

M is flat over R iff M_𝔭 is flat over R_𝔭 for every prime 𝔭 of R.

theorem flat_iff_forall_flat_atPrime
    {R : Type*} [CommRing R] (M : Type*) [AddCommGroup M] [Module R M] :
    Module.Flat R M ↔
      ∀ (P : Ideal R) (_ : P.IsPrime),
        Module.Flat (Localization.AtPrime P) (LocalizedModule.AtPrime P M)

flat_iff_flat_localizedModule_atMaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Localization.lean, line 103. The attribute's comment: “part4”. References: SGA 1 IV (1.2), “B = A”.

M is flat over R iff M_𝔪 is flat over R_𝔪 for every maximal ideal 𝔪 of R.

theorem flat_iff_flat_localizedModule_atMaximal
    {R : Type*} [CommRing R] (M : Type*) [AddCommGroup M] [Module R M] :
    Module.Flat R M ↔
      ∀ (m : Ideal R) (_ : m.IsMaximal),
        haveI : m.IsPrime := Ideal.IsMaximal.isPrime ‹_›
        Module.Flat (Localization.AtPrime m) (LocalizedModule.AtPrime m M)

flat_of_flat_localizedModule_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Localization.lean, line 190. The attribute's comment: “part7_backward”. References: SGA 1 IV (1.2), “(ii)”.

If every M_𝔪 (for 𝔪 ⊆ A maximal) is flat over R_𝔭 (with 𝔭 = R ∩ 𝔪), then M is flat over R.

theorem flat_of_flat_localizedModule_maximal
    {R : Type*} [CommRing R]
    {A : Type*} [CommRing A] [Algebra R A]
    (M : Type*) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
    (h : ∀ (m : Ideal A) (_ : m.IsMaximal),
        letI : m.IsPrime := Ideal.IsMaximal.isPrime ‹_›
        letI : (m.comap (algebraMap R A)).IsPrime := Ideal.comap_isPrime _ _
        letI : m.LiesOver (m.comap (algebraMap R A)) := ⟨rfl⟩
        letI : Algebra (Localization.AtPrime (m.comap (algebraMap R A)))
                       (Localization.AtPrime m) :=
          Localization.AtPrime.algebraOfLiesOver _ _
        letI : Module (Localization.AtPrime (m.comap (algebraMap R A)))
                      (LocalizedModule.AtPrime m M) :=
          Module.compHom _ (algebraMap _ (Localization.AtPrime m))
        Module.Flat
          (Localization.AtPrime (m.comap (algebraMap R A)))
          (LocalizedModule.AtPrime m M)) :
    Module.Flat R M

flat_of_flat_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Localization.lean, line 217. The attribute's comment: “part6_backward”. References: SGA 1 IV (1.2), “(ii) with all primes”.

If every M_𝔮 (for 𝔮 ⊆ A prime) is flat over R_𝔭 (with 𝔭 = 𝔮 ∩ R), then M is flat over R.

theorem flat_of_flat_atPrime
    {R : Type*} [CommRing R]
    {A : Type*} [CommRing A] [Algebra R A]
    (M : Type*) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
    (h : ∀ (Q : Ideal A) (_ : Q.IsPrime),
        letI : (Q.comap (algebraMap R A)).IsPrime := Ideal.comap_isPrime _ _
        letI : Q.LiesOver (Q.comap (algebraMap R A)) := ⟨rfl⟩
        letI : Algebra (Localization.AtPrime (Q.comap (algebraMap R A)))
                       (Localization.AtPrime Q) :=
          Localization.AtPrime.algebraOfLiesOver _ _
        letI : Module (Localization.AtPrime (Q.comap (algebraMap R A)))
                      (LocalizedModule.AtPrime Q M) :=
          Module.compHom _ (algebraMap _ (Localization.AtPrime Q))
        Module.Flat
          (Localization.AtPrime (Q.comap (algebraMap R A)))
          (LocalizedModule.AtPrime Q M)) :
    Module.Flat R M
Tag 090N, a lemma

Tag 090N in the Stacks Project.

faithfullyFlat_directLimit_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DirectLimit.lean, line 582. References: SGA 3 VIB (11.17.1), “constant base”.

A directed colimit of faithfully flat R-algebras is faithfully flat over R: if each R → Sᵢ is faithfully flat and the transition maps are R-algebra maps, then the induced map from R to colim Sᵢ is faithfully flat.

theorem faithfullyFlat_directLimit_of_faithfullyFlat
    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    (R : Type*) [CommRing R]
    (S : ι → Type*) [(i : ι) → CommRing (S i)] [(i : ι) → Algebra R (S i)]
    (φ : (i j : ι) → i ≤ j → S i →+* S j)
    [DirectedSystem S (fun i j h => φ i j h)]
    -- transition maps are R-algebra maps:
    (hφ : ∀ i j (h : i ≤ j), (φ i j h).comp (algebraMap R (S i)) = algebraMap R (S j))
    -- each Sᵢ is faithfully flat over R:
    (hff : ∀ i, (algebraMap R (S i)).FaithfullyFlat) :
    ((Ring.DirectLimit.of S (fun i j h => φ i j h) (Classical.arbitrary ι)).comp
      (algebraMap R (S (Classical.arbitrary ι)))).FaithfullyFlat
Sources
LeanModule.Flat · Module.Flat.iff_lTensor_exact · Module.FaithfullyFlat · Module.FaithfullyFlat.iff_exact_iff_lTensor_exact · RingHom.Flat · ideal_smul_top_inf · colimit_flat_of_flat · RingHom.Flat.comp

Section10.40 Supports and annihilators#

Section 10.40 of the Stacks Project, Tag 080S. 7 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0585, a lemma

Tag 0585 in the Stacks Project.

Declarations registered for the tag:

Tag 07T7, a definition

Tag 07T7 in the Stacks Project.

Declarations registered for the tag:

Tag 07T8, a lemma

Tag 07T8 in the Stacks Project.

ann_extension_eq_ann_baseChange_elem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Annihilator/FlatBaseChange.lean, line 78.

For a flat ring map φ : R → S and any m in an R-module M, the extension of the annihilator Ann_R(m) to S equals the S-annihilator of the base-changed element 1 ⊗ m ∈ S ⊗_R M: Ann_R(m) S = Ann_S(1 ⊗ m).

theorem ann_extension_eq_ann_baseChange_elem [Module.Flat R S] (m : M) :
    Ideal.map (algebraMap R S) (Ideal.torsionOf R M m)
      = Ideal.torsionOf S (S ⊗[R] M) ((1 : S) ⊗ₜ[R] m)

ann_extension_eq_ann_baseChange_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Annihilator/FlatBaseChange.lean, line 301. References: EGA IV (2.1.11), “affine case”.

For a flat ring map φ : R → S and a finite R-module M, the extension of the annihilator Ann_R(M) to S equals the S-annihilator of the base change S ⊗_R M: Ann_R(M) S = Ann_S(S ⊗_R M).

theorem ann_extension_eq_ann_baseChange_module [Module.Flat R S] [Module.Finite R M] :
    Ideal.map (algebraMap R S) (Module.annihilator R M)
      = Module.annihilator S (S ⊗[R] M)
Tag 00L2, a lemma

Tag 00L2 in the Stacks Project.

Declarations registered for the tag:

  • Module.isClosed_support registered with add_to_stacks in StacksFrontier/RingTheory/Support/Basic.lean, line 168 (StacksFrontier): “the support of a finite module is closed”. References: EGA 0 (16.1.7), “partial”; EGA 0 (5.2.2), “special case”; EGA I (4.1.2), “affine case”; EGA IV (5.1.12), “special case”; EGA IV (8.9.1), “closedness of Supp(F)”; SGA 3 VIA (2.1.3), “special case”.
Tag 0BUR, a lemma

Tag 0BUR in the Stacks Project.

IsBaseChange.support_eq_preimage_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Basic.lean, line 137.

Stacks 0BUR. Let R → S be a ring map, let M be a finite R-module and let f : M →ₗ[R] N exhibit the S-module N as the base change S ⊗_R M. Then Supp_S(N) is the inverse image of Supp_R(M) under the map Spec(S) → Spec(R) induced by R → S.

theorem support_eq_preimage_comap {R S M N : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N]
    [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) :
    Module.support S N = PrimeSpectrum.comap (algebraMap R S) ⁻¹' Module.support R M
Tag 051B, a lemma

Tag 051B in the Stacks Project.

support_isClosed_and_compl_isCompact_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Basic.lean, line 232. The attribute's comment: “Assumes (Module.annihilator R M).FG as a hypothesis. Stacks 051B derives that finite generation from a presentation matrix, so that step is not formalized.”. References: EGA 0 (16.1.7), “special case”; EGA 0 (5.2.2), “special case”.

The support of a finitely presented module whose annihilator is finitely generated is closed with quasi-compact complement.

The argument factors as: for a finite module M, Supp M = V(Ann M); and closed-with-quasi-compact-complement is a topological consequence of being V(I) for I finitely generated. Finite generation of Ann(R, M) for M finitely presented rests on the ideal of n × n minors of a presentation matrix being finitely generated, and is taken here as the hypothesis (Module.annihilator R M).FG.

theorem support_isClosed_and_compl_isCompact_of_finitePresentation
    [Module.FinitePresentation R M]
    (hAnn : (Module.annihilator R M).FG) :
    IsClosed (Module.support R M) ∧ IsCompact (Module.support R M)ᶜ
Tag 00L3, a lemma

Tag 00L3 in the Stacks Project.

support_submodule_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Basic.lean, line 192. The attribute's comment: “(2)”. References: EGA 0 (1.7.2), “partial”.

The support of a submodule is contained in the support of the ambient module.

theorem support_submodule_subset
    {R : Type*} {M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    (N : Submodule R M) :
    Module.support R N ⊆ Module.support R M
Sources
LeanModule.support_eq_empty_iff · Ideal.torsionOf · Module.annihilator · ann_extension_eq_ann_baseChange_elem · ann_extension_eq_ann_baseChange_module · Module.isClosed_support · IsBaseChange.support_eq_preimage_comap · support_isClosed_and_compl_isCompact_of_finitePresentation

Section10.41 Going up and going down#

Section 10.41 of the Stacks Project, Tag 00HU. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00HV, a definition

Tag 00HV in the Stacks Project.

RingHom.GoingUp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/GoingUpGoingDown/Defs.lean, line 63. The attribute's comment: “(1)”.

A ring map φ : R → S satisfies going up if for all primes p ⊆ p' of R and every prime q of S lying over p (that is, Ideal.comap φ q = p), there exists a prime q' of S with q ⊆ q' lying over p'.

def RingHom.GoingUp (φ : R →+* S) : Prop

RingHom.GoingDown, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/GoingUpGoingDown/Defs.lean, line 73. The attribute's comment: “(2)”.

A ring map φ : R → S satisfies going down if for all primes p ⊆ p' of R and every prime q' of S lying over p' (that is, Ideal.comap φ q' = p'), there exists a prime q of S with q ⊆ q' lying over p.

def RingHom.GoingDown (φ : R →+* S) : Prop
Tag 0407, a lemma

Tag 0407 in the Stacks Project.

isOpenMap_comap_satisfiesGoingDown, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Specialization.lean, line 653.

Stacks Tag 0407 (Lemma 10.41.2): if the induced map on prime spectra φ* = PrimeSpectrum.comap φ : Spec(S) → Spec(R) is an open map, then φ satisfies going down.

theorem isOpenMap_comap_satisfiesGoingDown
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (h : IsOpenMap (comap φ)) : φ.SatisfiesGoingDown
Tag 00HW, a lemma

Tag 00HW in the Stacks Project.

goingDown_iff_liftsGeneralizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Specialization.lean, line 299. The attribute's comment: “(1)”.

Stacks 00HW (1). A ring map φ : R → S satisfies going down if and only if generalizations lift along Spec(S) → Spec(R).

theorem goingDown_iff_liftsGeneralizations (φ : R →+* S) :
    RingHom.GoingDown φ ↔
      LiftsGeneralizations (PrimeSpectrum.comap φ)

goingUp_iff_liftsSpecializations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Specialization.lean, line 308. The attribute's comment: “(2)”.

Stacks 00HW (2). A ring map φ : R → S satisfies going up if and only if specializations lift along Spec(S) → Spec(R).

theorem goingUp_iff_liftsSpecializations (φ : R →+* S) :
    RingHom.GoingUp φ ↔
      LiftsSpecializations (PrimeSpectrum.comap φ)
Tag 00HX, a lemma

Tag 00HX in the Stacks Project.

RingHom.hasGoingDown_and_hasGoingUp_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Specialization.lean, line 128. The attribute's comment: “Both assertions, for a composite of ring maps. For a tower of algebras they are Algebra.HasGoingDown.trans and Algebra.HasGoingUp.trans, which carry this tag as well.”.

Stacks 00HX. If the ring maps f : R →+* S and g : S →+* T satisfy going down, then so does g ∘ f; likewise for going up.

public theorem hasGoingDown_and_hasGoingUp_comp {R S T : Type*} [CommRing R] [CommRing S]
    [CommRing T] (f : R →+* S) (g : S →+* T) :
    (letI := f.toAlgebra; letI := g.toAlgebra; letI := (g.comp f).toAlgebra;
      Algebra.HasGoingDown R S → Algebra.HasGoingDown S T → Algebra.HasGoingDown R T) ∧
    (letI := f.toAlgebra; letI := g.toAlgebra; letI := (g.comp f).toAlgebra;
      Algebra.HasGoingUp R S → Algebra.HasGoingUp S T → Algebra.HasGoingUp R T)
Tag 00HZ, a lemma

Tag 00HZ in the Stacks Project.

goingUp_iff_isClosedMap_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Specialization.lean, line 358.

Stacks 00HZ. For a ring map φ : R → S, going up holds if and only if the induced map Spec(S) → Spec(R) is closed.

theorem goingUp_iff_isClosedMap_comap (φ : R →+* S) :
    RingHom.GoingUp φ ↔ IsClosedMap (PrimeSpectrum.comap φ)
Tag 037F, a lemma

Tag 037F in the Stacks Project.

Stacks.TensorProductSpecImage.images_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/SpecImage.lean, line 257.

The images in Spec(R) of the two diagonal maps coincide: im(Spec(α)) = im(Spec(α')).

theorem images_eq (hι : Function.Injective ι) :
    Set.range (PrimeSpectrum.comap (R := R)
        (S := Localization.Away (baseChangeIncl k R S S' ι f)) (alphaMap k R S S' ι f)) =
      Set.range (PrimeSpectrum.comap (R := R) (S := Localization.Away f) (alphaPrime k R S'
          f))
Tag 00EA, a lemma

Tag 00EA in the Stacks Project.

localization_eq_of_unique_prime_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/UniquePrimeOver.lean, line 67.

If p is a prime of R with a unique prime q of S lying over it, and R → S satisfies going up (or going down together with injectivity of contraction on primes), then the localization of S at the image of R ∖ p is also a localization of S at the complement of q; that is, S_p = S_q.

theorem localization_eq_of_unique_prime_over
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (huniq : ∀ q' : Ideal S, q'.IsPrime → q'.LiesOver p → q' = q)
    (h2 :
      (∀ (p₁ p₂ : Ideal R) (q₁ : Ideal S), p₁.IsPrime → p₂.IsPrime → q₁.IsPrime →
          p₁ ≤ p₂ → q₁.under R = p₁ →
            ∃ q₂ : Ideal S, q₂.IsPrime ∧ q₁ ≤ q₂ ∧ q₂.under R = p₂) ∨
      (Algebra.HasGoingDown R S ∧
        ∀ (q₁ q₂ : Ideal S), q₁.IsPrime → q₂.IsPrime →
          q₁.under R = q₂.under R → q₁ = q₂)) :
    IsLocalization q.primeCompl
      (Localization (Algebra.algebraMapSubmonoid S p.primeCompl))
Tag 080T, a lemma

Tag 080T in the Stacks Project.

generalizingMap_suppMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/GoingDown.lean, line 379. References: SGA 1 IV (2.4), “more general”.

Stacks Tag 080T (topological formulation). If N is a finite S-module that is flat over R, then generalizations lift along π : Supp(N) → Spec(R).

theorem generalizingMap_suppMap [Module.Finite S N] [Module.Flat R N] :
    GeneralizingMap (suppMap (R := R) (S := S) (N := N))
Sources
LeanRingHom.GoingUp · RingHom.GoingDown · isOpenMap_comap_satisfiesGoingDown · goingDown_iff_liftsGeneralizations · goingUp_iff_liftsSpecializations · RingHom.hasGoingDown_and_hasGoingUp_comp · goingUp_iff_isClosedMap_comap · Stacks.TensorProductSpecImage.images_eq

Section10.42 Separable extensions#

Section 10.42 of the Stacks Project, Tag 030I. 4 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 030O, a definition

Tag 030O in the Stacks Project.

Algebra.IsSeparableExtension, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/Separable/Defs.lean, line 91. The attribute's comment: “part (2)”.

A field extension K/k is separable if every subextension k ⊆ K' ⊆ K with K' finitely generated over k is separably generated over k. For algebraic extensions this is Mathlib's Algebra.IsSeparable.

public class IsSeparableExtension (k K : Type*) [Field k] [Field K] [Algebra k K] : Prop
Tag 030P, a lemma

Tag 030P in the Stacks Project.

Declarations registered for the tag:

Tag 030Q, a lemma

Tag 030Q in the Stacks Project.

separablyGenerated_fg_exists_primitive_transcendence_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/TranscendentalSeparable.lean, line 588.

Stacks 030Q (Lemma 10.42.3). If K/k is separably generated and finitely generated, with transcendence degree r, then there are x_1, ..., x_{r+1} ∈ K (here packaged as x : Fin (r+1) → K) such that:

  1. x_1, ..., x_r (the entries x i.castSucc) form a transcendence basis of K over k;
  2. K = k(x_1, ..., x_{r+1}) (the adjoin of the whole tuple is ⊤); and
  3. x_{r+1} (the entry x (Fin.last r)) is separable over the subfield k(x_1, ..., x_r) generated by the first r entries.
theorem separablyGenerated_fg_exists_primitive_transcendence_basis
    (k K : Type*) [Field k] [Field K] [Algebra k K]
    (hsep : SeparablyGenerated k K)
    (hfg : (⊤ : IntermediateField k K).FG)
    (r : ℕ) (hr : Algebra.trdeg k K = r) :
    ∃ x : Fin (r + 1) → K,
      IsTranscendenceBasis k (fun i : Fin r => x i.castSucc) ∧
      IntermediateField.adjoin k (Set.range x) = ⊤ ∧
      IsSeparable
        (↥(IntermediateField.adjoin k (Set.range (fun i : Fin r => x i.castSucc))))
        (x (Fin.last r))
Tag 04KM, a lemma

Tag 04KM in the Stacks Project.

exists_isPurelyInseparable_and_isSeparablyGenerated_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/TranscendentalSeparable.lean, line 517.

Stacks 04KM. Let K/k be a finitely generated field extension and let Ω/K be a perfect field extension. Then inside Ω there is a diagram 

K  →  K'
↑     ↑
k  →  k'
with k'/k and K'/K finite purely inseparable and K'/k' separably generated.

public theorem exists_isPurelyInseparable_and_isSeparablyGenerated_of_essFiniteType
    (k K Ω : Type*) [Field k] [Field K] [Field Ω] [Algebra k K] [Algebra k Ω] [Algebra K Ω]
    [IsScalarTower k K Ω] [PerfectField Ω] [Algebra.EssFiniteType k K] :
    ∃ (K' : IntermediateField K Ω) (k' : IntermediateField k ↥K'),
      Module.Finite K ↥K' ∧ IsPurelyInseparable K ↥K' ∧
      Module.Finite k ↥k' ∧ IsPurelyInseparable k ↥k' ∧
      Algebra.IsSeparablyGenerated ↥k' ↥K'
Sources
LeanAlgebra.IsSeparableExtension · Algebra.isSeparable_tower_bot_of_isSeparable · IntermediateField.isSeparable_tower_bot · separablyGenerated_fg_exists_primitive_transcendence_basis · exists_isPurelyInseparable_and_isSeparablyGenerated_of_essFiniteType

Section10.43 Geometrically reduced algebras#

Section 10.43 of the Stacks Project, Tag 05DS. 8 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 030T, a lemma

Tag 030T in the Stacks Project.

DirectLimit.instIsGeometricallyReduced, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/DirectLimit.lean, line 303. The attribute's comment: “Part (3): a directed colimit of geometrically reduced algebras is geometrically reduced, stated for DirectLimit of a directed system of algebras over a commutative base ring. Parts (1) and (2) are Algebra.IsGeometricallyReduced.of_injective and Algebra.IsGeometricallyReduced.of_forall_fg; part (4) is Lemma 04KN.”.

Stacks 030T (3). A directed colimit of geometrically reduced R-algebras is geometrically reduced over R.

public instance instIsGeometricallyReduced
    {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    {G : ι → Type*} [∀ i, Ring (G i)] [∀ i, Algebra R (G i)]
    {T : ∀ ⦃i j : ι⦄, i ≤ j → Type*} {f : ∀ i j (h : i ≤ j), T h}
    [∀ i j (h : i ≤ j), FunLike (T h) (G i) (G j)]
    [∀ i j (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)]
    [DirectedSystem G (f · · ·)]
    [∀ i, Algebra.IsGeometricallyReduced R (G i)] :
    Algebra.IsGeometricallyReduced R (DirectLimit G f)
Tag 04KN, a lemma

Tag 04KN in the Stacks Project.

geometricallyReduced_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/Basic.lean, line 188. The attribute's comment: “(1)”. References: EGA IV (7.3.9), “(ii)”.

If R is geometrically reduced over the field k and A is a localization of R at a multiplicative subset M ⊆ R, carrying the induced k-algebra structure, then A is geometrically reduced over k.

Fix a field extension K/k; then K ⊗[k] R is reduced. The key base-change fact is that K ⊗[k] A is isomorphic to a localization of K ⊗[k] R: viewing K ⊗[k] R as an R-algebra, (K ⊗[k] R) ⊗[R] A is a localization of K ⊗[k] R at the image submonoid Algebra.algebraMapSubmonoid (K ⊗[k] R) M, and cancelling the base change gives a K-algebra isomorphism (K ⊗[k] R) ⊗[R] A ≃ₐ[K] K ⊗[k] A. A localization of a reduced ring is reduced, so (K ⊗[k] R) ⊗[R] A is reduced and reducedness transfers back to K ⊗[k] A along that isomorphism. As K/k was arbitrary, A is geometrically reduced over k.

theorem geometricallyReduced_localization
    (k : Type u) [Field k] (R : Type v) [CommRing R] [Algebra k R]
    (M : Submonoid R) (A : Type v) [CommRing A] [Algebra R A] [IsLocalization M A]
    [Algebra k A] [IsScalarTower k R A]
    (hR : GeometricallyReduced.{u, v, w} k R) :
    GeometricallyReduced.{u, v, w} k A

geometricallyReduced_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/Basic.lean, line 220. The attribute's comment: “(2)”. References: EGA IV (4.6.21), “4.6.21(ii), special case”; EGA IV (4.6.5), “(ii), special case”.

If R is geometrically reduced over the field k, then so is the polynomial ring R[x] in one variable.

Fix a field extension K/k. Then K ⊗[k] R is reduced, hence so is the polynomial ring (K ⊗[k] R)[X], and transferring reducedness backward along the ring isomorphism K ⊗[k] R[X] ≃+* (K ⊗[k] R)[X] shows K ⊗[k] R[X] is reduced. As K/k was arbitrary, R[X] is geometrically reduced.

theorem geometricallyReduced_polynomial
    (k : Type u) [Field k] (R : Type v) [CommRing R] [Algebra k R]
    (hR : GeometricallyReduced.{u, v, w} k R) :
    GeometricallyReduced.{u, v, w} k (Polynomial R)
Tag 00I3, a lemma

Tag 00I3 in the Stacks Project.

not_isReduced_of_not_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/Reduced.lean, line 122. The attribute's comment: “nonreduced”.

Stacks 00I3 (part 1). If R ⊗[k] S is nonreduced, then there exist finitely generated subalgebras R' ⊆ R, S' ⊆ S such that R' ⊗[k] S' is not reduced.

theorem not_isReduced_of_not_isReduced (h : ¬ IsReduced (R ⊗[k] S)) :
    ∃ (R' : Subalgebra k R) (S' : Subalgebra k S), R'.FG ∧ S'.FG ∧
      ¬ IsReduced (R' ⊗[k] S')

exists_zerodivisor_of_exists_zerodivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/Reduced.lean, line 144. The attribute's comment: “zerodivisor”.

Stacks 00I3 (part 2). If R ⊗[k] S contains a nonzero zerodivisor, then there exist finitely generated subalgebras R' ⊆ R, S' ⊆ S such that R' ⊗[k] S' contains a nonzero zerodivisor.

theorem exists_zerodivisor_of_exists_zerodivisor
    (h : ∃ x : R ⊗[k] S, x ≠ 0 ∧ ∃ y : R ⊗[k] S, y ≠ 0 ∧ x * y = 0) :
    ∃ (R' : Subalgebra k R) (S' : Subalgebra k S), R'.FG ∧ S'.FG ∧
      ∃ x : R' ⊗[k] S', x ≠ 0 ∧ ∃ y : R' ⊗[k] S', y ≠ 0 ∧ x * y = 0

exists_idempotent_of_exists_idempotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/Reduced.lean, line 167. The attribute's comment: “idempotent”.

Stacks 00I3 (part 3). If R ⊗[k] S contains a nontrivial idempotent, then there exist finitely generated subalgebras R' ⊆ R, S' ⊆ S such that R' ⊗[k] S' contains a nontrivial idempotent.

theorem exists_idempotent_of_exists_idempotent
    (h : ∃ e : R ⊗[k] S, e * e = e ∧ e ≠ 0 ∧ e ≠ 1) :
    ∃ (R' : Subalgebra k R) (S' : Subalgebra k S), R'.FG ∧ S'.FG ∧
      ∃ e : R' ⊗[k] S', e * e = e ∧ e ≠ 0 ∧ e ≠ 1
Tag 034N, a lemma

Tag 034N in the Stacks Project.

Algebra.IsGeometricallyReduced.isReduced_tensorProduct, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/TensorProduct.lean, line 113. The attribute's comment: “Stated with Mathlib's Algebra.IsGeometricallyReduced in place of the source's Definition 030S, the two being equivalent by Lemma 030V; as an instance, since both hypotheses are classes.”.

The tensor product of a reduced k-algebra R with a geometrically reduced k-algebra S is reduced.

public instance Algebra.IsGeometricallyReduced.isReduced_tensorProduct
    (k R S : Type*) [Field k] [CommRing R] [Algebra k R] [IsReduced R]
    [CommRing S] [Algebra k S] [Algebra.IsGeometricallyReduced k S] :
    IsReduced (R ⊗[k] S)
Tag 030U, a lemma

Tag 030U in the Stacks Project.

Algebra.isReduced_tensorProduct_of_isSeparableExtension_or_isSeparablyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/TensorProduct.lean, line 194. The attribute's comment: “Stated with the two notions of Definition 030O as a disjunctive hypothesis, as in the source: separably generated implies separable is Lemma 030X, whose proof uses this lemma.”. References: EGA 0 (23.1.7), “partial”; EGA IV (4.3.5), “more general”; EGA IV (4.3.6), “special case”.

Let k be a field, let S be a reduced k-algebra and let K/k be a field extension which is either separable or separably generated. Then K ⊗[k] S is reduced.

public theorem Algebra.isReduced_tensorProduct_of_isSeparableExtension_or_isSeparablyGenerated
    {k K S : Type*} [Field k] [Field K] [Algebra k K] [CommRing S] [Algebra k S] [IsReduced S]
    (hK : Algebra.IsSeparableExtension k K ∨ Algebra.IsSeparablyGenerated k K) :
    IsReduced (K ⊗[k] S)
Tag 07K2, a lemma

Tag 07K2 in the Stacks Project.

Algebra.IsGeometricallyReduced.of_forall_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/GeometricallyReduced.lean, line 131. The attribute's comment: “Stated with Mathlib's Algebra.IsGeometricallyReduced in place of the source's Definition 030S, the two being equivalent by Lemma 030V, and with the concrete localization Localization.AtPrime p for the source's S_𝔭.”.

Let k be a field and let S be a reduced k-algebra such that the localization Localization.AtPrime p is geometrically reduced over k for every minimal prime p of S. Then S is geometrically reduced over k.

public theorem Algebra.IsGeometricallyReduced.of_forall_minimalPrimes {k : Type u} {S : Type v}
    [Field k] [CommRing S] [Algebra k S] [IsReduced S]
    (H : ∀ (p : Ideal S) [p.IsPrime], p ∈ minimalPrimes S →
      Algebra.IsGeometricallyReduced k (Localization.AtPrime p)) :
    Algebra.IsGeometricallyReduced k S
Tag 0C2X, a lemma

Tag 0C2X in the Stacks Project.

exists_isLocalization_lmul'_of_isSeparable_isAlgebraic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/SeparableAlgebraic/Localization.lean, line 94.

Stacks Tag 0C2X (Lemma 10.43.8), primary IsLocalization formulation. For a separable algebraic field extension k'/k, equipping k' with the (k' ⊗_k k')-algebra structure given by the multiplication map m = Algebra.TensorProduct.lmul' k, there is a submonoid S ⊆ k' ⊗_k k' such that k' is the localization of k' ⊗_k k' at S.

theorem exists_isLocalization_lmul'_of_isSeparable_isAlgebraic
    (k k' : Type*) [Field k] [Field k'] [Algebra k k']
    [Algebra.IsAlgebraic k k'] [Algebra.IsSeparable k k'] :
    letI : Algebra (k' ⊗[k] k') k' :=
      RingHom.toAlgebra (Algebra.TensorProduct.lmul' (R := k) (S := k')).toRingHom
    ∃ S : Submonoid (k' ⊗[k] k'), IsLocalization S k'
Tag 0C2Y, a lemma

Tag 0C2Y in the Stacks Project.

Algebra.isGeometricallyReduced_iff_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/Separable.lean, line 47.

Stacks 0C2Y. For a separable algebraic field extension k'/k, a k'-algebra is geometrically reduced over k if and only if it is geometrically reduced over k'.

theorem Algebra.isGeometricallyReduced_iff_of_isSeparable (k k' A : Type*) [Field k] [Field k']
    [CommRing A] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A]
    [Algebra.IsSeparable k k'] :
    Algebra.IsGeometricallyReduced k A ↔ Algebra.IsGeometricallyReduced k' A
Sources
LeanDirectLimit.instIsGeometricallyReduced · geometricallyReduced_localization · geometricallyReduced_polynomial · not_isReduced_of_not_isReduced · exists_zerodivisor_of_exists_zerodivisor · exists_idempotent_of_exists_idempotent · Algebra.IsGeometricallyReduced.isReduced_tensorProduct · Algebra.isReduced_tensorProduct_of_isSeparableExtension_or_isSeparablyGenerated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.