Loogle!
Result
Found 653 declarations mentioning CategoryTheory.PreZeroHypercover.X. Of these, only the first 200 are shown.
- CategoryTheory.PreZeroHypercover.X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (self : CategoryTheory.PreZeroHypercover S) (i : self.I₀) : C - CategoryTheory.PreZeroHypercover.empty_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) (a✝ : PEmpty.{w + 1}) : (CategoryTheory.PreZeroHypercover.empty S).X a✝ = a✝.elim - CategoryTheory.PreZeroHypercover.bind 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) : CategoryTheory.PreZeroHypercover T - CategoryTheory.PreZeroHypercover.f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (self : CategoryTheory.PreZeroHypercover S) (i : self.I₀) : self.X i ⟶ S - CategoryTheory.PreZeroHypercover.singleton_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (x✝ : PUnit.{w + 1}) : (CategoryTheory.PreZeroHypercover.singleton f).X x✝ = S - CategoryTheory.PreZeroHypercover.presieve₀_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : E.presieve₀ (E.f i) - CategoryTheory.PreZeroHypercover.sieve₀_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : E.sieve₀.arrows (E.f i) - CategoryTheory.PreZeroHypercover.add_X_none 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C} (f : T ⟶ S) : (E.add f).X none = T - CategoryTheory.PreZeroHypercover.pushforward_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X) (i : E.I₀) : (CategoryTheory.PreZeroHypercover.pushforward f E).X i = E.X i - CategoryTheory.PreZeroHypercover.pullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : CategoryTheory.PreZeroHypercover S - CategoryTheory.PreZeroHypercover.pullback₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : CategoryTheory.PreZeroHypercover S - CategoryTheory.PreZeroHypercover.restrictIndex_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'} (f : ι → E.I₀) (a✝ : ι) : (E.restrictIndex f).X a✝ = (E.X ∘ f) a✝ - CategoryTheory.Precoverage.ZeroHypercover.bind 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : J.ZeroHypercover T - CategoryTheory.PreZeroHypercover.sum_X_inl 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : (E.sum F).X (Sum.inl i) = E.X i - CategoryTheory.PreZeroHypercover.sum_X_inr 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) (i : F.I₀) : (E.sum F).X (Sum.inr i) = F.X i - CategoryTheory.PreZeroHypercover.add_X_some 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C} (f : T ⟶ S) (i : E.I₀) : (E.add f).X (some i) = E.X i - CategoryTheory.PreZeroHypercover.Hom.h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (self : E.Hom F) (i : E.I₀) : E.X i ⟶ F.X (self.s₀ i) - CategoryTheory.PreZeroHypercover.restrictIndex_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'} (f : ι → E.I₀) (i : ι) : (E.restrictIndex f).f i = E.f (f i) - CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (E : CategoryTheory.PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f] (i : E.I₀) : CategoryTheory.Limits.HasPullback (E.f i) f - CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (E : CategoryTheory.PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f] (i : E.I₀) : CategoryTheory.Limits.HasPullback f (E.f i) - CategoryTheory.PreZeroHypercover.inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : CategoryTheory.PreZeroHypercover T - CategoryTheory.PreZeroHypercover.map_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : (CategoryTheory.PreZeroHypercover.map F E).X i = F.obj (E.X i) - CategoryTheory.PreZeroHypercover.sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.PreZeroHypercover S - CategoryTheory.PreZeroHypercover.bind_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) : (E.bind F).I₀ = ((i : E.I₀) × (F i).I₀) - CategoryTheory.PreZeroHypercover.Hom.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (x✝ : E.I₀) : (CategoryTheory.PreZeroHypercover.Hom.id E).h₀ x✝ = CategoryTheory.CategoryStruct.id (E.X x✝) - CategoryTheory.PreZeroHypercover.sum_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) (F : CategoryTheory.PreZeroHypercover X) (a✝ : E.I₀ ⊕ F.I₀) : (E.sum F).X a✝ = Sum.elim E.X F.X a✝ - CategoryTheory.PreZeroHypercover.pullback₁_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.PreZeroHypercover.pullback₁ f E).I₀ = E.I₀ - CategoryTheory.PreZeroHypercover.pullback₂_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : (CategoryTheory.PreZeroHypercover.pullback₂ f E).I₀ = E.I₀ - CategoryTheory.PreZeroHypercover.add_f_nome 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C} (f : T ⟶ S) : (E.add f).f none = f - CategoryTheory.PreZeroHypercover.interFst 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).Hom E - CategoryTheory.PreZeroHypercover.interSnd 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).Hom F - CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) : (E.sigmaOfIsColimit hc).I₀ = PUnit.{w + 1} - CategoryTheory.PreZeroHypercover.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (x✝ : E.I₀) : (CategoryTheory.CategoryStruct.id E).h₀ x✝ = CategoryTheory.CategoryStruct.id (E.X x✝) - CategoryTheory.PreZeroHypercover.sumInl_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) (x✝ : E.I₀) : (E.sumInl F).h₀ x✝ = CategoryTheory.CategoryStruct.id (E.X x✝) - CategoryTheory.PreZeroHypercover.sumInr_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) (x✝ : F.I₀) : (E.sumInr F).h₀ x✝ = CategoryTheory.CategoryStruct.id (F.X x✝) - CategoryTheory.Precoverage.ZeroHypercover.pullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : J.ZeroHypercover S - CategoryTheory.Precoverage.ZeroHypercover.pullback₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : J.ZeroHypercover S - CategoryTheory.PreZeroHypercover.pushforward_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X) (i : E.I₀) : (CategoryTheory.PreZeroHypercover.pushforward f E).f i = CategoryTheory.CategoryStruct.comp (E.f i) f - CategoryTheory.PreZeroHypercover.inter_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).I₀ = (E.I₀ × F.1) - CategoryTheory.PreZeroHypercover.add_f_some 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C} (f : T ⟶ S) (i : E.I₀) : (E.add f).f (some i) = E.f i - CategoryTheory.PreZeroHypercover.reindex_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) (a✝ : ι) : (E.reindex e).X a✝ = E.X (e a✝) - CategoryTheory.PreZeroHypercover.sum_f_inl 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : (E.sum F).f (Sum.inl i) = E.f i - CategoryTheory.PreZeroHypercover.sum_f_inr 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) (i : F.I₀) : (E.sum F).f (Sum.inr i) = F.f i - CategoryTheory.PreZeroHypercover.interLift 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F) : G.Hom (E.inter F) - CategoryTheory.PreZeroHypercover.shrink_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) : E.shrink.I₀ = ↑(Set.range fun i => ⟨E.X i, E.f i⟩) - CategoryTheory.PreZeroHypercover.instIsIsoH₀Hom 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : E.I₀) : CategoryTheory.IsIso (e.hom.h₀ i) - CategoryTheory.PreZeroHypercover.instIsIsoH₀Inv 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryTheory.IsIso (e.inv.h₀ i) - CategoryTheory.PreZeroHypercover.pullback₁_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] (i : E.I₀) : (CategoryTheory.PreZeroHypercover.pullback₁ f E).X i = CategoryTheory.Limits.pullback f (E.f i) - CategoryTheory.PreZeroHypercover.pullback₂_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (i : E.I₀) : (CategoryTheory.PreZeroHypercover.pullback₂ f E).X i = CategoryTheory.Limits.pullback (E.f i) f - CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {X : C} {R : CategoryTheory.Presieve X} : R ∈ J.coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f - CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g] : CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback f g) - CategoryTheory.PreZeroHypercover.pullbackCoverOfRight 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)] : CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback f g) - CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] {T : C} (f : T ⟶ S) [J.IsStableUnderBaseChange] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).Small - CategoryTheory.PreZeroHypercover.map_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : (CategoryTheory.PreZeroHypercover.map F E).f i = F.map (E.f i) - CategoryTheory.PreZeroHypercover.pullbackIso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : CategoryTheory.PreZeroHypercover.pullback₁ f E ≅ CategoryTheory.PreZeroHypercover.pullback₂ f E - CategoryTheory.PreZeroHypercover.Hom.w₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (self : E.Hom F) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (self.h₀ i) (F.f (self.s₀ i)) = E.f i - CategoryTheory.PreZeroHypercover.presieve₀_pullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : (CategoryTheory.PreZeroHypercover.pullback₂ f E).presieve₀ = CategoryTheory.Presieve.pullbackArrows f E.presieve₀ - CategoryTheory.PreZeroHypercover.interSnd_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (i : (E.inter F).I₀) : (E.interSnd F).s₀ i = i.2 - CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (x✝ : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc).X x✝ = c.pt - CategoryTheory.PreZeroHypercover.restrictIndexHom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {ι : Type w'} (f : ι → E.I₀) (x✝ : (E.restrictIndex f).I₀) : (E.restrictIndexHom f).h₀ x✝ = CategoryTheory.CategoryStruct.id ((E.restrictIndex f).X x✝) - CategoryTheory.PreZeroHypercover.interFst_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (i : (E.inter F).I₀) : (E.interFst F).s₀ i = i.1 - CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : (E.bind F).toPreZeroHypercover = E.bind fun i => (F i).toPreZeroHypercover - CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pullback₁ f E.toPreZeroHypercover - CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pullback₂ f E.toPreZeroHypercover - CategoryTheory.Precoverage.ZeroHypercover.inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : J.ZeroHypercover T - CategoryTheory.PreZeroHypercover.ext 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {S : C} {x y : CategoryTheory.PreZeroHypercover S} (I₀ : x.I₀ = y.I₀) (X : x.X ≍ y.X) (f : x.f ≍ y.f) : x = y - CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g] : (E.pullbackCoverOfLeft f g).I₀ = E.I₀ - CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)] : (E.pullbackCoverOfRight f g).I₀ = E.I₀ - CategoryTheory.Precoverage.ZeroHypercover.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (x✝ : J.ZeroHypercover S) (x✝¹ : x✝.I₀) : (CategoryTheory.CategoryStruct.id x✝).h₀ x✝¹ = CategoryTheory.CategoryStruct.id (x✝.X x✝¹) - CategoryTheory.PreZeroHypercover.ext_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {S : C} {x y : CategoryTheory.PreZeroHypercover S} : x = y ↔ x.I₀ = y.I₀ ∧ x.X ≍ y.X ∧ x.f ≍ y.f - CategoryTheory.PreZeroHypercover.pullback₁_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] (x✝ : E.I₀) : (CategoryTheory.PreZeroHypercover.pullback₁ f E).f x✝ = CategoryTheory.Limits.pullback.fst f (E.f x✝) - CategoryTheory.PreZeroHypercover.pullback₂_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (x✝ : E.I₀) : (CategoryTheory.PreZeroHypercover.pullback₂ f E).f x✝ = CategoryTheory.Limits.pullback.snd (E.f x✝) f - CategoryTheory.PreZeroHypercover.Hom.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ → F.I₀) (h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i := by cat_disch) : E.Hom F - CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : J.ZeroHypercover (CategoryTheory.Limits.pullback f g) - CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] : J.ZeroHypercover (CategoryTheory.Limits.pullback f g) - CategoryTheory.PreZeroHypercover.presieve₀_sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) : (E.sigmaOfIsColimit hc).presieve₀ = CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f) - CategoryTheory.Presieve.preZeroHypercover_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (R : CategoryTheory.Presieve S) (i : ↑R.uncurry) : R.preZeroHypercover.X i = (↑i).fst - CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (x✝ : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc).f x✝ = CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f - CategoryTheory.PreZeroHypercover.reindex_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) (i : ι) : (E.reindex e).f i = E.f (e i) - CategoryTheory.PreZeroHypercover.interLift_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F) (i : G.I₀) : (CategoryTheory.PreZeroHypercover.interLift f g).s₀ i = (f.s₀ i, g.s₀ i) - CategoryTheory.PreZeroHypercover.shrink_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (i : ↑E.presieve₀.uncurry) : E.shrink.X i = (↑i).fst - CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover - CategoryTheory.PreZeroHypercover.inter_def 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : E.inter F = (E.bind fun i => CategoryTheory.PreZeroHypercover.pullback₁ (E.f i) F).reindex (Equiv.sigmaEquivProd E.I₀ F.1).symm - CategoryTheory.PreZeroHypercover.bind_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀) : (E.bind F).X ij = (F ij.fst).X ij.snd - CategoryTheory.PreZeroHypercover.Hom.ext 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {x y : E.Hom F} (s₀ : x.s₀ = y.s₀) (h₀ : x.h₀ ≍ y.h₀) : x = y - CategoryTheory.PreZeroHypercover.Hom.w₀_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (self : E.Hom F) (i : E.I₀) {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.h₀ i) (CategoryTheory.CategoryStruct.comp (F.f (self.s₀ i)) h) = CategoryTheory.CategoryStruct.comp (E.f i) h - CategoryTheory.PreZeroHypercover.sum_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) (F : CategoryTheory.PreZeroHypercover X) (x✝ : E.I₀ ⊕ F.I₀) : (E.sum F).f x✝ = match x✝ with | Sum.inl i => E.f i | Sum.inr i => F.f i - CategoryTheory.PreZeroHypercover.Hom.ext_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {x y : E.Hom F} : x = y ↔ x.s₀ = y.s₀ ∧ x.h₀ ≍ y.h₀ - CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g] (i : E.I₀) : (E.pullbackCoverOfLeft f g).X i = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g - CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)] (i : E.I₀) : (E.pullbackCoverOfRight f g).X i = CategoryTheory.Limits.pullback f (CategoryTheory.CategoryStruct.comp (E.f i) g) - CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) : CategoryTheory.CategoryStruct.comp (c.inj i) ((E.sigmaOfIsColimit hc).f r) = E.f i - CategoryTheory.PreZeroHypercover.pullbackIso_hom_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (a : (CategoryTheory.PreZeroHypercover.pullback₁ f E).I₀) : (CategoryTheory.PreZeroHypercover.pullbackIso f E).hom.s₀ a = id a - CategoryTheory.PreZeroHypercover.pullbackIso_inv_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (a : (CategoryTheory.PreZeroHypercover.pullback₂ f E).I₀) : (CategoryTheory.PreZeroHypercover.pullbackIso f E).inv.s₀ a = id a - CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : (E.pullbackCoverOfLeft f g).toPreZeroHypercover = E.pullbackCoverOfLeft f g - CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] : (E.pullbackCoverOfRight f g).toPreZeroHypercover = E.pullbackCoverOfRight f g - CategoryTheory.PreZeroHypercover.pushforwardIsoBind_hom_s₀_fst 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X) (a : (CategoryTheory.PreZeroHypercover.pushforward f E).I₀) : ((CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).hom.s₀ a).fst = PUnit.unit - CategoryTheory.PreZeroHypercover.pushforwardIsoBind_hom_s₀_snd 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X) (a : (CategoryTheory.PreZeroHypercover.pushforward f E).I₀) : ((CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).hom.s₀ a).snd = a - CategoryTheory.PreZeroHypercover.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : CategoryTheory.PreZeroHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i)) - CategoryTheory.PreZeroHypercover.Hom.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} (f : E.Hom F) (g : F.Hom G) (i : E.I₀) : (f.comp g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i)) - CategoryTheory.PreZeroHypercover.Hom.ext' 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {f g : E.Hom F} (hs : f.s₀ = g.s₀) (hh : ∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)) : f = g - CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.hom.h₀ i)) (E.f i) = F.f (e.hom.s₀ i) - CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.inv.h₀ i)) (F.f i) = E.f (e.inv.s₀ i) - CategoryTheory.PreZeroHypercover.pullbackCoverOfLeftIsoPullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.fst f g) (E.f i)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : E.pullbackCoverOfLeft f g ≅ CategoryTheory.PreZeroHypercover.pullback₁ (CategoryTheory.Limits.pullback.fst f g) E - CategoryTheory.PreZeroHypercover.pullbackCoverOfRightIsoPullback₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) (E.f i)] : E.pullbackCoverOfRight f g ≅ CategoryTheory.PreZeroHypercover.pullback₂ (CategoryTheory.Limits.pullback.snd f g) E - CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc).f r) h) = CategoryTheory.CategoryStruct.comp (E.f i) h - CategoryTheory.PreZeroHypercover.sumLift_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} (f : E.Hom G) (g : F.Hom G) (x✝ : (E.sum F).I₀) : (CategoryTheory.PreZeroHypercover.sumLift f g).h₀ x✝ = match x✝ with | Sum.inl i => f.h₀ i | Sum.inr i => g.h₀ i - CategoryTheory.PreZeroHypercover.Hom.ext'_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {f g : E.Hom F} : f = g ↔ ∃ (hs : f.s₀ = g.s₀), ∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯) - CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g] (i : E.I₀) : (E.pullbackCoverOfLeft f g).f i = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (E.f i) f) g f g (E.f i) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)] (i : E.I₀) : (E.pullbackCoverOfRight f g).f i = CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (E.f i) g) f g (CategoryTheory.CategoryStruct.id X) (E.f i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : E.I₀) {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.hom.h₀ i)) (CategoryTheory.CategoryStruct.comp (E.f i) h) = CategoryTheory.CategoryStruct.comp (F.f (e.hom.s₀ i)) h - CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.inv.h₀ i)) (CategoryTheory.CategoryStruct.comp (F.f i) h) = CategoryTheory.CategoryStruct.comp (E.f (e.inv.s₀ i)) h - CategoryTheory.PreZeroHypercover.pullbackIso_hom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (i : (CategoryTheory.PreZeroHypercover.pullback₁ f E).I₀) : (CategoryTheory.PreZeroHypercover.pullbackIso f E).hom.h₀ i = (CategoryTheory.Limits.pullbackSymmetry f (E.f i)).hom - CategoryTheory.PreZeroHypercover.hom_inv_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (e.inv.h₀ (e.hom.s₀ i)) = CategoryTheory.eqToHom ⋯ - CategoryTheory.PreZeroHypercover.inv_hom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (e.hom.h₀ (e.inv.s₀ i)) = CategoryTheory.eqToHom ⋯ - CategoryTheory.PreZeroHypercover.pullbackIso_inv_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (i : (CategoryTheory.PreZeroHypercover.pullback₂ f E).I₀) : (CategoryTheory.PreZeroHypercover.pullbackIso f E).inv.h₀ i = (CategoryTheory.Limits.pullbackSymmetry f (E.f i)).inv - CategoryTheory.Precoverage.ZeroHypercover.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (i : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i)) - CategoryTheory.PreZeroHypercover.bind_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀) : (E.bind F).f ij = CategoryTheory.CategoryStruct.comp ((F ij.fst).f ij.snd) (E.f ij.fst) - CategoryTheory.PreZeroHypercover.isoMk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) : E ≅ F - CategoryTheory.PreZeroHypercover.hom_inv_h₀_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : E.I₀) {Z : C} (h : E.X (e.inv.s₀ (e.hom.s₀ i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (CategoryTheory.CategoryStruct.comp (e.inv.h₀ (e.hom.s₀ i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h - CategoryTheory.PreZeroHypercover.inv_hom_h₀_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) {Z : C} (h : F.X (e.hom.s₀ (e.inv.s₀ i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (CategoryTheory.CategoryStruct.comp (e.hom.h₀ (e.inv.s₀ i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h - CategoryTheory.PreZeroHypercover.pushforwardIsoBind_hom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X) (i : (CategoryTheory.PreZeroHypercover.pushforward f E).I₀) : (CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).hom.h₀ i = CategoryTheory.CategoryStruct.id (E.X i) - CategoryTheory.PreZeroHypercover.isoMk_hom_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (a : E.I₀) : (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).hom.s₀ a = s₀ a - CategoryTheory.PreZeroHypercover.isoMk_inv_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (a : F.I₀) : (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ a = s₀.symm a - CategoryTheory.PreZeroHypercover.pushforwardIsoBind_inv_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X) (i : ((CategoryTheory.PreZeroHypercover.singleton f).bind fun x => E).I₀) : (CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).inv.h₀ i = CategoryTheory.CategoryStruct.id (E.X i.snd) - CategoryTheory.PreZeroHypercover.isoMk_hom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (i : E.I₀) : (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).hom.h₀ i = (h₀ i).hom - CategoryTheory.PreZeroHypercover.isoMk_inv_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (i : F.I₀) : (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (h₀ (s₀.symm i)).inv - CategoryTheory.PreZeroHypercover.inter_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (a✝ : E.I₀ × F.1) : (E.inter F).X a✝ = CategoryTheory.Limits.pullback (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm a✝).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm a✝).snd) - CategoryTheory.PreZeroHypercover.interLift_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F) (i : G.I₀) : (CategoryTheory.PreZeroHypercover.interLift f g).h₀ i = CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯ - CategoryTheory.PreZeroHypercover.interFst_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (x✝ : (E.inter F).I₀) : (E.interFst F).h₀ x✝ = CategoryTheory.Limits.pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).snd) - CategoryTheory.PreZeroHypercover.interSnd_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (x✝ : (E.inter F).I₀) : (E.interSnd F).h₀ x✝ = CategoryTheory.Limits.pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).snd) - CategoryTheory.PreZeroHypercover.inter_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) (F : CategoryTheory.PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (i : E.I₀ × F.1) : (E.inter F).f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm i).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm i).snd)) (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm i).fst) - CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : J.Cover X) (f : S.Arrow) : S.preOneHypercover.X f = f.Y - CategoryTheory.PreOneHypercover.p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (self : CategoryTheory.PreOneHypercover S) ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : self.Y j ⟶ self.X i₁ - CategoryTheory.PreOneHypercover.p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (self : CategoryTheory.PreOneHypercover S) ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : self.Y j ⟶ self.X i₂ - CategoryTheory.PreZeroHypercover.refineOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) : CategoryTheory.PreOneHypercover X - CategoryTheory.PreOneHypercover.multicospanIndex_left 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.multicospanShape.L) : (E.multicospanIndex F).left i = F.obj (Opposite.op (E.X i)) - CategoryTheory.PreOneHypercover.sieve₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) : CategoryTheory.Sieve W - CategoryTheory.PreZeroHypercover.toPreOneHypercover_Y 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (i j : E.I₀) (x✝ : PUnit.{u_2 + 1}) : E.toPreOneHypercover.Y x✝ = CategoryTheory.Limits.pullback (E.f i) (E.f j) - CategoryTheory.instHasPullbacksRefineOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) : (E.refineOneHypercover F).HasPullbacks - CategoryTheory.PreZeroHypercover.refineOneHypercover_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) : (E.refineOneHypercover F).toPreZeroHypercover = E - CategoryTheory.PreOneHypercover.Hom.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (x✝ : E.I₀) : (CategoryTheory.PreOneHypercover.Hom.id E).h₀ x✝ = CategoryTheory.CategoryStruct.id (E.X x✝) - CategoryTheory.PreOneHypercover.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (x✝ : E.I₀) : (CategoryTheory.CategoryStruct.id E).h₀ x✝ = CategoryTheory.CategoryStruct.id (E.X x✝) - CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (x✝ x✝¹ : E.I₀) (x✝² : PUnit.{u_2 + 1}) : E.toPreOneHypercover.p₁ x✝² = CategoryTheory.Limits.pullback.fst (E.f x✝) (E.f x✝¹) - CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (x✝ x✝¹ : E.I₀) (x✝² : PUnit.{u_2 + 1}) : E.toPreOneHypercover.p₂ x✝² = CategoryTheory.Limits.pullback.snd (E.f x✝) (E.f x✝¹) - CategoryTheory.PreOneHypercover.sieve₁' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (i₁ i₂ : E.I₀) [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] : CategoryTheory.Sieve (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂)) - CategoryTheory.PreZeroHypercover.refineOneHypercover_I₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) : (E.refineOneHypercover F).I₁ i j = (F i j).I₀ - CategoryTheory.PreOneHypercover.instIsIsoH₀Hom 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F) (i : E.I₀) : CategoryTheory.IsIso (e.hom.h₀ i) - CategoryTheory.PreOneHypercover.instIsIsoH₀Inv 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryTheory.IsIso (e.inv.h₀ i) - CategoryTheory.PreOneHypercover.sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : CategoryTheory.PreOneHypercover S - CategoryTheory.PreOneHypercover.instUniqueLMulticospanShapeSigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : Unique (E.sigmaOfIsColimit hc hd).multicospanShape.L - CategoryTheory.PreOneHypercover.instUniqueRMulticospanShapeSigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : Unique (E.sigmaOfIsColimit hc hd).multicospanShape.R - CategoryTheory.PreOneHypercover.w 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (self : CategoryTheory.PreOneHypercover S) ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : CategoryTheory.CategoryStruct.comp (self.p₁ j) (self.f i₁) = CategoryTheory.CategoryStruct.comp (self.p₂ j) (self.f i₂) - CategoryTheory.PreOneHypercover.toPullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (j : E.I₁ i₁ i₂) : E.Y j ⟶ CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂) - CategoryTheory.PreOneHypercover.pullback_sieve₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) {T : C} (f : T ⟶ W) : CategoryTheory.Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (CategoryTheory.CategoryStruct.comp f p₁) (CategoryTheory.CategoryStruct.comp f p₂) - CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (x✝ : E.I₀) : (CategoryTheory.CategoryStruct.id E).h₀ x✝ = CategoryTheory.CategoryStruct.id (E.X x✝) - CategoryTheory.PreOneHypercover.sigmaOfIsColimit_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : (E.sigmaOfIsColimit hc hd).toPreZeroHypercover = E.sigmaOfIsColimit hc - CategoryTheory.PreZeroHypercover.refineOneHypercover_Y 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) (k : (F i j).I₀) : (E.refineOneHypercover F).Y k = (F i j).X k - CategoryTheory.PreOneHypercover.multifork_ι 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀) : (E.multifork F).ι i = F.map (E.f i).op - CategoryTheory.PreOneHypercover.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) (I₁ : toPreZeroHypercover.I₀ → toPreZeroHypercover.I₀ → Type w) (Y : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → I₁ i₁ i₂ → C) (p₁ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₁) (p₂ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₂) (w : ∀ ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ (j : I₁ i₁ i₂), CategoryTheory.CategoryStruct.comp (p₁ j) (toPreZeroHypercover.f i₁) = CategoryTheory.CategoryStruct.comp (p₂ j) (toPreZeroHypercover.f i₂)) : CategoryTheory.PreOneHypercover S - CategoryTheory.PreOneHypercover.sigmaOfIsColimit_Y 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (x✝ x✝¹ : (E.sigmaOfIsColimit hc).I₀) (x✝² : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc hd).Y x✝² = d.pt - CategoryTheory.PreZeroHypercover.sieve₁'_refineOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) : (E.refineOneHypercover F).sieve₁' i j = (F i j).sieve₀ - CategoryTheory.GrothendieckTopology.OneHypercover.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (toPreOneHypercover : CategoryTheory.PreOneHypercover S) (mem₀ : toPreOneHypercover.sieve₀ ∈ J S) (mem₁ : ∀ (i₁ i₂ : toPreOneHypercover.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover.X i₁) (p₂ : W ⟶ toPreOneHypercover.X i₂), CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover.f i₂) → toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W) : J.OneHypercover S - CategoryTheory.GrothendieckTopology.OneHypercover.mem₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (self : J.OneHypercover S) (i₁ i₂ : self.I₀) ⦃W : C⦄ (p₁ : W ⟶ self.X i₁) (p₂ : W ⟶ self.X i₂) (w : CategoryTheory.CategoryStruct.comp p₁ (self.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (self.f i₂)) : self.sieve₁ p₁ p₂ ∈ J W - CategoryTheory.PreOneHypercover.inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : CategoryTheory.PreOneHypercover S - CategoryTheory.PreOneHypercover.toPullback_fst 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂) : CategoryTheory.CategoryStruct.comp (E.toPullback k) (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) = E.p₁ k - CategoryTheory.PreOneHypercover.toPullback_snd 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂) : CategoryTheory.CategoryStruct.comp (E.toPullback k) (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂)) = E.p₂ k - CategoryTheory.PreOneHypercover.interFst 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).Hom E - CategoryTheory.PreOneHypercover.interSnd 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).Hom F - CategoryTheory.PreOneHypercover.interLift 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] {G : CategoryTheory.PreOneHypercover S} (f : G.Hom E) (g : G.Hom F) : G.Hom (E.inter F) - CategoryTheory.PreOneHypercover.inter_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover - CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (i₁ i₂ : E.I₀) [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] : E.sieve₁' i₁ i₂ = E.sieve₁ (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂)) - CategoryTheory.PreOneHypercover.sieve₁_apply 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) (Z : C) (g : Z ⟶ W) : (E.sieve₁ p₁ p₂).arrows g = ∃ j h, CategoryTheory.CategoryStruct.comp g p₁ = CategoryTheory.CategoryStruct.comp h (E.p₁ j) ∧ CategoryTheory.CategoryStruct.comp g p₂ = CategoryTheory.CategoryStruct.comp h (E.p₂ j) - CategoryTheory.PreOneHypercover.interFst_toHom 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.interFst F).toHom = E.interFst F.toPreZeroHypercover - CategoryTheory.PreOneHypercover.interSnd_toHom 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.interSnd F).toHom = E.interSnd F.toPreZeroHypercover - CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) (w : CategoryTheory.CategoryStruct.comp p₁ (E.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (E.f i₂)) : E.sieve₁ p₁ p₂ = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) - CategoryTheory.GrothendieckTopology.OneHypercover.mk' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (E : CategoryTheory.PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ ∈ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))) : J.OneHypercover S - CategoryTheory.PreZeroHypercover.refineOneHypercover_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) (k : (F i j).I₀) : (E.refineOneHypercover F).p₁ k = CategoryTheory.CategoryStruct.comp ((F i j).f k) (CategoryTheory.Limits.pullback.fst (E.f i) (E.f j)) - CategoryTheory.PreZeroHypercover.refineOneHypercover_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) (k : (F i j).I₀) : (E.refineOneHypercover F).p₂ k = CategoryTheory.CategoryStruct.comp ((F i j).f k) (CategoryTheory.Limits.pullback.snd (E.f i) (E.f j)) - CategoryTheory.PreOneHypercover.toPullback_fst_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂) {Z : C} (h : E.X i₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.toPullback k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) h) = CategoryTheory.CategoryStruct.comp (E.p₁ k) h - CategoryTheory.PreOneHypercover.toPullback_snd_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂) {Z : C} (h : E.X i₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.toPullback k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂)) h) = CategoryTheory.CategoryStruct.comp (E.p₂ k) h - CategoryTheory.GrothendieckTopology.OneHypercover.mk'_toPreOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (E : CategoryTheory.PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ ∈ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))) : (CategoryTheory.GrothendieckTopology.OneHypercover.mk' E mem₀ mem₁').toPreOneHypercover = E - CategoryTheory.PreOneHypercover.Hom.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (i : E.I₀) : (f.comp g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i)) - CategoryTheory.PreOneHypercover.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : CategoryTheory.PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i)) - CategoryTheory.PreOneHypercover.Hom.w₁₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (F.p₁ (self.s₁ k)) = CategoryTheory.CategoryStruct.comp (E.p₁ k) (self.h₀ i) - CategoryTheory.PreOneHypercover.Hom.w₁₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (F.p₂ (self.s₁ k)) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (self.h₀ j) - CategoryTheory.GrothendieckTopology.OneHypercover.inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} [CategoryTheory.Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : J.OneHypercover S - CategoryTheory.PreOneHypercover.isLimitSigmaOfIsColimitEquiv 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.X i)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F] : CategoryTheory.Limits.IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ CategoryTheory.Limits.IsLimit (E.multifork F) - CategoryTheory.PreOneHypercover.inter_I₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) : (E.inter F).I₁ i j = (E.I₁ i.1 j.1 × F.I₁ i.2 j.2) - CategoryTheory.GrothendieckTopology.OneHypercover.inter_toPreOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} [CategoryTheory.Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).toPreOneHypercover = E.inter F.toPreOneHypercover - CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (i₁ i₂ : E.I₀) [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] : E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂)) - CategoryTheory.PreOneHypercover.interFst_s₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j) : (E.interFst F).s₁ k = k.1 - CategoryTheory.PreOneHypercover.interSnd_s₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j) : (E.interSnd F).s₁ k = k.2 - CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (CategoryTheory.CategoryStruct.comp (F.p₁ (self.s₁ k)) h) = CategoryTheory.CategoryStruct.comp (E.p₁ k) (CategoryTheory.CategoryStruct.comp (self.h₀ i) h) - CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (CategoryTheory.CategoryStruct.comp (F.p₂ (self.s₁ k)) h) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (CategoryTheory.CategoryStruct.comp (self.h₀ j) h) - CategoryTheory.PreOneHypercover.hom_inv_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (e.inv.h₀ (e.hom.s₀ i)) = CategoryTheory.eqToHom ⋯ - CategoryTheory.PreOneHypercover.inv_hom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (e.hom.h₀ (e.inv.s₀ i)) = CategoryTheory.eqToHom ⋯ - CategoryTheory.PreZeroHypercover.ext_of_isSeparatedFor 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)} {S : C} (E : CategoryTheory.PreZeroHypercover S) (h : CategoryTheory.Presieve.IsSeparatedFor P E.presieve₀) {x y : P.obj (Opposite.op S)} (hi : ∀ (i : E.I₀), (CategoryTheory.ConcreteCategory.hom (P.map (E.f i).op)) x = (CategoryTheory.ConcreteCategory.hom (P.map (E.f i).op)) y) : x = y - CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv (E.p₁ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k)) = CategoryTheory.CategoryStruct.comp (E.p₁ k) (CategoryTheory.eqToHom ⋯) - CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv (E.p₂ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k)) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (CategoryTheory.eqToHom ⋯) - CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A} (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c) (F.obj.map (E.f i₀).op) = c.ι i₀
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.You can filter for definitions vs theorems: Using
⊢ (_ : Type _)finds all definitions which provide data while⊢ (_ : Prop)finds all theorems (and definitions of proofs).
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision 69fae59