NYLL
Module

CategoricalPushout.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CategoricalPushout
29 declarations indexed from sourceView source ↗

Module documentation

Pushout extension and transpose laws

The actual pushout adjunction transports maps as coefficients change.

Imports5
  • Mathlib.CategoryTheory.Adjunction.Basic
  • Mathlib.CategoryTheory.Comma.Over.Basic
  • Mathlib.CategoryTheory.Comma.Over.Pullback
  • Mathlib.CategoryTheory.HomCongr
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Imported by2

Declarations

abbrev

model

L37 ↗
CategoryTheory.CategoricalTensorDescent.model
Documentation

The actual chosen pushout under the coefficient ring, with the underlying object and structural arrow stored directly. Its projections reduce without unfolding an intermediate Under.mk factory.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · full declaration
abbrev model (S B : Under R) : Under S.right where
  left := ⟨⟨⟩⟩
  right := pushout B.hom S.hom
  hom := pushout.inr B.hom S.hom
lemma

model_right

L43 ↗
CategoryTheory.CategoricalTensorDescent.model_right
Documentation

The canonical carrier projection of the chosen model.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma model_right (S B : Under R) : (model S B).right = pushout B.hom S.hom
lemma

model_hom

L46 ↗
CategoryTheory.CategoricalTensorDescent.model_hom
Documentation

The canonical coefficient arrow of the chosen model.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma model_hom (S B : Under R) : (model S B).hom = pushout.inr B.hom S.hom
def

modelIsoPushout

L50 ↗
CategoryTheory.CategoricalTensorDescent.modelIsoPushout
Documentation

The chosen model is exactly the object selected by the existing pushout functor. This explicit comparison is used at the adjunction boundary.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
def modelIsoPushout (S B : Under R) : model S B ≅ (Under.pushout S.hom).obj B
lemma

modelIsoPushout_inv_right

L54 ↗
CategoryTheory.CategoricalTensorDescent.modelIsoPushout_inv_right
Documentation

The comparison is the identity on the same chosen pushout.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma modelIsoPushout_inv_right (S B : Under R) :
    (modelIsoPushout S B).inv.right = 𝟙 (pushout B.hom S.hom)
abbrev

coefficientFunctor

L61 ↗
CategoryTheory.CategoricalTensorDescent.coefficientFunctor
Documentation

The existing coefficient-variable pushout functor, with its chosen object fields exposed at this owner boundary. Its maps and laws are those of the existing pushout/restriction composite; no universal property is reproved.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · full declaration
abbrev coefficientFunctor (D : Under R) : Under R ⥤ Under R where
  obj S :=
    { left := ⟨⟨⟩⟩
      right := pushout S.hom D.hom
      hom := D.hom ≫ pushout.inr S.hom D.hom }
  map h := (Under.map D.hom).map ((Under.pushout D.hom).map h)
  map_id S := (Under.pushout D.hom ⋙ Under.map D.hom).map_id S
  map_comp f g := (Under.pushout D.hom ⋙ Under.map D.hom).map_comp f g
lemma

coefficientFunctor_eq

L71 ↗
CategoryTheory.CategoricalTensorDescent.coefficientFunctor_eq
Documentation

The factory retains the original coefficient functor itself.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma coefficientFunctor_eq (D : Under R) :
    coefficientFunctor D = Under.pushout D.hom ⋙ Under.map D.hom
lemma

coefficientFunctor_obj_right

L75 ↗
CategoryTheory.CategoricalTensorDescent.coefficientFunctor_obj_right
Documentation

The coefficient functor uses the literal chosen pushout object.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma coefficientFunctor_obj_right (S D : Under R) :
    ((coefficientFunctor D).obj S).right = pushout S.hom D.hom
lemma

coefficientFunctor_obj_hom

L79 ↗
CategoryTheory.CategoricalTensorDescent.coefficientFunctor_obj_hom
Documentation

Its original-base arrow is the fixed model's pushout coprojection.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma coefficientFunctor_obj_hom (S D : Under R) :
    ((coefficientFunctor D).obj S).hom = D.hom ≫ pushout.inr S.hom D.hom
def

flip

L83 ↗
CategoryTheory.CategoricalTensorDescent.flip
Documentation

Exchange the two pushout legs after restriction of scalars.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
def flip (S D : Under R) :
    (Under.map S.hom).obj (model S D) ≅ (coefficientFunctor D).obj S
def

transpose

L92 ↗
CategoryTheory.CategoricalTensorDescent.transpose
Documentation

The pushout adjunction, with the coefficient-variable target orientation.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
def transpose (S B D : Under R) :
    (model S B ⟶ model S D) ≃ (B ⟶ (coefficientFunctor D).obj S)
lemma

transpose_right

L97 ↗
CategoryTheory.CategoricalTensorDescent.transpose_right
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma transpose_right (S B D : Under R) (f : model S B ⟶ model S D) :
    (transpose S B D f).right = pushout.inl B.hom S.hom ≫ f.right ≫
      (pushoutSymmetry D.hom S.hom).hom
def

leg

L111 ↗
CategoryTheory.CategoricalTensorDescent.leg
Documentation

