ModuleExtensionPullback.lean
Nyll.EtaleFundamentalGroups.Cohomology.ExtensionPullback
3 declarations indexed from sourceView source ↗ Module documentation
Pulling an extension back with its original coefficient identification
The middle object is the actual categorical pullback. Its kernel is identified using a specified isomorphism to the original kernel, and its short exactness is proved from the pullback and kernel universal properties.
Imports2
- Mathlib.Algebra.Homology.ShortComplex.ShortExact
- Mathlib.CategoryTheory.Abelian.Basic
Imported by2
Declarations
EtaleFundamentalGroups.Cohomology.coefficientPullbackExtension
DocumentationThe actual pullback extension, keeping the chosen coefficient object.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
universe v u
namespace EtaleFundamentalGroups.Cohomology
variable {C : Type u} [Category.{v} C] [Abelian C]
(S : ShortComplex C) {F Y : C} (e : F ≅ S.X₁) (f : Y ⟶ S.X₃)
EtaleFundamentalGroups.Cohomology.coefficientPullbackExtension_f_fst
DocumentationIts middle map to the original extension preserves the original inclusion.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
universe v u
namespace EtaleFundamentalGroups.Cohomology
variable {C : Type u} [Category.{v} C] [Abelian C]
(S : ShortComplex C) {F Y : C} (e : F ≅ S.X₁) (f : Y ⟶ S.X₃)
EtaleFundamentalGroups.Cohomology.coefficientPullbackExtension_shortExact
DocumentationPullback preserves short exactness, including the original coefficient identification; no new exactness hypothesis is imposed on the pullback.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
universe v u
namespace EtaleFundamentalGroups.Cohomology
variable {C : Type u} [Category.{v} C] [Abelian C]
(S : ShortComplex C) {F Y : C} (e : F ≅ S.X₁) (f : Y ⟶ S.X₃)