Locally finitely generated systems: bookkeeping

Lemmas on the definitions of Hironaka/AnalyticSpace/Coherent.lean, the "obvious" parts of [Fre17, Ch. I, §10] and [Fre17, Ch. V, §7]:

• mem_relationSubmodule_iff: a ∈ ker F_y ↔ ∀ i, Σ_j (F i j)_y * a j = 0, Freitag's F_a;
• restriction of a matrix of sections to a smaller open does not change the relation modules (relationSubmodule_res), and locally finitely generated systems restrict (HasLocalGeneratorsOn.mono) and are local (hasLocalGeneratorsOn_of_forall_exists) [Fre17, Ch. I, 10.2];
• the facts about ⊤: (⊤ : IdealSheaf 𝒪).IsCoherent ↔ ∀ J, J.IsCoherent (IdealSheaf.isCoherent_top_iff; every family of sections is a family of sections of ⊤), and IsCoherent 𝒪 → (⊤).IsCoherent (the q = 1 slice, IsCoherent.isCoherent_top);
• the first step of Oka's theorem [Fre17, Ch. I, 10.3]: coherence of the sheaf of rings follows from the one-row case by induction on the number of rows (isCoherent_of_isCoherent_top), so that 𝒪_X is coherent iff every ideal sheaf of finite type is (isCoherent_iff_forall_isCoherent_idealSheaf, the equivalence recalled in [BM97, (3.8)]).

The bridge between IdealSheaf.HasLocalGenerators (one generator per section, on the whole space) and HasLocalGeneratorsOn with p = 1 is hasLocalGenerators_iff_hasLocalGeneratorsOn_top in Hironaka/AnalyticSpace/CoherentAnalytic.lean.

theorem Manifold.mem_relationSubmodule_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p q : ℕ} (F : Fin q → Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) {y : ↑X} (hy : y ∈ U) (a : Fin p → ↑(𝒪.presheaf.stalk y)) : a ∈ relationSubmodule 𝒪 F y hy ↔ ∀ (i : Fin q), ∑ j : Fin p, (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U y hy)) (F i j) * a j = 0

Freitag's F_a: a is a relation at y iff every row of F vanishes on a at y.

theorem Manifold.relationSubmodule_res {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p q : ℕ} {V : TopologicalSpace.Opens ↑X} (hVU : V ≤ U) (F : Fin q → Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) {y : ↑X} (hy : y ∈ V) : relationSubmodule 𝒪 (fun (i : Fin q) (j : Fin p) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map (CategoryTheory.homOfLE hVU).op)) (F i j)) y hy = relationSubmodule 𝒪 F y ⋯

Restricting the matrix of sections to a smaller open does not change the relation module at a point of the smaller open.

theorem Manifold.HasLocalGeneratorsOn.mono {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} {M : (y : ↑X) → y ∈ U → Submodule (↑(𝒪.presheaf.stalk y)) (Fin p → ↑(𝒪.presheaf.stalk y))} (h : HasLocalGeneratorsOn 𝒪 U p M) {V : TopologicalSpace.Opens ↑X} (hVU : V ≤ U) : HasLocalGeneratorsOn 𝒪 V p fun (y : ↑X) (hy : y ∈ V) => M y ⋯

Local finite generation restricts to smaller opens [Fre17, Ch. I, 10.2].

theorem Manifold.hasLocalGeneratorsOn_of_forall_exists {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} {M : (y : ↑X) → y ∈ U → Submodule (↑(𝒪.presheaf.stalk y)) (Fin p → ↑(𝒪.presheaf.stalk y))} (h : ∀ x ∈ U, ∃ (V : TopologicalSpace.Opens ↑X) (hVU : V ≤ U), x ∈ V ∧ HasLocalGeneratorsOn 𝒪 V p fun (y : ↑X) (hy : y ∈ V) => M y ⋯) : HasLocalGeneratorsOn 𝒪 U p M

A system is locally finitely generated on U if every point of U has a neighbourhood in U on which it is [Fre17, Ch. I, 10.2].

