Theorems · Theorem · category theory

TopCat.Sheaf.isIso_iff_isIso_basis

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X}
  {F G : TopCat.Sheaf C X},
  TopologicalSpace.Opens.IsBasis (Set.range B) →
    ∀ {φ : F ⟶ G}, (∀ (i : ι), CategoryTheory.IsIso (φ.hom.app (Opposite.op (B i)))) → CategoryTheory.IsIso φ

Defined in

Mathlib.Topology.Sheaves.SheafCondition.Sites

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category