Products of section charts in a slice category

The pullback of two sections over the same base has equal projections to that base. Consequently a product chart followed by multiplication in a monoid object evaluates as the product of its two sections. This is useful for restricting group operations to a subscheme covered by sections.

theorem TauCeti.CategoryTheory.Over.pullback_map_comp_mul_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {S : C} {D G : CategoryTheory.Over S} [CategoryTheory.MonObj G] (i : D ⟶ G) (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left a) D.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left b) D.hom) D.hom D.hom (CategoryTheory.Over.Hom.left a) (CategoryTheory.Over.Hom.left b) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left a) D.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left b) D.hom)) (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp a i * CategoryTheory.CategoryStruct.comp b i))

On a product of two section charts, multiplication after a map to a monoid object is the product of the resulting sections, pulled back from the base.

theorem TauCeti.CategoryTheory.Over.pullback_map_comp_mul_left_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {S : C} {D G : CategoryTheory.Over S} [CategoryTheory.MonObj G] (i : D ⟶ G) (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ D) {Z : C} (h : G.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left a) D.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left b) D.hom) D.hom D.hom (CategoryTheory.Over.Hom.left a) (CategoryTheory.Over.Hom.left b) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left a) D.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left b) D.hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp a i * CategoryTheory.CategoryStruct.comp b i)) h)

On a product of two section charts, multiplication after a map to a monoid object is the product of the resulting sections, pulled back from the base.