Theorems · Definition · category theory

CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso

{C : Type u} →
  [inst : 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) → E.Y ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k) ≅ E.Y k

If i = i' and j = j' this is the isomorphism between the 1-component at congrIndexOneOfEq k : E.I₁ i' j' and the 1-component at k : E.I₁ i j. Note: This isomorphism could also be constructed inline from eqToIso. We only use eqToIso directly to construct isomorphisms E.Y k ≅ E.Y k' where k k' : E.I₁ i j and whenever k : E.I₁ i j and k' : E.I₁ i' j' have to be related we use congrIndexOneOfEqIso, possibly combined with an additional eqToIso instead. The reason for this is that the lemmas around eqToHom_naturality are hard to apply in the case where there is a mismatch in the type of the index.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

24 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category