Free sheaves on finitely many generators

This file records basic properties of free sheaves of modules. It gives the canonical identification between the free sheaf on one generator and the tensor unit, shows that the free sheaf on no generators is a zero object, and identifies the sections of a finite free sheaf with tuples of sections of the coefficient sheaf.

For a finite index type, the free sheaf is also a finite biproduct of copies of the sheaf of rings, so each of its sections is a linear combination of the tautological sections SheafOfModules.freeSection, with coefficients in the ring of sections over the same object. The morphism out of a free sheaf determined by a family of sections sends such a combination to the corresponding combination of those sections. These are the sectionwise computations by which generators and relations of a finitely presented sheaf are handled locally.

Main declarations

• TauCeti.SheafOfModules.freePUnitIsoUnit identifies the free sheaf on PUnit with the sheaf of rings itself, regarded as a sheaf of modules;
• TauCeti.SheafOfModules.isZero_free: the free sheaf on an empty type is a zero object;
• TauCeti.SheafOfModules.biproductIsoFree: a finite free sheaf is the biproduct of copies of the unit;
• TauCeti.SheafOfModules.evaluationFreeIso: the sections of a finite free sheaf are tuples of sections of the coefficient sheaf;
• TauCeti.SheafOfModules.freeBasis: the corresponding basis of sections, consisting of the tautological sections freeSection i;
• TauCeti.SheafOfModules.exists_eq_sum_smul_freeSection: every section of a finite free sheaf is a linear combination of the tautological sections;
• TauCeti.SheafOfModules.freeHomEquiv_symm_val_app_sum_smul: evaluation of the morphism out of a free sheaf on such a linear combination;
• TauCeti.SheafOfModules.isIso_unitHomEquiv_symm: the morphism unit R ⟶ M attached to a global section s is an isomorphism when scalar multiplication on s is bijective over every object, that is, when s is a global basis of M.

The first comparison is used both by tensor-unit computations and when restricting a rank-one local trivialization. No formalization is vendored; it is Mathlib's canonical isomorphism from a coproduct indexed by a unique type to its unique summand.

noncomputable def TauCeti.SheafOfModules.freePUnitIsoUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.Sheaf J RingCat) : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.unit S

The free sheaf on one generator is canonically isomorphic to the tensor unit.

Equations

• TauCeti.SheafOfModules.freePUnitIsoUnit S = CategoryTheory.Limits.coproductUniqueIso fun (x : PUnit.{?u.3 + 1}) => SheafOfModules.unit S

@[simp]

theorem TauCeti.SheafOfModules.freePUnitIsoUnit_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.Sheaf J RingCat) : (freePUnitIsoUnit S).inv = SheafOfModules.ιFree PUnit.unit

The inverse of freePUnitIsoUnit is the unique basis inclusion.

theorem TauCeti.SheafOfModules.isZero_free {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {S : CategoryTheory.Sheaf J RingCat} (I : Type u) [IsEmpty I] : CategoryTheory.Limits.IsZero (SheafOfModules.free I)

The free sheaf of modules on an empty type is a zero object: it is the coproduct of the empty family.

theorem TauCeti.SheafOfModules.exists_eq_sum_smul_freeSection {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} {I : Type u} [Fintype I] {Y : Cᵒᵖ} (c : ↑((SheafOfModules.free I).val.obj Y)) : ∃ (a : I → ↑(R.obj.obj Y)), c = ∑ k : I, a k • PresheafOfModules.sections.eval (SheafOfModules.freeSection k) Y

Every section of a free sheaf on a finite type is a linear combination of the tautological sections, with coefficients in the ring of sections over the same object.

theorem TauCeti.SheafOfModules.freeHomEquiv_symm_val_app_sum_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} {I : Type u} [Fintype I] {M : SheafOfModules R} (s : I → M.sections) (Y : Cᵒᵖ) (a : I → ↑(R.obj.obj Y)) : (CategoryTheory.ConcreteCategory.hom ((M.freeHomEquiv.symm s).val.app Y)) (∑ k : I, a k • PresheafOfModules.sections.eval (SheafOfModules.freeSection k) Y) = ∑ k : I, a k • PresheafOfModules.sections.eval (s k) Y

The morphism out of a finite free sheaf determined by a family of sections s sends a linear combination of the tautological sections to the same linear combination of the s k.

@[simp]

theorem TauCeti.SheafOfModules.unitHomEquiv_symm_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (s : M.sections) (Y : Cᵒᵖ) (r : ↑(R.obj.obj Y)) : (CategoryTheory.ConcreteCategory.hom ((M.unitHomEquiv.symm s).val.app Y)) r = r • PresheafOfModules.sections.eval s Y

The morphism unit R ⟶ M attached to a global section s sends a scalar r over Y to r • s.

theorem TauCeti.SheafOfModules.isIso_unitHomEquiv_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (s : M.sections) (hs : ∀ (Y : Cᵒᵖ), Function.Bijective fun (r : ↑(R.obj.obj Y)) => r • PresheafOfModules.sections.eval s Y) : CategoryTheory.IsIso (M.unitHomEquiv.symm s)

