Gluing K-morphisms into (Kⁿ, 𝒜_{Kⁿ}) along an open cover

A K-local-ringed space Z covered by opens U i, with K-morphisms h i : Z|U i ⟶ (Kⁿ, 𝒜_{Kⁿ}) that agree on the overlaps — the same base point, and the same germ of the pullback of every function of 𝒜_{Kⁿ} at every point of U i ∩ U j — has a K-morphism Z ⟶ (Kⁿ, 𝒜_{Kⁿ}) (glueHomAffine) which agrees with h i on U i in the same two senses: on base points (toFun_glueHomAffine_eq) and on the germs of pulled-back sections (germ_pullbackΓ_glueHomAffine); the equation ofRestrict Z (U i) ≫ glueHomAffine … = h i itself is not proved here. The agreement hypotheses are stated on germs, so that everything is decided by TopCat.Presheaf.section_ext and the sheaf property of 𝒪_Z; in the application (a morphism X ⟶ (Kⁿ, 𝒜_{Kⁿ}) of an analytic K-space from n global sections, Hironaka/AnalyticSpace/HomOfSections.lean) the agreement comes from the uniqueness ringHom_ext_of_coord on the stalks. This is the gluing step in the construction of Hironaka's extended coordination h' [Hir64, Ch. 0, §1, p. 120]. Elementary sheaf theory; not in the sources.

