Base change of the second factor of a pullback, and sections

Fix π : Y ⟶ S. A morphism k : T' ⟶ T with k ≫ a = a' induces the base-change morphism

pullback.mapSnd π a a' k hk : pullback π a' ⟶ pullback π a

which is the identity on the first factor Y and k on the second. A lift s : T ⟶ Y of a : T ⟶ S through π induces a section pullbackSection π a s hs : T ⟶ pullback π a of the second projection pullback.snd π a, with first projection s.

When s = a ≫ σ for a section σ of π, pullbackSection π a s hs is the section underlying CategoryTheory.SplitEpi.pullback.

Main definitions

• CategoryTheory.Limits.pullback.mapSnd: the morphism pullback π a' ⟶ pullback π a induced by a morphism k : T' ⟶ T over S.
• CategoryTheory.Limits.pullbackSection: the section of pullback.snd π a induced by a lift of a through π.

Main results

• CategoryTheory.Limits.pullback.mapSnd_id and CategoryTheory.Limits.pullback.mapSnd_comp: pullback.mapSnd preserves identities and composition.
• CategoryTheory.Limits.pullbackSection_comp_mapSnd: pullbackSection is natural across pullback.mapSnd.

Provenance

pullback.mapSnd, pullbackSection and their lemmas generalise declarations of AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/Picard/RelativePic.lean: AlgebraicGeometry.Scheme.Modules.baseChangeMap, baseChangeMap_id, baseChangeMap_comp, baseChangeZero, baseChangeZero_snd, and baseChangeZero_baseChangeMap. There the category is that of schemes and the section is induced by a section of π; here the category is arbitrary and the section is induced by any lift of a through π.

noncomputable def CategoryTheory.Limits.pullback.mapSnd {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') [HasPullback π a] [HasPullback π a'] : pullback π a' ⟶ pullback π a

Base change of the second factor along k : T' ⟶ T with k ≫ a = a': the morphism pullback π a' ⟶ pullback π a that is the identity on the first factor Y and k on the second, namely pullback.map with identities on Y and S.

Equations

