Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.mk.noConfusion

{S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    {inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀} →
      {inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰} →
        {P : Sort u_3} →
          {functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme} →
            {natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰} →
              {equifibered : CategoryTheory.NatTrans.Equifibered natTrans} →
                {functor' : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme} →
                  {natTrans' : functor' ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰} →
                    {equifibered' : CategoryTheory.NatTrans.Equifibered natTrans'} →
                      { functor := functor, natTrans := natTrans, equifibered := equifibered } =
                          { functor := functor', natTrans := natTrans', equifibered := equifibered' } →
                        (functor ≍ functor' → natTrans ≍ natTrans' → P) → P

Defined in

Mathlib.AlgebraicGeometry.RelativeGluing

Cited by

1 results in Mathlib

Foundations

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