theorem Manifold.HasLocalGeneratorsOn.congr {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} {M N : (y : ↑X) → y ∈ U → Submodule (↑(𝒪.presheaf.stalk y)) (Fin p → ↑(𝒪.presheaf.stalk y))} (h : HasLocalGeneratorsOn 𝒪 U p M) (hMN : ∀ (y : ↑X) (hy : y ∈ U), M y hy = N y hy) : HasLocalGeneratorsOn 𝒪 U p N

Local finite generation is invariant under a stalkwise equality of systems.

theorem Manifold.IdealSheaf.isCoherent_top_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : ⊤.IsCoherent ↔ ∀ (J : IdealSheaf 𝒪), J.IsCoherent

(⊤ : IdealSheaf 𝒪).IsCoherent ↔ ∀ J, J.IsCoherent: every finite family of sections is a family of sections of ⊤ ([BM97, (3.8)], "every ideal of finite type in 𝒪_X is coherent").

theorem Manifold.IsCoherent.isCoherent_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (h : IsCoherent 𝒪) : ⊤.IsCoherent

The q = 1 slice of coherence of the sheaf of rings: ⊤ is a coherent ideal sheaf.

theorem Manifold.relKer_of_isEmpty {R : Type u_1} [CommRing R] {p q : ℕ} [IsEmpty (Fin q)] (F : Fin q → Fin p → R) : relKer F = ⊤

theorem Manifold.span_range_single_one_eq_top {R : Type u_1} [CommRing R] (p : ℕ) : Submodule.span R (Set.range fun (l : Fin p) => Pi.single l 1) = ⊤

The unit vectors span Fin p → R.

theorem Manifold.sum_mul_sum_swap {R : Type u_1} [CommRing R] {p k : ℕ} (f : Fin p → R) (g : Fin k → Fin p → R) (c : Fin k → R) : ∑ j : Fin p, f j * ∑ l : Fin k, c l * g l j = ∑ l : Fin k, (∑ j : Fin p, f j * g l j) * c l

Swapping a double sum with the coefficients pulled through.

theorem Manifold.sum_mul_sum_swap' {R : Type u_1} [CommRing R] {p k : ℕ} (f : Fin p → R) (g : Fin k → Fin p → R) (c : Fin k → R) : ∑ j : Fin p, f j * ∑ l : Fin k, c l * g l j = ∑ l : Fin k, c l * ∑ j : Fin p, f j * g l j

theorem Manifold.relKer_succ_eq_span {R : Type u_1} [CommRing R] {p q k m : ℕ} (F : Fin (q + 1) → Fin p → R) (A : Fin k → Fin p → R) (B : Fin m → Fin k → R) (hA : (relKer fun (i : Fin q) => F i.succ) = Submodule.span R (Set.range A)) (hB : (relKer fun (x : Fin 1) (l : Fin k) => ∑ j : Fin p, F 0 j * A l j) = Submodule.span R (Set.range B)) : relKer F = Submodule.span R (Set.range fun (i : Fin m) (j : Fin p) => ∑ l : Fin k, B i l * A l j)

The first step of Oka's theorem [Fre17, Ch. I, 10.3], the algebra at one ring: if the relations of the last q rows of F are generated by A, and the relations of the row l ↦ Σ_j F 0 j · A l j are generated by B, then the relations of F are generated by C i j = Σ_l B i l · A l j.

theorem Manifold.isCoherent_of_isCoherent_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (h : ⊤.IsCoherent) : IsCoherent 𝒪

The first step of Oka's theorem [Fre17, Ch. I, 10.3]: coherence of the sheaf of rings follows from the case of one row ((⊤ : IdealSheaf 𝒪).IsCoherent), by induction on the number of rows.

theorem Manifold.isCoherent_iff_forall_isCoherent_idealSheaf {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : IsCoherent 𝒪 ↔ ∀ (J : IdealSheaf 𝒪), J.IsCoherent

A sheaf of rings 𝒪_X is coherent iff every ideal of finite type in 𝒪_X is coherent ([BM97, (3.8)], recalled there for the structure sheaf of a space), for any sheaf of commutative rings on any space: → is the q = 1 slice through ⊤, ← is Freitag's first step.