Stalk maps of a morphism into an open subspace

For l : A ⟶ B|V with l ≫ ofRestrict B V = g, the stalk map of l at x is conjugate to the stalk map of g at x by the stalk isomorphism of the open immersion B|V ⟶ B (Mathlib's restrictStalkIso) and the identification of the stalks of B at the two (equal) base points (stalkMap_ofRestrict_comp_stalkMap_of_comp_eq, stalkMap_apply_stalkMap_ofRestrict_of_comp_eq). Hence l and g have bijective, respectively surjective, stalk maps at the same points (bijective_stalkMap_iff_of_comp_eq, surjective_stalkMap_iff_of_comp_eq), and the germ of a section of B on V, read in B|V, is sent by the stalk map of l to what the stalk map of g does to its germ in B (stalkMap_germ_of_comp_eq, stalkMap_germ_top_of_comp_eq). The same conjugation for a factorization ρ ≫ h' = g₀ through a morphism ρ with bijective stalk map at x (stalkMap_apply_stalkMap_of_comp_eq, surjective_stalkMap_of_comp_eq_of_bijective, stalkMap_eq_zero_iff_of_comp_eq_of_bijective: the stalk map of h' at ρ x is surjective when that of g₀ is, and its kernel is read off from that of g₀), and the algebra behind it: the stalk map of a specialization along an equality of points is bijective (bijective_stalkSpecializes_of_eq), a bijective ring homomorphism preserves membership in spans (mem_span_range_iff_of_bijective), and the stalk maps of an isomorphism are bijective (bijective_stalkMap_of_isIso). Used by Hironaka/AnalyticSpace/RestrictToIso.lean. Routine.

theorem AnalyticSpace.bijective_stalkSpecializes_of_eq {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {p q : ↑X} (hpq : p = q) : Function.Bijective ⇑(CommRingCat.Hom.hom (F.stalkSpecializes ⋯))

The stalk specialization map between the stalks at two equal points is bijective.

theorem AnalyticSpace.KLocallyRingedSpace.bijective_stalkMap_of_isIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (φ : A ⟶ B) [CategoryTheory.IsIso φ] (x : ↑↑A.toPresheafedSpace) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑φ) x))

The stalk maps of an isomorphism are bijective. Duplicates KIso.bijective_stalkMap of Hironaka/AnalyticSpace/StalkMapLemmas.lean in the [IsIso φ] form.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_ofRestrict_comp_stalkMap_of_comp_eq {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (l : A ⟶ B.restrictOpen V) (g : A ⟶ B) (hl : CategoryTheory.CategoryStruct.comp l (B.ofRestrict V) = g) (x : ↑↑A.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(B.ofRestrict V)) ((CategoryTheory.ConcreteCategory.hom (↑l).base) x)) (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x) = CategoryTheory.CategoryStruct.comp (B.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) x)

For l ≫ ofRestrict B V = g: the stalk map of the open immersion followed by the stalk map of l is the identification of the stalks at the equal base points followed by the stalk map of g.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_apply_stalkMap_of_comp_eq {K : Type} [RCLike K] {A B C : KLocallyRingedSpace K} (ρ : A ⟶ B) (h' : B ⟶ C) (g₀ : A ⟶ C) (hρ : CategoryTheory.CategoryStruct.comp ρ h' = g₀) (x : ↑↑A.toPresheafedSpace) (a : ↑(C.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑h').base) ((CategoryTheory.ConcreteCategory.hom (↑ρ).base) x)))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑ρ) x)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑h') ((CategoryTheory.ConcreteCategory.hom (↑ρ).base) x))) a) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g₀) x)) ((CategoryTheory.ConcreteCategory.hom (C.presheaf.stalkSpecializes ⋯)) a)

For ρ ≫ h' = g₀: the stalk map of ρ after the stalk map of h' at ρ x is the stalk map of g₀ after the identification of the stalks at the equal base points (function form).

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_apply_stalkMap_ofRestrict_of_comp_eq {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (l : A ⟶ B.restrictOpen V) (g : A ⟶ B) (hl : CategoryTheory.CategoryStruct.comp l (B.ofRestrict V) = g) (x : ↑↑A.toPresheafedSpace) (γ : ↑(B.presheaf.stalk ↑((CategoryTheory.ConcreteCategory.hom (↑l).base) x))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(B.ofRestrict V)) ((CategoryTheory.ConcreteCategory.hom (↑l).base) x))) γ) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) x)) ((CategoryTheory.ConcreteCategory.hom (B.presheaf.stalkSpecializes ⋯)) γ)

The function form of stalkMap_ofRestrict_comp_stalkMap_of_comp_eq.

