Pullbacks of split epimorphisms

This file proves that a chosen section pulls back along an arbitrary morphism. If s : S ⟶ X is a section of f : X ⟶ S and g : T ⟶ S, its base change is the canonical morphism

T ⟶ X ×[S] T

whose projections are g ≫ s and 𝟙 T. The construction is packaged as CategoryTheory.SplitEpi.pullback; its projection formulas characterize it uniquely. The file also records naturality in both the split epimorphism and the base-change morphism, and supplies the corresponding low-priority IsSplitEpi instance.

For a scheme over a field, a rational point is precisely such a chosen section of the structure morphism. Thus this construction supplies base change of rational points, as required by the displayed x₀.baseChange K and base-change compatibility target in TauCetiRoadmap/JacobianChallenge/README.md. No formalization is vendored; the construction is the universal property of Mathlib's pullback.

noncomputable def CategoryTheory.SplitEpi.pullback {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T : C} (g : T ⟶ S) [Limits.HasPullback f g] : SplitEpi (Limits.pullback.snd f g)

Pull a chosen section of f : X ⟶ S back along g : T ⟶ S.

The resulting section of pullback.snd f g has first projection g ≫ h.section_ and second projection the identity of T.

Equations

• h.pullback g = { section_ := CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp g h.section_) (CategoryTheory.CategoryStruct.id T) ⋯, id := ⋯ }

theorem CategoryTheory.SplitEpi.pullback_section_def {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T : C} (g : T ⟶ S) [Limits.HasPullback f g] : (h.pullback g).section_ = Limits.pullback.lift (CategoryStruct.comp g h.section_) (CategoryStruct.id T) ⋯

The section underlying SplitEpi.pullback is the canonical pullback lift.

@[simp]

theorem CategoryTheory.SplitEpi.pullback_section_fst {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T : C} (g : T ⟶ S) [Limits.HasPullback f g] : CategoryStruct.comp (h.pullback g).section_ (Limits.pullback.fst f g) = CategoryStruct.comp g h.section_

The first projection of a pulled-back section is the original section after the base-change morphism.

@[simp]

theorem CategoryTheory.SplitEpi.pullback_section_fst_assoc {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T : C} (g : T ⟶ S) [Limits.HasPullback f g] {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (h.pullback g).section_ (CategoryStruct.comp (Limits.pullback.fst f g) h✝) = CategoryStruct.comp g (CategoryStruct.comp h.section_ h✝)

The first projection of a pulled-back section is the original section after the base-change morphism.

theorem CategoryTheory.SplitEpi.eq_pullback_section {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T : C} (g : T ⟶ S) [Limits.HasPullback f g] (t : T ⟶ Limits.pullback f g) (hfst : CategoryStruct.comp t (Limits.pullback.fst f g) = CategoryStruct.comp g h.section_) (hsnd : CategoryStruct.comp t (Limits.pullback.snd f g) = CategoryStruct.id T) : t = (h.pullback g).section_

The two projection formulas uniquely determine the pulled-back section.

theorem CategoryTheory.SplitEpi.pullback_section_naturality {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} {Y : C} {f' : Y ⟶ S} (h : SplitEpi f) (h' : SplitEpi f') (i : X ⟶ Y) (hi : f = CategoryStruct.comp i f') (hsection : CategoryStruct.comp h.section_ i = h'.section_) {T : C} (g : T ⟶ S) [Limits.HasPullback f g] [Limits.HasPullback f' g] : CategoryStruct.comp (h.pullback g).section_ (Limits.pullback.map f g f' g i (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) = (h'.pullback g).section_

Pullback of chosen sections is natural in morphisms of split epimorphisms.

Here i : X ⟶ Y lies over S, and h.section_ ≫ i = h'.section_ says that it preserves the chosen sections. The induced map of pullbacks then preserves their pulled-back sections.

theorem CategoryTheory.SplitEpi.pullback_section_map {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T T' : C} (g : T ⟶ S) (k : T' ⟶ T) [Limits.HasPullback f g] [Limits.HasPullback f (CategoryStruct.comp k g)] : CategoryStruct.comp (h.pullback (CategoryStruct.comp k g)).section_ (Limits.pullback.map f (CategoryStruct.comp k g) f g (CategoryStruct.id X) k (CategoryStruct.id S) ⋯ ⋯) = CategoryStruct.comp k (h.pullback g).section_

Pullback of a chosen section is natural in the base-change morphism.

For k : T' ⟶ T, the canonical map from the pullback along k ≫ g to the pullback along g carries the section over T' to the section over T precomposed with k.

theorem CategoryTheory.SplitEpi.pullback_section_map_of_eq {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : SplitEpi f) {T T' : C} (g : T ⟶ S) (g' : T' ⟶ S) (k : T' ⟶ T) (w : CategoryStruct.comp k g = g') [Limits.HasPullback f g] [Limits.HasPullback f g'] : CategoryStruct.comp (h.pullback g').section_ (Limits.pullback.map f g' f g (CategoryStruct.id X) k (CategoryStruct.id S) ⋯ ⋯) = CategoryStruct.comp k (h.pullback g).section_

Naturality of a pulled-back section when the base-change composite is given by an equal morphism. This form is convenient for morphisms in an over category.

@[instance 100]

instance CategoryTheory.Limits.pullback.snd_isSplitEpi {C : Type u} [Category.{v, u} C] {X S T : C} (f : X ⟶ S) (g : T ⟶ S) [HasPullback f g] [IsSplitEpi f] : IsSplitEpi (snd f g)

A pullback of a split epimorphism is a split epimorphism.

The low priority leaves more specialized instances, such as the diagonal pullback, in control when they apply. Use SplitEpi.pullback when the particular chosen section matters.