Generated subsheaves via coproduct images

Generic coproduct-image API used to express subsheaves generated by a family of local sections.

Main definitions

• TopCat.Sheaf.familyMap — the universal map from a family coproduct into a sheaf.
• TopCat.Sheaf.familyImage — the image subsheaf generated by such a family.
• TopCat.Presheaf.SectionIndex — generic indexing type for local sections of a presheaf.
• TopCat.Presheaf.finsetGeneratorMap, TopCat.Presheaf.finsetGeneratedSheaf — finite-section wrappers around the same generated-subsheaf construction.
• TopCat.Presheaf.allSectionMap — the canonical coproduct map from all zeroOutsideInt generators of F, together with its Epi instance.

@[reducible, inline]

noncomputable abbrev TopCat.Sheaf.familyMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} {ι : Type u_2} (G : ι → Sheaf C X) {F : Sheaf C X} (f : (i : ι) → G i ⟶ F) [CategoryTheory.Limits.HasCoproduct G] : ∐ G ⟶ F

For a family of morphisms into F, the universal map from their coproduct into F.

Equations

• TopCat.Sheaf.familyMap G f = CategoryTheory.Limits.Sigma.desc f

@[reducible, inline]

noncomputable abbrev TopCat.Sheaf.familyImage {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} {ι : Type u_2} (G : ι → Sheaf C X) {F : Sheaf C X} (f : (i : ι) → G i ⟶ F) [CategoryTheory.Limits.HasCoproduct G] [CategoryTheory.Limits.HasImage (familyMap G f)] : Sheaf C X

The image subsheaf generated by a family of morphisms into F.

Equations

• TopCat.Sheaf.familyImage G f = CategoryTheory.Limits.image (TopCat.Sheaf.familyMap G f)

@[reducible, inline]

abbrev TopCat.Presheaf.sheafOfIsSheaf {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) : Sheaf AddCommGrpCat X

Regard a topological presheaf equipped with the sheaf condition as a sheaf.

Equations

• TopCat.Presheaf.sheafOfIsSheaf hF = id { obj := F, property := hF }

theorem TopCat.Presheaf.hasImagesTopCatSheaf {X : TopCat} : CategoryTheory.Limits.HasImages (Sheaf AddCommGrpCat X)

theorem TopCat.Presheaf.hasImagesCategoryTheorySheaf {X : TopCat} : CategoryTheory.Limits.HasImages (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)

@[reducible, inline]

abbrev TopCat.Presheaf.SectionIndex {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} (F : Presheaf C X) : Type (max u u_3)

Indexing type for all local sections of a presheaf.

Equations

• F.SectionIndex = ((U : TopologicalSpace.Opens ↑X) × CategoryTheory.ToType (F.obj (Opposite.op U)))

noncomputable def TopCat.Presheaf.sectionHom {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (σ : F.SectionIndex) : Sheaf.zeroOutsideInt σ.fst ⟶ sheafOfIsSheaf hF

The presheaf morphism associated to a section.

Equations

• TopCat.Presheaf.sectionHom hF σ = CategoryTheory.ObjectProperty.homMk (TopCat.Sheaf.zeroOutsideInt.sHomVal hF σ.snd)

@[reducible, inline]

noncomputable abbrev TopCat.Presheaf.finsetGeneratorMap {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (S : Finset F.SectionIndex) [CategoryTheory.Limits.HasCoproduct fun (σ : ↥S) => Sheaf.zeroOutsideInt (↑σ).fst] : (∐ fun (σ : ↥S) => Sheaf.zeroOutsideInt (↑σ).fst) ⟶ sheafOfIsSheaf hF

The canonical map attached to a finite set of local sections.

Equations

• TopCat.Presheaf.finsetGeneratorMap hF S = TopCat.Sheaf.familyMap (fun (σ : ↥S) => TopCat.Sheaf.zeroOutsideInt (↑σ).fst) fun (σ : ↥S) => TopCat.Presheaf.sectionHom hF ↑σ

theorem TopCat.Presheaf.finsetGeneratorMapHasImage {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (S : Finset F.SectionIndex) [CategoryTheory.Limits.HasCoproduct fun (σ : ↥S) => Sheaf.zeroOutsideInt (↑σ).fst] : CategoryTheory.Limits.HasImage (finsetGeneratorMap hF S)

theorem TopCat.Presheaf.finsetGeneratorImageIotaMono {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (S : Finset F.SectionIndex) [CategoryTheory.Limits.HasCoproduct fun (σ : ↥S) => Sheaf.zeroOutsideInt (↑σ).fst] : CategoryTheory.Mono (CategoryTheory.Limits.image.ι (finsetGeneratorMap hF S))

@[reducible, inline]

noncomputable abbrev TopCat.Presheaf.finsetGeneratedSheaf {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (S : Finset F.SectionIndex) [CategoryTheory.Limits.HasCoproduct fun (σ : ↥S) => Sheaf.zeroOutsideInt (↑σ).fst] : Sheaf AddCommGrpCat X

The subsheaf of F generated by a finite set of local sections.

Equations

• TopCat.Presheaf.finsetGeneratedSheaf hF S = TopCat.Sheaf.familyImage (fun (σ : ↥S) => TopCat.Sheaf.zeroOutsideInt (↑σ).fst) fun (σ : ↥S) => TopCat.Presheaf.sectionHom hF ↑σ

noncomputable def TopCat.Presheaf.finsetCoproductInclGen {X : TopCat} {F : Presheaf AddCommGrpCat X} {S S' : Finset F.SectionIndex} (h : S ⊆ S') : (∐ fun (σ : ↥S) => Sheaf.zeroOutsideInt (↑σ).fst) ⟶ ∐ fun (σ : ↥S') => Sheaf.zeroOutsideInt (↑σ).fst

Coproduct inclusion induced by S ⊆ S' on the finite generator coproducts.

Equations

• TopCat.Presheaf.finsetCoproductInclGen h = CategoryTheory.Limits.Sigma.desc fun (σ : ↥S) => CategoryTheory.Limits.Sigma.ι (fun (τ : ↥S') => TopCat.Sheaf.zeroOutsideInt (↑τ).fst) ⟨↑σ, ⋯⟩

noncomputable def TopCat.Presheaf.finsetImageInclGen {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) {S S' : Finset F.SectionIndex} (h : S ⊆ S') : finsetGeneratedSheaf hF S ⟶ finsetGeneratedSheaf hF S'

Inclusion of finitely generated subsheaves induced by S ⊆ S'.

Equations

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

theorem TopCat.Presheaf.finsetImageInclGen_comp_ι {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) {S S' : Finset F.SectionIndex} (h : S ⊆ S') : CategoryTheory.CategoryStruct.comp (finsetImageInclGen hF h) (CategoryTheory.Limits.image.ι (finsetGeneratorMap hF S')) = CategoryTheory.Limits.image.ι (finsetGeneratorMap hF S)

instance TopCat.Presheaf.finsetImageInclGen_mono {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) {S S' : Finset F.SectionIndex} (h : S ⊆ S') : CategoryTheory.Mono (finsetImageInclGen hF h)

@[reducible, inline]

noncomputable abbrev TopCat.Presheaf.allSectionMap {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) [CategoryTheory.Limits.HasCoproduct fun (σ : F.SectionIndex) => Sheaf.zeroOutsideInt σ.fst] : (∐ fun (σ : F.SectionIndex) => Sheaf.zeroOutsideInt σ.fst) ⟶ sheafOfIsSheaf hF

The canonical map from the coproduct of all zeroOutsideInt U indexed by local sections of F onto the sheaf associated to F. This is the formal Step 3A starting point for building finitely generated subsheaves via images of smaller subcoproducts.

Equations

• TopCat.Presheaf.allSectionMap hF = TopCat.Sheaf.familyMap (fun (σ : F.SectionIndex) => TopCat.Sheaf.zeroOutsideInt σ.fst) (TopCat.Presheaf.sectionHom hF)

instance TopCat.Presheaf.allSectionMap_epi {X : TopCat} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) [CategoryTheory.Limits.HasCoproduct fun (σ : F.SectionIndex) => Sheaf.zeroOutsideInt σ.fst] : CategoryTheory.Epi (allSectionMap hF)