Coherence under isomorphisms and restriction to opens

Coherence of a sheaf of rings ([Fre17, Ch. V, 7.2], in the shape of [Fre17, Ch. I, 10.3]; Hironaka/AnalyticSpace/Coherent.lean) is a statement about sections over opens, their germs and the spans of germs at every point. It is therefore invariant under isomorphisms of locally ringed spaces and local. This file records the three transport lemmas that the proof of isCoherent_analyticSpace (Hironaka/AnalyticSpace/CoherentAnalytic.lean) needs to pass from Oka's theorem on the model (Kⁿ, 𝒜_{Kⁿ}) through a local model to an analytic K-space, which is by definition locally K-isomorphic to an open subspace of a local model:

• isCoherent_of_isIso: an isomorphism φ : X ≅ Y of locally ringed spaces carries coherence of 𝒪_X to coherence of 𝒪_Y — sections are pulled back along the inverse and the stalk maps of the inverse are ring isomorphisms compatible with germs (stalkMap_germ_apply);
• isCoherent_restrict: coherence passes to the open subspace X | U — the sections of X | U over V are the sections of X over the image of V, with the same germs (restrictStalkIso);
• isCoherent_of_forall_restrict: coherence is local — it holds on X when every point has an open neighbourhood U with 𝒪_{X|U} coherent.

The algebraic core is one lemma: a ring isomorphism τ : R ≃+* S carries ker F = span (v) to ker (τ F) = span (τ v) (relKer_eq_span_map); every transport is this lemma applied to the stalk isomorphism at each point with the germ identities of the sections. Routine; not stated in the sources.

theorem Manifold.mem_relKer_map_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (τ : R ≃+* S) {p q : ℕ} (F : Fin q → Fin p → R) (a : Fin p → R) : ((fun (j : Fin p) => τ (a j)) ∈ relKer fun (i : Fin q) (j : Fin p) => τ (F i j)) ↔ a ∈ relKer F

A ring isomorphism carries relations to relations.

theorem Manifold.mem_span_range_map_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (τ : R ≃+* S) {p k : ℕ} (v : Fin k → Fin p → R) (a : Fin p → R) : (fun (j : Fin p) => τ (a j)) ∈ Submodule.span S (Set.range fun (l : Fin k) (j : Fin p) => τ (v l j)) ↔ a ∈ Submodule.span R (Set.range v)

A ring isomorphism carries spans to spans.

theorem Manifold.relKer_eq_span_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (τ : R ≃+* S) {p q k : ℕ} (F : Fin q → Fin p → R) (v : Fin k → Fin p → R) (h : relKer F = Submodule.span R (Set.range v)) : (relKer fun (i : Fin q) (j : Fin p) => τ (F i j)) = Submodule.span S (Set.range fun (l : Fin k) (j : Fin p) => τ (v l j))

The core of every transport: a ring isomorphism carries ker F = span v to ker (τ F) = span (τ v).

theorem Manifold.relationSubmodule_eq_span_of_ringEquiv {X X' : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {𝒪' : TopCat.Sheaf CommRingCat X'} {U V : TopologicalSpace.Opens ↑X} {U' V' : TopologicalSpace.Opens ↑X'} {y : ↑X} {y' : ↑X'} (hy : y ∈ U) (hy' : y' ∈ U') (hyV : y ∈ V) (hyV' : y' ∈ V') (τ : ↑(𝒪.presheaf.stalk y) ≃+* ↑(𝒪'.presheaf.stalk y')) {p q k : ℕ} (F : Fin q → Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) (F' : Fin q → Fin p → ↑(𝒪'.presheaf.obj (Opposite.op U'))) (r : Fin k → Fin p → ↑(𝒪.presheaf.obj (Opposite.op V))) (r' : Fin k → Fin p → ↑(𝒪'.presheaf.obj (Opposite.op V'))) (hF : ∀ (i : Fin q) (j : Fin p), τ ((CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U y hy)) (F i j)) = (CategoryTheory.ConcreteCategory.hom (𝒪'.presheaf.germ U' y' hy')) (F' i j)) (hr : ∀ (l : Fin k) (j : Fin p), τ ((CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V y hyV)) (r l j)) = (CategoryTheory.ConcreteCategory.hom (𝒪'.presheaf.germ V' y' hyV')) (r' l j)) (h : relationSubmodule 𝒪 F y hy = Submodule.span (↑(𝒪.presheaf.stalk y)) (Set.range fun (l : Fin k) (j : Fin p) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V y hyV)) (r l j))) : relationSubmodule 𝒪' F' y' hy' = Submodule.span (↑(𝒪'.presheaf.stalk y')) (Set.range fun (l : Fin k) (j : Fin p) => (CategoryTheory.ConcreteCategory.hom (𝒪'.presheaf.germ V' y' hyV')) (r' l j))

Transport of "the relations of F at y are spanned by the germs of r" along a ring isomorphism of stalks compatible with the germs of F and of r.

theorem AnalyticSpace.isCoherent_of_isIso {X Y : AlgebraicGeometry.LocallyRingedSpace} (φ : X ⟶ Y) [CategoryTheory.IsIso φ] (hX : Manifold.IsCoherent X.𝒪) : Manifold.IsCoherent Y.𝒪

Coherence of the structure sheaf transports along an isomorphism of locally ringed spaces (sections pulled back along the inverse; the stalk maps of the inverse are ring isomorphisms compatible with germs).

theorem AnalyticSpace.functor_obj_map_obj_le (X : AlgebraicGeometry.LocallyRingedSpace) (U W : TopologicalSpace.Opens ↑X.toTopCat) : ⋯.functor.obj ((TopologicalSpace.Opens.map U.inclusion').obj W) ≤ W

The image of the preimage of an open is contained in the open.

theorem AnalyticSpace.isCoherent_restrict (X : AlgebraicGeometry.LocallyRingedSpace) (hX : Manifold.IsCoherent X.𝒪) (U : TopologicalSpace.Opens ↑X.toTopCat) : Manifold.IsCoherent (X.restrict ⋯).𝒪

Coherence of the structure sheaf passes to the open subspaces X | U.

theorem AnalyticSpace.isCoherent_of_forall_restrict (X : AlgebraicGeometry.LocallyRingedSpace) (h : ∀ (x : ↑X.toTopCat), ∃ (U : TopologicalSpace.Opens ↑X.toTopCat), x ∈ U ∧ Manifold.IsCoherent (X.restrict ⋯).𝒪) : Manifold.IsCoherent X.𝒪

Coherence of the structure sheaf is local: it holds when every point has an open neighbourhood U with 𝒪_{X|U} coherent.

theorem AnalyticSpace.KLocallyRingedSpace.isCoherent_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (hX : Manifold.IsCoherent X.𝒪) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Manifold.IsCoherent (X.restrictOpen U).𝒪

Coherence passes to the open subspaces X | U of a K-local-ringed space.

theorem AnalyticSpace.KLocallyRingedSpace.isCoherent_of_kIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (hB : Manifold.IsCoherent B.𝒪) : Manifold.IsCoherent A.𝒪

Coherence transports along a K-isomorphism.

theorem AnalyticSpace.KLocallyRingedSpace.isCoherent_of_forall_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (h : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), x ∈ U ∧ Manifold.IsCoherent (X.restrictOpen U).𝒪) : Manifold.IsCoherent X.𝒪

Coherence of a K-local-ringed space is local.