Theorems · Definition · algebraic geometry

TopCat.Presheaf.EtaleSpace.mk.noConfusion

{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} →
                  {P : Sort u_1} →
                    {base : ↑X} →
                      {germ : CategoryTheory.ToType (F.stalk base)} →
                        {base' : ↑X} →
                          {germ' : CategoryTheory.ToType (F.stalk base')} →
                            { base := base, germ := germ } = { base := base', germ := germ' } →
                              (base ≍ base' → germ ≍ germ' → P) → P

Defined in

Mathlib.Topology.Sheaves.EtaleSpace

Cited by

1 results in Mathlib

Foundations

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