theorem AnalyticSpace.KLocallyRingedSpace.surjective_stalkMap_of_comp_eq_of_bijective {K : Type} [RCLike K] {A B C : KLocallyRingedSpace K} (ρ : A ⟶ B) (h' : B ⟶ C) (g₀ : A ⟶ C) (hρ : CategoryTheory.CategoryStruct.comp ρ h' = g₀) (x : ↑↑A.toPresheafedSpace) (hb : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑ρ) x))) (hs : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g₀) x))) : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑h') ((CategoryTheory.ConcreteCategory.hom (↑ρ).base) x)))

For ρ ≫ h' = g₀ with bijective stalk maps of ρ: the stalk map of h' at ρ x is surjective when that of g₀ at x is.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_eq_zero_iff_of_comp_eq_of_bijective {K : Type} [RCLike K] {A B C : KLocallyRingedSpace K} (ρ : A ⟶ B) (h' : B ⟶ C) (g₀ : A ⟶ C) (hρ : CategoryTheory.CategoryStruct.comp ρ h' = g₀) (x : ↑↑A.toPresheafedSpace) (hb : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑ρ) x))) (a : ↑(C.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑h').base) ((CategoryTheory.ConcreteCategory.hom (↑ρ).base) x)))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑h') ((CategoryTheory.ConcreteCategory.hom (↑ρ).base) x))) a = 0 ↔ (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g₀) x)) ((CategoryTheory.ConcreteCategory.hom (C.presheaf.stalkSpecializes ⋯)) a) = 0

For ρ ≫ h' = g₀ with bijective stalk maps of ρ: a is in the kernel of the stalk map of h' at ρ x iff its transport is in the kernel of the stalk map of g₀ at x.

theorem AnalyticSpace.mem_span_range_iff_of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (Φ : R →+* S) (hΦ : Function.Bijective ⇑Φ) {ι : Type u_3} (v : ι → R) (a : R) : Φ a ∈ Ideal.span (Set.range fun (i : ι) => Φ (v i)) ↔ a ∈ Ideal.span (Set.range v)

An element is in the ideal generated by a family iff its image under a bijective ring homomorphism is in the ideal generated by the images.

theorem AnalyticSpace.KLocallyRingedSpace.bijective_stalkMap_iff_of_comp_eq {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (l : A ⟶ B.restrictOpen V) (g : A ⟶ B) (hl : CategoryTheory.CategoryStruct.comp l (B.ofRestrict V) = g) (x : ↑↑A.toPresheafedSpace) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x)) ↔ Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) x))

The stalk map of l : A ⟶ B|V is bijective exactly when that of g = l ≫ ofRestrict B V is.

theorem AnalyticSpace.KLocallyRingedSpace.surjective_stalkMap_iff_of_comp_eq {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (l : A ⟶ B.restrictOpen V) (g : A ⟶ B) (hl : CategoryTheory.CategoryStruct.comp l (B.ofRestrict V) = g) (x : ↑↑A.toPresheafedSpace) : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x)) ↔ Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) x))

The stalk map of l : A ⟶ B|V is surjective exactly when that of g = l ≫ ofRestrict B V is.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_germ_of_comp_eq {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (l : A ⟶ B.restrictOpen V) (g : A ⟶ B) (hl : CategoryTheory.CategoryStruct.comp l (B.ofRestrict V) = g) (x : ↑↑A.toPresheafedSpace) (T : TopologicalSpace.Opens ↑↑(B.restrictOpen V).toPresheafedSpace) (hT : (CategoryTheory.ConcreteCategory.hom (↑l).base) x ∈ T) (τ : ↑(B.presheaf.obj (Opposite.op (B.imgOpens V T)))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x)) ((CategoryTheory.ConcreteCategory.hom ((B.restrictOpen V).presheaf.germ T ((CategoryTheory.ConcreteCategory.hom (↑l).base) x) hT)) τ) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) x)) ((CategoryTheory.ConcreteCategory.hom (B.presheaf.germ (B.imgOpens V T) (Hom.toFun g x) ⋯)) τ)

The stalk map of l : A ⟶ B|V on the germ of a section τ of B|V on T (a section of B on the image of T) is the stalk map of g = l ≫ ofRestrict B V on the germ of τ in B.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_germ_top_of_comp_eq {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} {V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace} (l : A ⟶ B.restrictOpen V) (g : A ⟶ B) (hl : CategoryTheory.CategoryStruct.comp l (B.ofRestrict V) = g) (x : ↑↑A.toPresheafedSpace) (τ : ↑(B.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x)) ((CategoryTheory.ConcreteCategory.hom ((B.restrictOpen V).presheaf.germ ⊤ ((CategoryTheory.ConcreteCategory.hom (↑l).base) x) trivial)) ((CategoryTheory.ConcreteCategory.hom (B.presheaf.map (CategoryTheory.homOfLE ⋯).op)) τ)) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) x)) ((CategoryTheory.ConcreteCategory.hom (B.presheaf.germ V (Hom.toFun g x) ⋯)) τ)

stalkMap_germ_of_comp_eq for a section of B on V read as a global section of B|V.