Exercise 1.26 (Scott 1981, PRG-19, §1) — ideals of a commutative ring

Scott (for algebraists): let A be a commutative ring with unit and let Δ be the set of finite subsets F ⊆ A. Put

I(F) = {G ∈ Δ ∣ F ⊆ ⟨G⟩} (the ideal generated by G).

Then the sets I(F) form a neighbourhood system and the corresponding domain is isomorphic to the poset (Ideals A, ⊆).

This file formalizes (Δ = Finset A, tokens are finite subsets):

• IFamily F = {G ∣ ↑F ⊆ Ideal.span ↑G} and ringSystem, the neighbourhood system. The master is I(∅) = Δ, and I(F₁) ∩ I(F₂) = I(F₁ ∪ F₂) so the family is closed under all intersections (no consistency hypothesis needed — inter_mem is unconditional).
• idealOf x = {a ∣ I({a}) ∈ x} — a filter's elements collapse to a genuine ideal; conversely ofIdeal J = {I(F) ∣ ↑F ⊆ J}.
• ringIso : |𝒟| ≃o Ideal A — the order isomorphism to (Ideals A, ⊆) (Scott's claim). The token order is reverse (bigger F ⟹ smaller I(F)), but the resulting filter order matches ideal inclusion.

Constructive ([propext, Quot.sound]): the round trips are equational, the only inputs being mathlib's Ideal.span API.

def Domain.Neighborhood.Ring.IFamily {A : Type u_1} [CommRing A] (F : Finset A) : Set (Finset A)

Exercise 1.26 — the basic neighbourhood I(F). I(F) = {G ∣ F ⊆ ⟨G⟩}, the finite sets G whose generated ideal contains F.

Equations

• Domain.Neighborhood.Ring.IFamily F = {G : Finset A | ↑F ⊆ ↑(Ideal.span ↑G)}

@[simp]

theorem Domain.Neighborhood.Ring.mem_IFamily {A : Type u_1} [CommRing A] {F G : Finset A} : G ∈ IFamily F ↔ ↑F ⊆ ↑(Ideal.span ↑G)

theorem Domain.Neighborhood.Ring.IFamily_subset_iff {A : Type u_1} [CommRing A] (F₁ F₂ : Finset A) : IFamily F₁ ⊆ IFamily F₂ ↔ ↑F₂ ⊆ ↑(Ideal.span ↑F₁)

Inclusion of neighbourhoods reversed to ideal generation: I(F₁) ⊆ I(F₂) ↔ F₂ ⊆ ⟨F₁⟩.

theorem Domain.Neighborhood.Ring.span_eq_of_IFamily_eq {A : Type u_1} [CommRing A] {F₁ F₂ : Finset A} (h : IFamily F₁ = IFamily F₂) : Ideal.span ↑F₁ = Ideal.span ↑F₂

theorem Domain.Neighborhood.Ring.IFamily_eq_of_span_eq {A : Type u_1} [CommRing A] {F₁ F₂ : Finset A} (h : Ideal.span ↑F₁ = Ideal.span ↑F₂) : IFamily F₁ = IFamily F₂

theorem Domain.Neighborhood.Ring.IFamily_inter {A : Type u_1} [CommRing A] [DecidableEq A] (F₁ F₂ : Finset A) : IFamily F₁ ∩ IFamily F₂ = IFamily (F₁ ∪ F₂)

I(F₁) ∩ I(F₂) = I(F₁ ∪ F₂): the system is closed under all binary intersections.

def Domain.Neighborhood.Ring.ringSystem {A : Type u_1} [CommRing A] [DecidableEq A] : NeighborhoodSystem (Finset A)

Exercise 1.26 — the neighbourhood system of a commutative ring. Tokens are finite subsets F ⊆ A; neighbourhoods are the sets I(F). The master is I(∅) (all of Δ), and intersections I(F₁) ∩ I(F₂) = I(F₁ ∪ F₂) are always neighbourhoods.

Equations

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

@[simp]

theorem Domain.Neighborhood.Ring.ringSystem_mem {A : Type u_1} [CommRing A] [DecidableEq A] {S : Set (Finset A)} : ringSystem.mem S ↔ ∃ (F : Finset A), S = IFamily F

theorem Domain.Neighborhood.Ring.IFamily_mem {A : Type u_1} [CommRing A] [DecidableEq A] (F : Finset A) : ringSystem.mem (IFamily F)

From filters to ideals.

def Domain.Neighborhood.Ring.idealOf {A : Type u_1} [CommRing A] [DecidableEq A] (x : ringSystem.Element) : Ideal A

Exercise 1.26 — the ideal of a filter. idealOf x = {a ∣ I({a}) ∈ x}. The closure properties of an ideal come from the filter axioms: 0 from the master, + from ∩-closure (I({a}) ∩ I({b}) = I({a,b}) ⊆ I({a+b})), and • from upward closure (I({a}) ⊆ I({c·a})).

Equations

• Domain.Neighborhood.Ring.idealOf x = { carrier := {a : A | x.mem (Domain.Neighborhood.Ring.IFamily {a})}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Domain.Neighborhood.Ring.mem_idealOf {A : Type u_1} [CommRing A] [DecidableEq A] {x : ringSystem.Element} {a : A} : a ∈ idealOf x ↔ x.mem (IFamily {a})

theorem Domain.Neighborhood.Ring.mem_IFamily_of_forall {A : Type u_1} [CommRing A] [DecidableEq A] (x : ringSystem.Element) (F : Finset A) (h : ∀ a ∈ F, x.mem (IFamily {a})) : x.mem (IFamily F)

A filter contains I(F) whenever it contains I({a}) for every a ∈ F (by ∩-closure).

From ideals to filters.

def Domain.Neighborhood.Ring.ofIdeal {A : Type u_1} [CommRing A] [DecidableEq A] (J : Ideal A) : ringSystem.Element

Exercise 1.26 — the filter of an ideal. ofIdeal J = {I(F) ∣ ↑F ⊆ J}.

Equations

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

theorem Domain.Neighborhood.Ring.mem_ofIdeal_IFamily {A : Type u_1} [CommRing A] [DecidableEq A] (J : Ideal A) (F : Finset A) : (ofIdeal J).mem (IFamily F) ↔ Ideal.span ↑F ≤ J

The order isomorphism |𝒟| ≅ (Ideals A, ⊆).

theorem Domain.Neighborhood.Ring.idealOf_ofIdeal {A : Type u_1} [CommRing A] [DecidableEq A] (J : Ideal A) : idealOf (ofIdeal J) = J

theorem Domain.Neighborhood.Ring.ofIdeal_idealOf {A : Type u_1} [CommRing A] [DecidableEq A] (x : ringSystem.Element) : ofIdeal (idealOf x) = x

def Domain.Neighborhood.Ring.ringIso {A : Type u_1} [CommRing A] [DecidableEq A] : ringSystem.Element ≃o Ideal A

Exercise 1.26 — |𝒟| ≅ (Ideals A, ⊆). The domain of the ring's neighbourhood system is order-isomorphic to the ideals of A ordered by inclusion, via x ↦ {a ∣ I({a}) ∈ x}.

Equations

• Domain.Neighborhood.Ring.ringIso = { toFun := Domain.Neighborhood.Ring.idealOf, invFun := Domain.Neighborhood.Ring.ofIdeal, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }