Transporting generating sections #
This file provides a general transport for generating sections: first carry them along a colimit-preserving functor, then read them through an isomorphism of the resulting sheaf. The transport preserves the indexing type, invertibility of the generating morphism, and finiteness.
It also records what it means, sectionwise, for finitely many sections to generate: every section is, locally on a covering sieve, a linear combination of the restricted generators. This is the form in which generators are used to compute stalks.
The iterated-slice specialization provides the transport used to combine local bases over a refinement. It is adapted from Brian Nugent's implementation.
Main declarations #
SheafOfModules.GeneratingSections.equivOfIso_apply_π: the generating morphism after transport along an isomorphism;SheafOfModules.GeneratingSections.mapIso: generating sections carried along a colimit-preserving functor and read through an isomorphism;SheafOfModules.GeneratingSections.restrict: generating sections restricted along an arrow;SheafOfModules.GeneratingSections.ofIteratedSlice: generating sections on an iterated slice, read as generating sections on the slice over the underlying object;SheafOfModules.GeneratingSections.exists_sieve_sum_smul_eq: finitely many generating sections generate every section locally.
@[simp]
theorem
SheafOfModules.GeneratingSections.equivOfIso_apply_I
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{M N : SheafOfModules R}
(e : M ≅ N)
(σ : M.GeneratingSections)
:
Transporting generating sections along an isomorphism preserves their index type.
@[simp]
theorem
SheafOfModules.GeneratingSections.equivOfIso_apply_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{M N : SheafOfModules R}
(e : M ≅ N)
(σ : M.GeneratingSections)
:
Transporting generating sections along an isomorphism e composes the generating morphism
with e.
instance
SheafOfModules.GeneratingSections.isIso_equivOfIso_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{M N : SheafOfModules R}
(e : M ≅ N)
(σ : M.GeneratingSections)
[hσ : CategoryTheory.IsIso σ.π]
:
CategoryTheory.IsIso ((equivOfIso e) σ).π
Transporting generating sections along an isomorphism preserves an invertible generating morphism.
instance
SheafOfModules.GeneratingSections.isFiniteType_equivOfIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{M N : SheafOfModules R}
(e : M ≅ N)
(σ : M.GeneratingSections)
[hσ : σ.IsFiniteType]
:
((equivOfIso e) σ).IsFiniteType
Transporting generating sections along an isomorphism preserves finiteness.
noncomputable def
SheafOfModules.GeneratingSections.mapIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
{S : CategoryTheory.Sheaf K RingCat}
[CategoryTheory.HasSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{N : SheafOfModules S}
(σ : M.GeneratingSections)
(F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
[CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
max (max (u + 1) u₂) v₂}
F]
(η : unit S ≅ F.obj (unit R))
(e : F.obj M ≅ N)
:
Generating sections carried along a colimit-preserving functor F and then read through an
isomorphism e : F.obj M ≅ N.
Equations
- σ.mapIso F η e = (SheafOfModules.GeneratingSections.equivOfIso e) (σ.map F η)
Instances For
@[simp]
theorem
SheafOfModules.GeneratingSections.mapIso_I
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
{S : CategoryTheory.Sheaf K RingCat}
[CategoryTheory.HasSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{N : SheafOfModules S}
(σ : M.GeneratingSections)
(F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
[CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
max (max (u + 1) u₂) v₂}
F]
(η : unit S ≅ F.obj (unit R))
(e : F.obj M ≅ N)
:
Carrying generating sections along a functor and an isomorphism preserves their index type.
@[simp]
theorem
SheafOfModules.GeneratingSections.mapIso_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
{S : CategoryTheory.Sheaf K RingCat}
[CategoryTheory.HasSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{N : SheafOfModules S}
(σ : M.GeneratingSections)
(F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
[CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
max (max (u + 1) u₂) v₂}
F]
(η : unit S ≅ F.obj (unit R))
(e : F.obj M ≅ N)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (σ.mapIso F η e).π = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (mapFreeIso F σ.I η).hom (F.map σ.π)) e.hom
The generating morphism of carried generating sections is the mapped generating morphism
followed by the isomorphism, read along the identification mapIso_I of the index types.
instance
SheafOfModules.GeneratingSections.isIso_mapIso_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
{S : CategoryTheory.Sheaf K RingCat}
[CategoryTheory.HasSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{N : SheafOfModules S}
(σ : M.GeneratingSections)
(F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
[CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
max (max (u + 1) u₂) v₂}
F]
(η : unit S ≅ F.obj (unit R))
(e : F.obj M ≅ N)
[CategoryTheory.IsIso σ.π]
:
CategoryTheory.IsIso (σ.mapIso F η e).π
Carrying generating sections along a functor and an isomorphism preserves an invertible generating morphism.
instance
SheafOfModules.GeneratingSections.isFiniteType_mapIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
{S : CategoryTheory.Sheaf K RingCat}
[CategoryTheory.HasSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{N : SheafOfModules S}
(σ : M.GeneratingSections)
(F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
[CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
max (max (u + 1) u₂) v₂}
F]
(η : unit S ≅ F.obj (unit R))
(e : F.obj M ≅ N)
[hσ : σ.IsFiniteType]
:
(σ.mapIso F η e).IsFiniteType
Carrying generating sections along a functor and an isomorphism preserves finiteness.
noncomputable def
SheafOfModules.GeneratingSections.restrict
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{X Y : C}
(G : (M.over X).GeneratingSections)
(f : Y ⟶ X)
:
(M.over Y).GeneratingSections
Generating sections of M.over X restricted along f : Y ⟶ X to generating sections of
M.over Y: they are carried by the restriction functor overMap R f, which is identified with
restriction to Y by overFunctorMap.
Equations
- G.restrict f = G.mapIso (SheafOfModules.overMap R f) (SheafOfModules.overMapUnitIso f).symm ((SheafOfModules.overFunctorMap R f).app M)
Instances For
@[simp]
theorem
SheafOfModules.GeneratingSections.restrict_I
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{X Y : C}
(G : (M.over X).GeneratingSections)
(f : Y ⟶ X)
:
Restricting generating sections preserves their index type.
@[simp]
theorem
SheafOfModules.GeneratingSections.restrict_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{X Y : C}
(G : (M.over X).GeneratingSections)
(f : Y ⟶ X)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (G.restrict f).π = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (mapFreeIso (overMap R f) G.I (overMapUnitIso f).symm).hom
((overMap R f).map G.π))
((overFunctorMap R f).app M).hom
The generating morphism of restricted generating sections is obtained by mapping the original
generating morphism and then applying the comparison with restriction to Y, read along the
identification restrict_I of the index types.
instance
SheafOfModules.GeneratingSections.isIso_restrict_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{X Y : C}
(G : (M.over X).GeneratingSections)
(f : Y ⟶ X)
[CategoryTheory.IsIso G.π]
:
CategoryTheory.IsIso (G.restrict f).π
Restricting generating sections preserves an invertible generating morphism.
instance
SheafOfModules.GeneratingSections.isFiniteType_restrict
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
{X Y : C}
(G : (M.over X).GeneratingSections)
(f : Y ⟶ X)
[hG : G.IsFiniteType]
:
(G.restrict f).IsFiniteType
Restricting generating sections preserves finiteness.
noncomputable def
SheafOfModules.GeneratingSections.ofIteratedSlice
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M : SheafOfModules R}
{Z : C}
{Y : CategoryTheory.Over Z}
[CategoryTheory.HasSheafify (J.over Y.left) AddCommGrpCat]
[(J.over Y.left).WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify ((J.over Z).over Y) AddCommGrpCat]
[((J.over Z).over Y).WEqualsLocallyBijective AddCommGrpCat]
(σ : ((M.over Z).over Y).GeneratingSections)
:
(M.over Y.left).GeneratingSections
Generating sections of the twice-restricted sheaf (M.over Z).over Y, read along
Sheaf.iteratedSliceEquivalence as generating sections of the restriction of M to Y.left.
Equations
Instances For
@[simp]
theorem
SheafOfModules.GeneratingSections.ofIteratedSlice_I
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M : SheafOfModules R}
{Z : C}
{Y : CategoryTheory.Over Z}
[CategoryTheory.HasSheafify (J.over Y.left) AddCommGrpCat]
[(J.over Y.left).WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify ((J.over Z).over Y) AddCommGrpCat]
[((J.over Z).over Y).WEqualsLocallyBijective AddCommGrpCat]
(σ : ((M.over Z).over Y).GeneratingSections)
:
Transporting generating sections off an iterated slice preserves their index type.
@[simp]
theorem
SheafOfModules.GeneratingSections.ofIteratedSlice_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M : SheafOfModules R}
{Z : C}
{Y : CategoryTheory.Over Z}
[CategoryTheory.HasSheafify (J.over Y.left) AddCommGrpCat]
[(J.over Y.left).WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify ((J.over Z).over Y) AddCommGrpCat]
[((J.over Z).over Y).WEqualsLocallyBijective AddCommGrpCat]
(σ : ((M.over Z).over Y).GeneratingSections)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) σ.ofIteratedSlice.π = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(mapFreeIso (Sheaf.iteratedSliceEquivalence R Y).inverse σ.I (Sheaf.iteratedSliceEquivalenceUnitSheafIso R Y)).hom
((Sheaf.iteratedSliceEquivalence R Y).inverse.map σ.π))
(Sheaf.iteratedSliceEquivalenceInverseObjIso R Y M).hom
The generating morphism after transport off an iterated slice is the mapped generating
morphism followed by the comparison with restriction to Y.left, read along the identification
ofIteratedSlice_I of the index types.
instance
SheafOfModules.GeneratingSections.isIso_ofIteratedSlice_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M : SheafOfModules R}
{Z : C}
{Y : CategoryTheory.Over Z}
[CategoryTheory.HasSheafify (J.over Y.left) AddCommGrpCat]
[(J.over Y.left).WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify ((J.over Z).over Y) AddCommGrpCat]
[((J.over Z).over Y).WEqualsLocallyBijective AddCommGrpCat]
(σ : ((M.over Z).over Y).GeneratingSections)
[CategoryTheory.IsIso σ.π]
:
Reading a local basis through Sheaf.iteratedSliceEquivalence again gives a local basis.
instance
SheafOfModules.GeneratingSections.isFiniteType_ofIteratedSlice
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M : SheafOfModules R}
{Z : C}
{Y : CategoryTheory.Over Z}
[CategoryTheory.HasSheafify (J.over Y.left) AddCommGrpCat]
[(J.over Y.left).WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify ((J.over Z).over Y) AddCommGrpCat]
[((J.over Z).over Y).WEqualsLocallyBijective AddCommGrpCat]
(σ : ((M.over Z).over Y).GeneratingSections)
[hσ : σ.IsFiniteType]
:
Transporting generating sections off an iterated slice preserves finiteness.
theorem
SheafOfModules.GeneratingSections.exists_sieve_sum_smul_eq
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[CategoryTheory.HasSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules R}
(G : M.GeneratingSections)
[Fintype G.I]
{Y : C}
(m : ↑(M.val.obj (Opposite.op Y)))
:
∃ S ∈ J Y,
∀ ⦃Z : C⦄ (f : Z ⟶ Y),
S.arrows f →
∃ (a : G.I → ↑(R.obj.obj (Opposite.op Z))),
∑ k : G.I, a k • PresheafOfModules.sections.eval (G.s k) (Opposite.op Z) = (CategoryTheory.ConcreteCategory.hom (M.val.map f.op)) m
Finitely many generating sections generate every section locally: a section m of M over
Y is, on a covering sieve of Y, a linear combination of the restricted generators.