• CategoryTheory.Limits.pullback.mapSnd π a a' k hk = CategoryTheory.Limits.pullback.map π a' π a (CategoryTheory.CategoryStruct.id Y) k (CategoryTheory.CategoryStruct.id S) ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_fst {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') [HasPullback π a] [HasPullback π a'] : CategoryStruct.comp (mapSnd π a a' k hk) (fst π a) = fst π a'

Base change of the second factor is the identity on the first factor Y: it commutes with the first projections.

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_fst_assoc {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') [HasPullback π a] [HasPullback π a'] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (mapSnd π a a' k hk) (CategoryStruct.comp (fst π a) h) = CategoryStruct.comp (fst π a') h

Base change of the second factor is the identity on the first factor Y: it commutes with the first projections.

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_snd {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') [HasPullback π a] [HasPullback π a'] : CategoryStruct.comp (mapSnd π a a' k hk) (snd π a) = CategoryStruct.comp (snd π a') k

Base change of the second factor along k is k on second factors: followed by the second projection of pullback π a, it is the second projection of pullback π a' followed by k.

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_snd_assoc {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') [HasPullback π a] [HasPullback π a'] {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (mapSnd π a a' k hk) (CategoryStruct.comp (snd π a) h) = CategoryStruct.comp (snd π a') (CategoryStruct.comp k h)

Base change of the second factor along k is k on second factors: followed by the second projection of pullback π a, it is the second projection of pullback π a' followed by k.

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_id {C : Type u} [Category.{v, u} C] {Y S T : C} (π : Y ⟶ S) (a : T ⟶ S) [HasPullback π a] : mapSnd π a a (CategoryStruct.id T) ⋯ = CategoryStruct.id (pullback π a)

Base change of the second factor along the identity is the identity.

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_comp {C : Type u} [Category.{v, u} C] {Y S T T' T'' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (a'' : T'' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') (l : T'' ⟶ T') (hl : CategoryStruct.comp l a' = a'') [HasPullback π a] [HasPullback π a'] [HasPullback π a''] : CategoryStruct.comp (mapSnd π a' a'' l hl) (mapSnd π a a' k hk) = mapSnd π a a'' (CategoryStruct.comp l k) ⋯

Base change of the second factor is compatible with composition: base change along l : T'' ⟶ T' followed by base change along k : T' ⟶ T is base change along l ≫ k.

@[simp]

theorem CategoryTheory.Limits.pullback.mapSnd_comp_assoc {C : Type u} [Category.{v, u} C] {Y S T T' T'' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (a'' : T'' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') (l : T'' ⟶ T') (hl : CategoryStruct.comp l a' = a'') [HasPullback π a] [HasPullback π a'] [HasPullback π a''] {Z : C} (h : pullback π a ⟶ Z) : CategoryStruct.comp (mapSnd π a' a'' l hl) (CategoryStruct.comp (mapSnd π a a' k hk) h) = CategoryStruct.comp (mapSnd π a a'' (CategoryStruct.comp l k) ⋯) h

Base change of the second factor is compatible with composition: base change along l : T'' ⟶ T' followed by base change along k : T' ⟶ T is base change along l ≫ k.

noncomputable def CategoryTheory.Limits.pullbackSection {C : Type u} [Category.{v, u} C] {Y S T : C} (π : Y ⟶ S) (a : T ⟶ S) (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] : T ⟶ pullback π a

The section of pullback.snd π a induced by a lift s of a through π: its first projection is s and its second projection is the identity of T.

Equations

• CategoryTheory.Limits.pullbackSection π a s hs = CategoryTheory.Limits.pullback.lift s (CategoryTheory.CategoryStruct.id T) ⋯

@[simp]

theorem CategoryTheory.Limits.pullbackSection_fst {C : Type u} [Category.{v, u} C] {Y S T : C} (π : Y ⟶ S) (a : T ⟶ S) (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] : CategoryStruct.comp (pullbackSection π a s hs) (pullback.fst π a) = s

The first projection of the section induced by a lift s is s.

@[simp]

theorem CategoryTheory.Limits.pullbackSection_fst_assoc {C : Type u} [Category.{v, u} C] {Y S T : C} (π : Y ⟶ S) (a : T ⟶ S) (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (pullbackSection π a s hs) (CategoryStruct.comp (pullback.fst π a) h) = CategoryStruct.comp s h

The first projection of the section induced by a lift s is s.

@[simp]

theorem CategoryTheory.Limits.pullbackSection_snd {C : Type u} [Category.{v, u} C] {Y S T : C} (π : Y ⟶ S) (a : T ⟶ S) (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] : CategoryStruct.comp (pullbackSection π a s hs) (pullback.snd π a) = CategoryStruct.id T

The section induced by a lift is a section of the second projection.

@[simp]

theorem CategoryTheory.Limits.pullbackSection_snd_assoc {C : Type u} [Category.{v, u} C] {Y S T : C} (π : Y ⟶ S) (a : T ⟶ S) (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (pullbackSection π a s hs) (CategoryStruct.comp (pullback.snd π a) h) = h

The section induced by a lift is a section of the second projection.

theorem CategoryTheory.Limits.pullbackSection_comp_mapSnd {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] [HasPullback π a'] : CategoryStruct.comp (pullbackSection π a' (CategoryStruct.comp k s) ⋯) (pullback.mapSnd π a a' k hk) = CategoryStruct.comp k (pullbackSection π a s hs)

Naturality of pullbackSection across pullback.mapSnd: base change along k carries the section induced by the lift k ≫ s of a' to k followed by the section induced by s.

theorem CategoryTheory.Limits.pullbackSection_comp_mapSnd_assoc {C : Type u} [Category.{v, u} C] {Y S T T' : C} (π : Y ⟶ S) (a : T ⟶ S) (a' : T' ⟶ S) (k : T' ⟶ T) (hk : CategoryStruct.comp k a = a') (s : T ⟶ Y) (hs : CategoryStruct.comp s π = a) [HasPullback π a] [HasPullback π a'] {Z : C} (h : pullback π a ⟶ Z) : CategoryStruct.comp (pullbackSection π a' (CategoryStruct.comp k s) ⋯) (CategoryStruct.comp (pullback.mapSnd π a a' k hk) h) = CategoryStruct.comp k (CategoryStruct.comp (pullbackSection π a s hs) h)

Naturality of pullbackSection across pullback.mapSnd: base change along k carries the section induced by the lift k ≫ s of a' to k followed by the section induced by s.