The underlying pushout map for a change of coefficient object.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
def leg {S T : Under R} (h : S ⟶ T) (B : Under R) :
    (model S B).right ⟶ (model T B).right
lemma

leg_inl

L121 ↗
CategoryTheory.CategoricalTensorDescent.leg_inl
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma leg_inl {S T : Under R} (h : S ⟶ T) (B : Under R) :
    pushout.inl B.hom S.hom ≫ leg h B = pushout.inl B.hom T.hom
lemma

leg_inr

L126 ↗
CategoryTheory.CategoricalTensorDescent.leg_inr
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma leg_inr {S T : Under R} (h : S ⟶ T) (B : Under R) :
    pushout.inr B.hom S.hom ≫ leg h B = h.right ≫ pushout.inr B.hom T.hom
lemma

leg_id

L130 ↗
CategoryTheory.CategoricalTensorDescent.leg_id
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma leg_id (S B : Under R) : leg (𝟙 S) B = 𝟙 (model S B).right
lemma

leg_comp

L135 ↗
CategoryTheory.CategoricalTensorDescent.leg_comp
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma leg_comp {S T U : Under R} (h : S ⟶ T) (k : T ⟶ U) (B : Under R) :
    leg (h ≫ k) B = leg h B ≫ leg k B
def

extend

L143 ↗
CategoryTheory.CategoricalTensorDescent.extend
Documentation

Extend a morphism of base-extended models along a coefficient morphism.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
def extend {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : model S B ⟶ model S D) : model T B ⟶ model T D
lemma

extend_inl

L165 ↗
CategoryTheory.CategoricalTensorDescent.extend_inl
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_inl {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : model S B ⟶ model S D) :
    pushout.inl B.hom T.hom ≫ (extend h f).right =
      pushout.inl B.hom S.hom ≫ f.right ≫ leg h D
lemma

extend_inr

L172 ↗
CategoryTheory.CategoricalTensorDescent.extend_inr
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_inr {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : model S B ⟶ model S D) :
    pushout.inr B.hom T.hom ≫ (extend h f).right = pushout.inr D.hom T.hom
lemma

extend_leg

L177 ↗
CategoryTheory.CategoricalTensorDescent.extend_leg
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_leg {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : model S B ⟶ model S D) :
    leg h B ≫ (extend h f).right = f.right ≫ leg h D
lemma

extend_id

L187 ↗
CategoryTheory.CategoricalTensorDescent.extend_id
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_id {S T : Under R} (h : S ⟶ T) (B : Under R) :
    extend h (𝟙 (model S B)) = 𝟙 (model T B)
lemma

extend_comp

L194 ↗
CategoryTheory.CategoricalTensorDescent.extend_comp
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_comp {S T : Under R} (h : S ⟶ T) {B D E : Under R}
    (f : model S B ⟶ model S D) (g : model S D ⟶ model S E) :
    extend h (f ≫ g) = extend h f ≫ extend h g
lemma

extend_identity_arrow

L203 ↗
CategoryTheory.CategoricalTensorDescent.extend_identity_arrow
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_identity_arrow (S : Under R) {B D : Under R}
    (f : model S B ⟶ model S D) : extend (𝟙 S) f = f
lemma

extend_trans

L210 ↗
CategoryTheory.CategoricalTensorDescent.extend_trans
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma extend_trans {S T U : Under R} (h : S ⟶ T) (k : T ⟶ U) {B D : Under R}
    (f : model S B ⟶ model S D) : extend k (extend h f) = extend (h ≫ k) f
lemma

coefficientFunctor_map_inl

L219 ↗
CategoryTheory.CategoricalTensorDescent.coefficientFunctor_map_inl
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma coefficientFunctor_map_inl {S T : Under R} (h : S ⟶ T) (D : Under R) :
    pushout.inl S.hom D.hom ≫ ((coefficientFunctor D).map h).right =
      h.right ≫ pushout.inl T.hom D.hom
lemma

coefficientFunctor_map_inr

L225 ↗
CategoryTheory.CategoricalTensorDescent.coefficientFunctor_map_inr
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma coefficientFunctor_map_inr {S T : Under R} (h : S ⟶ T) (D : Under R) :
    pushout.inr S.hom D.hom ≫ ((coefficientFunctor D).map h).right =
      pushout.inr T.hom D.hom
lemma

leg_flip

L230 ↗
CategoryTheory.CategoricalTensorDescent.leg_flip
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma leg_flip {S T : Under R} (h : S ⟶ T) (D : Under R) :
    leg h D ≫ (pushoutSymmetry D.hom T.hom).hom =
      (pushoutSymmetry D.hom S.hom).hom ≫ ((coefficientFunctor D).map h).right
lemma

transpose_naturality

L239 ↗
CategoryTheory.CategoricalTensorDescent.transpose_naturality
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.CategoricalTensorDescent
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPushouts C] {R : C}
noncomputable section
Lean source · statement
lemma transpose_naturality {S T : Under R} (h : S ⟶ T) {B D : Under R}
    (f : model S B ⟶ model S D) :
    transpose T B D (extend h f) = transpose S B D f ≫ (coefficientFunctor D).map h

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.