Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.mk.inj

∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} {inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀}
  {inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰}
  {functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme}
  {natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰}
  {equifibered : CategoryTheory.NatTrans.Equifibered natTrans}
  {functor_1 : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme}
  {natTrans_1 : functor_1 ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰}
  {equifibered_1 : CategoryTheory.NatTrans.Equifibered natTrans_1},
  { functor := functor, natTrans := natTrans, equifibered := equifibered } =
      { functor := functor_1, natTrans := natTrans_1, equifibered := equifibered_1 } →
    functor = functor_1 ∧ natTrans ≍ natTrans_1

Defined in

Mathlib.AlgebraicGeometry.RelativeGluing

Cited by

1 results in Mathlib

Foundations

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