Invertible ideals

Invertibility of ideals and of ideal sheaves is the library's notion of "effective Cartier divisor", in the form the blow-up construction uses: a morphism f : Y ⟶ X is admissible for an ideal sheaf I when (I.comap f).IsInvertible, that is, when the inverse image of the subscheme of I is an effective Cartier divisor on Y [TSPA, Tag 0806]. An ideal sheaf is invertible (AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible) when it is generated on an affine neighbourhood of every point by a nonzerodivisor [TSPA, Tag 01WS]; this file defines the ring-level notion in the same local form and proves its algebra.

Main declarations

• Ideal.IsInvertible J [TSPA, Tags 01WR and 01WS]; [Hau14, Definition 4.3]: an ideal J ⊆ A is invertible if for every prime 𝔭 of A there are s ∉ 𝔭 and a ∈ J with J A_s = a A_s and a a nonzerodivisor of A_s.
• Ideal.IsRegularGeneratorIn J B a: the local datum "a generates J B and is a nonzerodivisor of B", with its transport lemmas (of_algEquiv, of_isLocalization, of_isLocalization_away_mul): the datum passes along A-algebra isomorphisms and along further localizations.
• Ideal.isInvertible_top, Ideal.IsInvertible.mul, Ideal.IsInvertible.map_away (localization stability), Ideal.IsInvertible.of_mul (factors of an invertible ideal are invertible).

The arguments

Products. At a prime 𝔭, with J₁ A_{s₁} = (a₁) and J₂ A_{s₂} = (a₂), pass to A_{s₁ s₂}: both data survive (localization preserves nonzerodivisors), and (J₁ J₂) A_{s₁s₂} = (a₁)(a₂) = (a₁ a₂) with a₁ a₂ a nonzerodivisor.

