Theorems · Inductive type · algebraic geometry

CategoryTheory.PresheafOfGroups.OneCocycle

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ GrpCat → {I : Type w'} → (I → C) → Type (max (max (max u v) w) w')

A 1-cocycle is a 1-cochain which satisfies the cocycle condition.

Defined in: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Cited by: 10 results in Mathlib
Foundations: Depth 16 from the axioms · uses propext, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement · cited by 32,673
CategoryTheory.Functorstatement · cited by 16,252
Oppositestatement · cited by 8,081
GrpCatstatement · cited by 146

Cited by19

Results whose statement or proof uses this declaration.

CategoryTheory.PresheafOfGroups.OneCocycle.toOneCochainstatement and proof · cited by 5
CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologousstatement and proof · cited by 3
CategoryTheory.PresheafOfGroups.OneCocycle.classstatement and proof · cited by 2
CategoryTheory.PresheafOfGroups.OneCocycle.ev_transstatement and proof · cited by 2
CategoryTheory.PresheafOfGroups.OneCocycle.equivalence_isCohomologousstatement and proof · cited by 1
CategoryTheory.PresheafOfGroups.OneCocycle.ev_reflstatement and proof · cited by 1
CategoryTheory.PresheafOfGroups.OneCocycle.mk.injstatement · cited by 1
CategoryTheory.PresheafOfGroups.OneCocycle.mk.noConfusionstatement · cited by 1
CategoryTheory.PresheafOfGroups.OneCocycle.casesOnstatement and proof · cited by 0
CategoryTheory.PresheafOfGroups.OneCocycle.class_eq_iffstatement and proof · cited by 0
CategoryTheory.PresheafOfGroups.OneCocycle.ctorIdxstatement and proof · cited by 0
CategoryTheory.PresheafOfGroups.OneCocycle.ev_symmstatement and proof · cited by 0