Extradegeneracy for the Cech object #
Let U : FormalCoproduct C. Let T be a terminal object in C.
In this file, we construct an isomorphism from the Cech object U.cech that is
defined for objects in FormalCoproduct to the general Cech nerve construction
applied to the morphism from U to the terminal object.
This isomorphism is used in order to show that, as an augmented object (over T),
the Cech object U.cech has an extra degeneracy when there is a
morphism T ⟶ U.obj i₀ for some i₀.
instance
CategoryTheory.Limits.FormalCoproduct.instHasWidePullbackFinHAddNatOfNatRightMkFromIsTerminalInclLeftHom
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : ℕ)
:
HasWidePullback (Arrow.mk ((isTerminalIncl T hT).from U)).right
(fun (x : Fin (n + 1)) => (Arrow.mk ((isTerminalIncl T hT).from U)).left) fun (x : Fin (n + 1)) =>
(Arrow.mk ((isTerminalIncl T hT).from U)).hom
instance
CategoryTheory.Limits.FormalCoproduct.instHasLimitWidePullbackShapeToTypeSimplexCategoryOrderHomFinHAddNatLenOfNatWideCospanObjInclFromIsTerminalIncl
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : SimplexCategory)
:
HasLimit
(WidePullbackShape.wideCospan ((incl C).obj T) (fun (x : ToType n) => U) fun (x : ToType n) =>
(isTerminalIncl T hT).from U)
noncomputable def
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : SimplexCategoryᵒᵖ)
:
Auxiliary definition for cechIsoCechNerve.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : SimplexCategoryᵒᵖ)
(i : ToType (Opposite.unop n))
:
CategoryStruct.comp (U.cechIsoCechNerveApp hT n).hom
(WidePullback.π (fun (x : ToType (Opposite.unop n)) => (isTerminalIncl T hT).from U) i) = U.powerπ i
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π_assoc
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : SimplexCategoryᵒᵖ)
(i : ToType (Opposite.unop n))
{Z : FormalCoproduct C}
(h : U ⟶ Z)
:
CategoryStruct.comp (U.cechIsoCechNerveApp hT n).hom
(CategoryStruct.comp (WidePullback.π (fun (x : ToType (Opposite.unop n)) => (isTerminalIncl T hT).from U) i) h) = CategoryStruct.comp (U.powerπ i) h
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : SimplexCategoryᵒᵖ)
(i : ToType (Opposite.unop n))
:
CategoryStruct.comp (U.cechIsoCechNerveApp hT n).inv (U.powerπ i) = WidePullback.π (fun (x : ToType (Opposite.unop n)) => (isTerminalIncl T hT).from U) i
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π_assoc
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(n : SimplexCategoryᵒᵖ)
(i : ToType (Opposite.unop n))
{Z : FormalCoproduct C}
(h : U ⟶ Z)
:
CategoryStruct.comp (U.cechIsoCechNerveApp hT n).inv (CategoryStruct.comp (U.powerπ i) h) = CategoryStruct.comp (WidePullback.π (fun (x : ToType (Opposite.unop n)) => (isTerminalIncl T hT).from U) i) h
noncomputable def
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
:
The Cech construction for FormalCoproduct is isomorphic
to the general Arrow.cechNerve construction applied to the morphism
to the terminal object.
Equations
- U.cechIsoCechNerve hT = CategoryTheory.NatIso.ofComponents (fun (x : SimplexCategoryᵒᵖ) => U.cechIsoCechNerveApp hT x) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_hom_app
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(X : SimplexCategoryᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_inv_app
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
(X : SimplexCategoryᵒᵖ)
:
noncomputable def
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
:
U.cech.augmentOfIsTerminal (isTerminalIncl T hT) ≅ (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve
The Cech construction for FormalCoproduct is isomorphic
to the general Arrow.augmentedCechNerve construction applied to the morphism
to the terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_inv_left
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
:
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_left
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
:
@[simp]
theorem
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_right
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
:
noncomputable def
CategoryTheory.Limits.FormalCoproduct.extraDegeneracyCech
{C : Type u}
[Category.{v, u} C]
[HasFiniteProducts C]
(U : FormalCoproduct C)
{T : C}
(hT : IsTerminal T)
{i₀ : U.I}
(d : T ⟶ U.obj i₀)
:
(U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).ExtraDegeneracy
The Cech object of U : FormalCoproduct C has an extra degeneracy
when there is a morphism T ⟶ U.obj i₀ from the terminal object.
Equations
- One or more equations did not get rendered due to their size.