Localization. A prime 𝔮 of A_s lies over a prime 𝔭 ∌ s of A; the datum of J at 𝔭, in A_{s'}, survives in (A_s)_{s'} = A_{s s'}, which is the required neighbourhood of 𝔮.

Factors (the argument of [Hau14, Theorem 4.18, proof (c)], run on a neighbourhood). Let (J₁ J₂) A_s = (g) with g a nonzerodivisor, 𝔮 the prime of A_s over 𝔭. Write g = ∑ aᵢ bᵢ with aᵢ ∈ J₁ A_s, bᵢ ∈ J₂ A_s; each aᵢ bᵢ = tᵢ g, so ∑ tᵢ = 1 after cancelling g, and some tᵢ ∉ 𝔮. Localizing further at tᵢ, aᵢ bᵢ is a unit multiple of g, hence a nonzerodivisor, so aᵢ and bᵢ are; and for x ∈ J₁, x bᵢ ∈ (g) = (aᵢ bᵢ) gives x = r aᵢ by cancelling bᵢ. So J₁ = (aᵢ) with aᵢ a nonzerodivisor on the neighbourhood D(s tᵢ), which is the form of the definition (the fraction aᵢ is a unit multiple of an element of J₁, and tᵢ of an element of A).

Conventions

"Nonzerodivisor" is nonZeroDivisors (multiplication by the element is injective), never ≠ 0: on the zero ring every element is a nonzerodivisor, so the unit ideal and the zero ring are covered without special cases. The condition is existential at each point (a neighbourhood exists), not a condition on every affine open containing the point; the equivalence with the latter is proved in Hironaka.Scheme.BlowUp.InvertibleSheaf.

Boundary cases

Every ideal of the zero ring is invertible (no primes). The unit ideal is invertible (s = 1, a = 1). The zero ideal of a nonzero ring is not: its only element 0 is a nonzerodivisor of A_s only when A_s = 0, i.e. s nilpotent, which s ∉ 𝔭 forbids. On the empty scheme every ideal sheaf is invertible; ⊤ is invertible on every scheme.

Namespace

The predicates extend Mathlib's Ideal, so they live in Mathlib's namespace (dot notation J.IsInvertible), as the invertibility of ideal sheaves lives in IdealSheafData ((I.comap f).IsInvertible).

def Ideal.IsInvertible {A : Type u} [CommRing A] (J : Ideal A) : Prop

An ideal J ⊆ A is invertible (locally principal with a nonzerodivisor generator) if for every prime 𝔭 there are s ∉ 𝔭 and a ∈ J such that J A_s = a A_s and the image of a is a nonzerodivisor of A_s — the local characterisation of [TSPA, Tags 01WR and 01WS] taken as the definition; [Hau14, Definition 4.3].

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.map_mem_nonZeroDivisors_of_ringEquiv {B : Type v} {C : Type w} [CommRing B] [CommRing C] (e : B ≃+* C) {b : B} (hb : b ∈ nonZeroDivisors B) : e b ∈ nonZeroDivisors C

A ring isomorphism preserves nonzerodivisors.

def Ideal.IsRegularGeneratorIn {A : Type u} [CommRing A] (J : Ideal A) (B : Type v) [CommRing B] [Algebra A B] (a : A) : Prop

The local datum of invertibility (the condition on one basic open): a generates the extended ideal J B and is a nonzerodivisor of B.

Equations

• J.IsRegularGeneratorIn B a = (Ideal.map (algebraMap A B) J = Ideal.span {(algebraMap A B) a} ∧ (algebraMap A B) a ∈ nonZeroDivisors B)

theorem Ideal.isInvertible_iff_forall_exists {A : Type u} [CommRing A] (J : Ideal A) : J.IsInvertible ↔ ∀ (p : PrimeSpectrum A), ∃ s ∉ p.asIdeal, ∃ a ∈ J, J.IsRegularGeneratorIn (Localization.Away s) a

theorem Ideal.IsRegularGeneratorIn.of_algEquiv {A : Type u} [CommRing A] {J : Ideal A} {a : A} {B : Type v} {C : Type w} [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (h : J.IsRegularGeneratorIn B a) : J.IsRegularGeneratorIn C a

The datum passes along A-algebra isomorphisms.

theorem Ideal.IsRegularGeneratorIn.of_isLocalization {A : Type u} [CommRing A] {J : Ideal A} {a : A} {B : Type v} {C : Type w} [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (M : Submonoid B) [IsLocalization M C] (h : J.IsRegularGeneratorIn B a) : J.IsRegularGeneratorIn C a

The datum passes to a further localization: if C is a localization of the A-algebra B, the image of a still generates J C and is still a nonzerodivisor.

theorem Ideal.IsRegularGeneratorIn.of_isLocalization_away_mul {A : Type u} [CommRing A] {J : Ideal A} {a s t : A} (h : J.IsRegularGeneratorIn (Localization.Away s) a) (C : Type w) [CommRing C] [Algebra A C] [IsLocalization.Away (s * t) C] : J.IsRegularGeneratorIn C a

The datum in A_s passes to every localization of A away from s * t.

theorem Ideal.isInvertible_top {A : Type u} [CommRing A] : ⊤.IsInvertible

The unit ideal is invertible (s = 1, a = 1).

theorem Ideal.IsInvertible.mul {A : Type u} [CommRing A] {J₁ J₂ : Ideal A} (h₁ : J₁.IsInvertible) (h₂ : J₂.IsInvertible) : (J₁ * J₂).IsInvertible

A product of invertible ideals is invertible: multiply the local generators on the common neighbourhood D(s₁ s₂).

theorem Ideal.IsInvertible.map_away {A : Type u} [CommRing A] {J : Ideal A} (hJ : J.IsInvertible) (s : A) : (map (algebraMap A (Localization.Away s)) J).IsInvertible

Invertibility is stable under localization at an element: a prime of A_s lies over a prime 𝔭 ∌ s of A, and the datum of J at 𝔭 survives in (A_s)_{s'} = A_{s s'}.

theorem Ideal.IsInvertible.of_mul_left {A : Type u} [CommRing A] {J₁ J₂ : Ideal A} (h : (J₁ * J₂).IsInvertible) : J₁.IsInvertible

If J₁ J₂ is invertible then J₁ is: the argument of [Hau14, Theorem 4.18, proof (c)], run on a neighbourhood (see the module docstring).

theorem Ideal.IsInvertible.of_mul {A : Type u} [CommRing A] {J₁ J₂ : Ideal A} (h : (J₁ * J₂).IsInvertible) : J₁.IsInvertible ∧ J₂.IsInvertible

If J₁ J₂ is invertible then J₁ and J₂ are.