The morphism unit R ⟶ M attached to a global section s is an isomorphism as soon as, over every object Y, multiplying s by scalars is a bijection R(Y) ⟶ M(Y): s is then a global basis of M.

noncomputable def TauCeti.SheafOfModules.biproductIsoFree {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] : (⨁ fun (x : I) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) ≅ SheafOfModules.free I

The free sheaf of modules on a finite type I is the biproduct of I copies of the unit.

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.biproduct_ι_biproductIsoFree_hom {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I : Type u} [Finite I] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : I) => SheafOfModules.unit (ringCatSheaf R)) i) (biproductIsoFree I).hom = SheafOfModules.ιFree i

biproductIsoFree sends the i-th summand to the i-th basis section.

@[simp]

theorem TauCeti.SheafOfModules.biproduct_ι_biproductIsoFree_hom_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I : Type u} [Finite I] (i : I) {Z : SheafOfModules (ringCatSheaf R)} (h : SheafOfModules.free I ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : I) => SheafOfModules.unit (ringCatSheaf R)) i) (CategoryTheory.CategoryStruct.comp (biproductIsoFree I).hom h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) h

biproductIsoFree sends the i-th summand to the i-th basis section.

@[simp]

theorem TauCeti.SheafOfModules.ιFree_biproductIsoFree_inv {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I : Type u} [Finite I] (i : I) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (biproductIsoFree I).inv = CategoryTheory.Limits.biproduct.ι (fun (x : I) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) i

The inverse of biproductIsoFree sends the i-th basis section to the i-th summand.

@[simp]

theorem TauCeti.SheafOfModules.ιFree_biproductIsoFree_inv_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I : Type u} [Finite I] (i : I) {Z : SheafOfModules (ringCatSheaf R)} (h : (⨁ fun (x : I) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (CategoryTheory.CategoryStruct.comp (biproductIsoFree I).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : I) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) i) h

The inverse of biproductIsoFree sends the i-th basis section to the i-th summand.

noncomputable def TauCeti.SheafOfModules.evaluationFreeIso {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (W : Cᵒᵖ) : (SheafOfModules.evaluation (ringCatSheaf R) W).obj (SheafOfModules.free I) ≅ ↧(I → ↑((ringCatSheaf R).obj.obj W))

The sections over W of the free sheaf of modules on a finite type I are the I-indexed tuples of sections of the sheaf of rings over W: free I is the product of I copies of the unit, and evaluation at W preserves products.

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.evaluationFreeIso_hom_comp_proj {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (W : Cᵒᵖ) (i : I) : CategoryTheory.CategoryStruct.comp (evaluationFreeIso I W).hom (ModuleCat.ofHom (LinearMap.proj i)) = (SheafOfModules.evaluation (ringCatSheaf R) W).map (CategoryTheory.CategoryStruct.comp (biproductIsoFree I).inv (CategoryTheory.Limits.biproduct.π (fun (x : I) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) i))

The i-th coordinate of a section of free I under evaluationFreeIso is its image under the i-th projection free I ⟶ R of the biproduct decomposition of free I.

@[simp]

theorem TauCeti.SheafOfModules.evaluationFreeIso_hom_comp_proj_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (W : Cᵒᵖ) (i : I) {Z : ModuleCat ↑((ringCatSheaf R).obj.obj W)} (h : ↧↑((ringCatSheaf R).obj.obj W) ⟶ Z) : CategoryTheory.CategoryStruct.comp (evaluationFreeIso I W).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.proj i)) h) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.evaluation (ringCatSheaf R) W).map (CategoryTheory.CategoryStruct.comp (biproductIsoFree I).inv (CategoryTheory.Limits.biproduct.π (fun (x : I) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) i))) h

The i-th coordinate of a section of free I under evaluationFreeIso is its image under the i-th projection free I ⟶ R of the biproduct decomposition of free I.

noncomputable def TauCeti.SheafOfModules.freeBasis {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (W : Cᵒᵖ) : Module.Basis I ↑(R.obj.obj W) ↑(PresheafOfModulesOfCommRing.obj (SheafOfModules.free I).val W)

The basis of the sections over W of the free sheaf of modules on a finite type I, obtained from the standard basis of I-tuples through evaluationFreeIso. Its i-th member is the basis section freeSection i over W (freeBasis_apply).

Equations

• TauCeti.SheafOfModules.freeBasis I W = (Pi.basisFun (↑(R.obj.obj W)) I).map (TauCeti.SheafOfModules.evaluationFreeIso I W).toLinearEquiv.symm

@[simp]

theorem TauCeti.SheafOfModules.freeBasis_apply {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (W : Cᵒᵖ) (i : I) : (freeBasis I W) i = PresheafOfModules.sections.eval (SheafOfModules.freeSection i) W

The i-th member of freeBasis I W is the basis section freeSection i over W.

theorem TauCeti.SheafOfModules.freeBasis_map {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] {W W' : Cᵒᵖ} (f : W ⟶ W') (i : I) : (CategoryTheory.ConcreteCategory.hom ((SheafOfModules.free I).val.map f)) ((freeBasis I W) i) = (freeBasis I W') i

The restriction maps of a finite free sheaf preserve the members of freeBasis.