Construction. The base map is z ↦ (h i).base z for any i with z ∈ U i (well defined and continuous because it is so on each U i). For an open V ⊆ Kⁿ and F ∈ 𝒜(V), the sections (h i)^*F over U i ∩ b⁻¹(V) are compatible (equal germs, hence equal by section_ext), and glue to a section over b⁻¹(V) (existsUnique_gluing'); uniqueness of the gluing gives the naturality and the ring-homomorphism axioms of the sheaf map. The stalk map at z ∈ U i is the stalk map of h i (through the isomorphism of the stalk of Z|U i with that of Z), hence local, and the constants pull back to constants because they do so for each h i.

The image of an open of an open subspace

@[reducible, inline]

abbrev AnalyticSpace.KLocallyRingedSpace.imgOpens {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (V : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (T : TopologicalSpace.Opens ↑↑(Z.restrictOpen V).toPresheafedSpace) : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace

The image in Z of an open T of the open subspace Z|V: the functor of the open embedding V → Z. Sections of 𝒪_{Z|V} over T are, by definition of the restriction, sections of 𝒪_Z over imgOpens Z V T.

Equations

• Z.imgOpens V T = ⋯.functor.obj T

theorem AnalyticSpace.KLocallyRingedSpace.mem_imgOpens {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) {V : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} {T : TopologicalSpace.Opens ↑↑(Z.restrictOpen V).toPresheafedSpace} {z : ↑↑Z.toPresheafedSpace} : z ∈ Z.imgOpens V T ↔ ∃ (hz : z ∈ V), ⟨z, hz⟩ ∈ T

theorem AnalyticSpace.KLocallyRingedSpace.mem_imgOpens_of_mem {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) {V : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace} {T : TopologicalSpace.Opens ↑↑(Z.restrictOpen V).toPresheafedSpace} {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ V) (hT : ⟨z, hz⟩ ∈ T) : z ∈ Z.imgOpens V T

theorem AnalyticSpace.KLocallyRingedSpace.imgOpens_top_le {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) : Z.imgOpens W ⊤ ≤ W

The image of the whole open subspace Z|W is contained in W.

The glued base map

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueIdx {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (z : ↑↑Z.toPresheafedSpace) : ι

An index of the cover containing z.

Equations

• Z.glueIdx U hU z = ⋯.choose

theorem AnalyticSpace.KLocallyRingedSpace.mem_glueIdx {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (z : ↑↑Z.toPresheafedSpace) : z ∈ U (Z.glueIdx U hU z)

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueBase {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (z : ↑↑Z.toPresheafedSpace) : Kn K n

The glued base map z ↦ (h i).base z, z ∈ U i.

Equations

• Z.glueBase U hU h z = (CategoryTheory.ConcreteCategory.hom (↑(h (Z.glueIdx U hU z))).base) ⟨z, ⋯⟩

theorem AnalyticSpace.KLocallyRingedSpace.glueBase_eq {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (i : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) : Z.glueBase U hU h z = (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩

theorem AnalyticSpace.KLocallyRingedSpace.continuous_glueBase {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) : Continuous (Z.glueBase U hU h)

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueBaseHom {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) : Z.toTopCat ⟶ (affine K n).toTopCat

The glued base map as a morphism of TopCat.

Equations

• Z.glueBaseHom U hU h hbase = TopCat.ofHom { toFun := Z.glueBase U hU h, continuous_toFun := ⋯ }

theorem AnalyticSpace.KLocallyRingedSpace.glueBaseHom_apply {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (z : ↑↑Z.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (Z.glueBaseHom U hU h hbase)) z = Z.glueBase U hU h z

The glued sections

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.preV {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (V : TopologicalSpace.Opens (Kn K n)) : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace

The preimage of V ⊆ Kⁿ under the glued base map.

Equations

• Z.preV U hU h hbase V = (TopologicalSpace.Opens.map (Z.glueBaseHom U hU h hbase)).obj V

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.locV {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (i : ι) (V : TopologicalSpace.Opens (Kn K n)) : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace

The piece U i ∩ b⁻¹(V) of the preimage, as the image of the preimage of V under h i.

Equations

• Z.locV U h i V = Z.imgOpens (U i) ((TopologicalSpace.Opens.map (↑(h i)).base).obj V)

theorem AnalyticSpace.KLocallyRingedSpace.mem_locV {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) {i : ι} {V : TopologicalSpace.Opens (Kn K n)} {z : ↑↑Z.toPresheafedSpace} : z ∈ Z.locV U h i V ↔ ∃ (hi : z ∈ U i), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ ∈ V

theorem AnalyticSpace.KLocallyRingedSpace.locV_le_preV {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (i : ι) (V : TopologicalSpace.Opens (Kn K n)) : Z.locV U h i V ≤ Z.preV U hU h hbase V

theorem AnalyticSpace.KLocallyRingedSpace.preV_le_iSup {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (V : TopologicalSpace.Opens (Kn K n)) : Z.preV U hU h hbase V ≤ ⨆ (i : ι), Z.locV U h i V

theorem AnalyticSpace.KLocallyRingedSpace.mem_locV_of_mem_preV {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) {V : TopologicalSpace.Opens (Kn K n)} {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ Z.preV U hU h hbase V) {i : ι} (hi : z ∈ U i) : z ∈ Z.locV U h i V

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.locSec {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (i : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : ↑(Z.presheaf.obj (Opposite.op (Z.locV U h i V)))

The pullback of F ∈ 𝒜(V) along h i, as a section of 𝒪_Z over U i ∩ b⁻¹(V).

Equations

• Z.locSec U h i V F = (CategoryTheory.ConcreteCategory.hom ((↑(h i)).c.app (Opposite.op V))) F

theorem AnalyticSpace.KLocallyRingedSpace.isCompatible_locSec {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : Z.presheaf.IsCompatible (fun (i : ι) => Z.locV U h i V) fun (i : ι) => Z.locSec U h i V F

theorem AnalyticSpace.KLocallyRingedSpace.existsUnique_glueSec {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : ∃! t : ↑(Z.presheaf.obj (Opposite.op (Z.preV U hU h hbase V))), ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.map (CategoryTheory.homOfLE ⋯).op)) t = Z.locSec U h i V F

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueSec {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : ↑(Z.presheaf.obj (Opposite.op (Z.preV U hU h hbase V)))

The glued pullback of F ∈ 𝒜(V): the section of 𝒪_Z over b⁻¹(V) restricting to (h i)^*F on every U i ∩ b⁻¹(V).

Equations

• Z.glueSec U hU h hbase hgerm V F = ⋯.choose

theorem AnalyticSpace.KLocallyRingedSpace.glueSec_res {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (i : ι) : (CategoryTheory.ConcreteCategory.hom (Z.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (Z.glueSec U hU h hbase hgerm V F) = Z.locSec U h i V F

theorem AnalyticSpace.KLocallyRingedSpace.glueSec_unique {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (t : ↑(Z.presheaf.obj (Opposite.op (Z.preV U hU h hbase V)))) (ht : ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.map (CategoryTheory.homOfLE ⋯).op)) t = Z.locSec U h i V F) : t = Z.glueSec U hU h hbase hgerm V F

theorem AnalyticSpace.KLocallyRingedSpace.germ_glueSec {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ Z.preV U hU h hbase V) {i : ι} (hi : z ∈ U i) : (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.preV U hU h hbase V) z hz)) (Z.glueSec U hU h hbase hgerm V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z ⋯)) (Z.locSec U h i V F)

The germ of the glued section at z ∈ U i is the germ of (h i)^*F.

theorem AnalyticSpace.KLocallyRingedSpace.eq_glueSec_of_germ {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (t : ↑(Z.presheaf.obj (Opposite.op (Z.preV U hU h hbase V)))) (ht : ∀ (z : ↑↑Z.toPresheafedSpace) (hz : z ∈ Z.preV U hU h hbase V) (i : ι) (hi : z ∈ U i), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.preV U hU h hbase V) z hz)) t = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z ⋯)) (Z.locSec U h i V F)) : t = Z.glueSec U hU h hbase hgerm V F

Two sections over b⁻¹(V) with the same germs as the local pullbacks are equal: the uniqueness in existsUnique_glueSec, at the level of germs.

The glued sheaf map

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueCApp {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) : ↑((affine K n).presheaf.obj (Opposite.op V)) →+* ↑(Z.presheaf.obj (Opposite.op (Z.preV U hU h hbase V)))

The component at V of the glued sheaf map, as a ring homomorphism F ↦ glueSec F.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.glueCApp_apply {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : (Z.glueCApp U hU h hbase hgerm V) F = Z.glueSec U hU h hbase hgerm V F

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueC {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) : (affine K n).presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat (Z.glueBaseHom U hU h hbase)).obj Z.presheaf

The sheaf map 𝒜_{Kⁿ} ⟶ b_* 𝒪_Z of the glued morphism: F ↦ glueSec F.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.glueC_app_apply {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom ((Z.glueC U hU h hbase hgerm).app (Opposite.op V))) F = Z.glueSec U hU h hbase hgerm V F

The glued morphism

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueAux {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) : Z.toPresheafedSpace ⟶ (affine K n).toPresheafedSpace

The glued morphism of presheafed spaces.

Equations

• Z.glueAux U hU h hbase hgerm = { base := Z.glueBaseHom U hU h hbase, c := Z.glueC U hU h hbase hgerm }

theorem AnalyticSpace.KLocallyRingedSpace.glueAux_base_apply {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (z : ↑↑Z.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (Z.glueAux U hU h hbase hgerm).base) z = Z.glueBase U hU h z

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_glueAux_germ {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (V : TopologicalSpace.Opens (Kn K n)) {z : ↑↑Z.toPresheafedSpace} (hz : (CategoryTheory.ConcreteCategory.hom (Z.glueAux U hU h hbase hgerm).base) z ∈ V) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) {i : ι} (hi : z ∈ U i) : (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (Z.glueAux U hU h hbase hgerm) z)) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ V ((CategoryTheory.ConcreteCategory.hom (Z.glueAux U hU h hbase hgerm).base) z) hz)) F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z ⋯)) (Z.locSec U h i V F)

The stalk map of the glued morphism on a germ: the germ of the local pullback (h i)^*F.

theorem AnalyticSpace.KLocallyRingedSpace.restrictStalkIso_inv_germ {K : Type} [RCLike K] (Z : KLocallyRingedSpace K) (W : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (T : TopologicalSpace.Opens ↑↑(Z.restrictOpen W).toPresheafedSpace) {z : ↑↑Z.toPresheafedSpace} (hz : z ∈ W) (hT : ⟨z, hz⟩ ∈ T) (s : ↑(Z.presheaf.obj (Opposite.op (Z.imgOpens W T)))) : (CommRingCat.Hom.hom (Z.restrictStalkIso ⋯ ⟨z, hz⟩).inv) ((CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.imgOpens W T) z ⋯)) s) = (CategoryTheory.ConcreteCategory.hom ((Z.restrictOpen W).presheaf.germ T ⟨z, hz⟩ hT)) s

The isomorphism of the stalk of Z at z ∈ W with the stalk of Z|W on a germ: a section of 𝒪_Z over the image of an open T of Z|W is a section of 𝒪_{Z|W} over T, with the corresponding germ (Mathlib's restrictStalkIso_inv_eq_germ).

theorem AnalyticSpace.KLocallyRingedSpace.isLocalHom_stalkMap_glueAux {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (z : ↑↑Z.toPresheafedSpace) : IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (Z.glueAux U hU h hbase hgerm) z))

The stalk maps of the glued morphism are local: a germ whose glued pullback is a unit has a nonzero value, because the pullback along h i is a unit and h i is a K-morphism.

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueHomAffine {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) : Z ⟶ affine K n

The glued K-morphism Z ⟶ (Kⁿ, 𝒜_{Kⁿ}) of compatible morphisms h i on an open cover of Z.

Equations

• Z.glueHomAffine U hU h hbase hgerm = ⟨{ toHom := Z.glueAux U hU h hbase hgerm, prop := ⋯ }, ⋯⟩

theorem AnalyticSpace.KLocallyRingedSpace.toFun_glueHomAffine {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (z : ↑↑Z.toPresheafedSpace) : Hom.toFun (Z.glueHomAffine U hU h hbase hgerm) z = Z.glueBase U hU h z

theorem AnalyticSpace.KLocallyRingedSpace.toFun_glueHomAffine_eq {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) {i : ι} (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) : Hom.toFun (Z.glueHomAffine U hU h hbase hgerm) z = (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩

theorem AnalyticSpace.KLocallyRingedSpace.germ_pullbackΓ_glueHomAffine {K : Type} [RCLike K] {n : ℕ} (Z : KLocallyRingedSpace K) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hU : ∀ (z : ↑↑Z.toPresheafedSpace), ∃ (i : ι), z ∈ U i) (h : (i : ι) → Z.restrictOpen (U i) ⟶ affine K n) (hbase : ∀ (i j : ι) (z : ↑↑Z.toPresheafedSpace) (hi : z ∈ U i) (hj : z ∈ U j), (CategoryTheory.ConcreteCategory.hom (↑(h i)).base) ⟨z, hi⟩ = (CategoryTheory.ConcreteCategory.hom (↑(h j)).base) ⟨z, hj⟩) (hgerm : ∀ (i j : ι) (V : TopologicalSpace.Opens (Kn K n)) (F : ↑((affine K n).presheaf.obj (Opposite.op V))) (z : ↑↑Z.toPresheafedSpace) (hzi : z ∈ Z.locV U h i V) (hzj : z ∈ Z.locV U h j V), (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i V) z hzi)) (Z.locSec U h i V F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h j V) z hzj)) (Z.locSec U h j V F)) (F : ↑((affine K n).presheaf.obj (Opposite.op ⊤))) (z : ↑↑Z.toPresheafedSpace) {i : ι} (hi : z ∈ U i) : (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ ⊤ z ⋯)) ((Hom.pullbackΓ (Z.glueHomAffine U hU h hbase hgerm)) F) = (CategoryTheory.ConcreteCategory.hom (Z.presheaf.germ (Z.locV U h i ⊤) z ⋯)) ((Hom.pullbackΓ (h i)) F)

The germ at z ∈ U i of the pullback of a global section of 𝒜_{Kⁿ} along the glued morphism is the germ of its pullback along h i.