Theorems · Theorem · algebraic geometry

TopCat.Presheaf.EtaleSpace.mk.inj

∀ {X : TopCat} {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {CC : C → Type v} {FC : C → C → Type w}
  {inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)} {inst_2 : CategoryTheory.ConcreteCategory C FC}
  {inst_3 : CategoryTheory.Limits.HasColimits C} {F : TopCat.Presheaf C X} {base : ↑X}
  {germ : CategoryTheory.ToType (F.stalk base)} {base_1 : ↑X} {germ_1 : CategoryTheory.ToType (F.stalk base_1)},
  { base := base, germ := germ } = { base := base_1, germ := germ_1 } → base = base_1 ∧ germ ≍ germ_1

Defined in

Mathlib.Topology.Sheaves.EtaleSpace

Cited by

1 results in Mathlib

Foundations

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