Loogle!

Result

Found 486 declarations mentioning CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover. Of these, only the first 200 are shown.

CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (self : J.ZeroHypercover S) : CategoryTheory.PreZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.instSmallOfSmallI₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [Small.{w', w} E.I₀] : E.Small
CategoryTheory.Precoverage.ZeroHypercover.reindex 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : CategoryTheory.Precoverage.ZeroHypercover.Small.Index E → E.I₀
CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) [K.HasPullbacks] {X Y : C} (E : K.ZeroHypercover X) (f : Y ⟶ X) : E.presieve₀.HasPullbacks f
CategoryTheory.Precoverage.ZeroHypercover.mem₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (self : J.ZeroHypercover S) : self.presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.bind 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.isoMk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : E ≅ F
CategoryTheory.Precoverage.ZeroHypercover.reindex_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).toPreZeroHypercover = E.reindex e
CategoryTheory.Precoverage.ZeroHypercover.sum_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} [J.IsStableUnderSup] (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) : (E.sum F).toPreZeroHypercover = E.sum F.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.weaken_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {K L : CategoryTheory.Precoverage C} {X : C} (E : K.ZeroHypercover X) (h : K ≤ L) : (E.weaken h).toPreZeroHypercover = E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : E.restrictIndexOfSmall.toPreZeroHypercover = E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)
CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C} {E : J.ZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (e : E.toPreZeroHypercover ≅ F) : F.presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.le_of_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.Precoverage C} (h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X) : J ≤ K
CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : (E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)).presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.singleton_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} (f : S ⟶ T) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings T) : (CategoryTheory.Precoverage.ZeroHypercover.singleton f hf).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.singleton f
CategoryTheory.Precoverage.ZeroHypercover.id_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (x✝ : J.ZeroHypercover S) (a : x✝.I₀) : (CategoryTheory.CategoryStruct.id x✝).s₀ a = a
CategoryTheory.Precoverage.ZeroHypercover.pullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.pullback₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [self : E.Small] : ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.Small.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E : J.ZeroHypercover S} (exists_restrictIndex_mem : ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S) : E.Small
CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {X : C} {R : CategoryTheory.Presieve X} : R ∈ J.coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] {T : C} (f : T ⟶ S) [J.IsStableUnderBaseChange] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).Small
CategoryTheory.Precoverage.ZeroHypercover.pushforward_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] [J.HasIsos] {X Y : C} (f : X ⟶ Y) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings Y) (E : J.ZeroHypercover X) : (CategoryTheory.Precoverage.ZeroHypercover.pushforward f hf E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pushforward f E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.add 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S) : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.map_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Precoverage D} (F : CategoryTheory.Functor C D) (E : J.ZeroHypercover S) (h : J ≤ CategoryTheory.Precoverage.comap F K) : (CategoryTheory.Precoverage.ZeroHypercover.map F E h).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : (E.bind F).toPreZeroHypercover = E.bind fun i => (F i).toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pullback₁ f E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pullback₂ f E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (x✝ : J.ZeroHypercover S) (x✝¹ : x✝.I₀) : (CategoryTheory.CategoryStruct.id x✝).h₀ x✝¹ = CategoryTheory.CategoryStruct.id (x✝.X x✝¹)
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : J.ZeroHypercover (CategoryTheory.Limits.pullback f g)
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] : J.ZeroHypercover (CategoryTheory.Limits.pullback f g)
CategoryTheory.Precoverage.ZeroHypercover.isoMk_hom 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : (CategoryTheory.Precoverage.ZeroHypercover.isoMk e).hom = e.hom
CategoryTheory.Precoverage.ZeroHypercover.isoMk_inv 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : (CategoryTheory.Precoverage.ZeroHypercover.isoMk e).inv = e.inv
CategoryTheory.Precoverage.ZeroHypercover.add_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S) : (E.add f hf).toPreZeroHypercover = E.add f
CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.comp_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (a✝ : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : (E.pullbackCoverOfLeft f g).toPreZeroHypercover = E.pullbackCoverOfLeft f g
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] : (E.pullbackCoverOfRight f g).toPreZeroHypercover = E.pullbackCoverOfRight f g
CategoryTheory.Precoverage.ZeroHypercover.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (i : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.HasPullbacks] : J.toGrothendieck.OneHypercover S
CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (E : J.OneHypercover S) : E.toZeroHypercover.toPreZeroHypercover = E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.HasPullbacks] : E.toOneHypercover.toPreOneHypercover = E.toPreOneHypercover
CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small 📋 Mathlib.CategoryTheory.Sites.Coverage
{C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.Small] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), CategoryTheory.Presieve.IsSheafFor P E.presieve₀
CategoryTheory.Precoverage.ZeroHypercover.morphismProperty 📋 Mathlib.CategoryTheory.Sites.MorphismProperty
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Precoverage C} {X : C} {E : K.ZeroHypercover X} (i : E.I₀) : K.morphismProperty (E.f i)
AlgebraicGeometry.Scheme.AffineCover.cover_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) : 𝒰.cover.I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.Cover.idx 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x : ↥X) : 𝒰.I₀
AlgebraicGeometry.Scheme.Cover.nonempty_of_nonempty 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K] [Nonempty ↥X] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) : Nonempty 𝒰.I₀
AlgebraicGeometry.Scheme.AffineCover.cover_X 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (j : 𝒰.I₀) : 𝒰.cover.X j = AlgebraicGeometry.Spec (𝒰.X j)
AlgebraicGeometry.Scheme.Cover.ulift_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) : 𝒰.ulift.I₀ = ↥X
AlgebraicGeometry.Scheme.Cover.map_prop 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (i : 𝒰.I₀) : P (𝒰.f i)
AlgebraicGeometry.Scheme.AffineCover.cover_f 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (j : 𝒰.I₀) : 𝒰.cover.f j = 𝒰.f j
AlgebraicGeometry.Scheme.coverOfIsIso_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (AlgebraicGeometry.Scheme.coverOfIsIso f).I₀ = PUnit.{v + 1}
AlgebraicGeometry.Scheme.Cover.changeProp 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)) : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage Q) X
AlgebraicGeometry.Scheme.coverOfIsIso_X 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : PUnit.{v + 1}) : (AlgebraicGeometry.Scheme.coverOfIsIso f).X x✝ = X
AlgebraicGeometry.Scheme.Cover.ulift_X 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (x : ↥X) : 𝒰.ulift.X x = 𝒰.X (𝒰.idx x)
AlgebraicGeometry.Scheme.Cover.add_toPreZeroHypercover 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : Y ⟶ X) (hf : P f := by infer_instance) : (𝒰.add f hf).toPreZeroHypercover = 𝒰.add f
AlgebraicGeometry.Scheme.coverOfIsIso_f 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : PUnit.{v + 1}) : (AlgebraicGeometry.Scheme.coverOfIsIso f).f x✝ = f
AlgebraicGeometry.Scheme.Cover.pushforwardIso_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : (𝒰.pushforwardIso f).I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.Cover.ulift_f 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (x : ↥X) : 𝒰.ulift.f x = 𝒰.f (𝒰.idx x)
AlgebraicGeometry.Scheme.Cover.pushforwardIso_X 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : 𝒰.I₀) : (𝒰.pushforwardIso f).X x✝ = 𝒰.X x✝
AlgebraicGeometry.Scheme.Cover.pullbackHom 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X) (i : 𝒰.toPreZeroHypercover.1) [∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i
AlgebraicGeometry.Scheme.Cover.pullbackHom_map 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X) [∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (𝒰.f i) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f
AlgebraicGeometry.Scheme.Cover.mkOfCovers_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).I₀ = J
AlgebraicGeometry.Scheme.Cover.mkOfCovers_X 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) (a✝ : J) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).X a✝ = obj a✝
AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X) [∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (CategoryTheory.CategoryStruct.comp f h)
AlgebraicGeometry.Scheme.Cover.mkOfCovers_f 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) (j : J) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).f j = map j
AlgebraicGeometry.Scheme.Cover.exists_eq 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x : ↥X) : ∃ i y, (𝒰.f i) y = x
AlgebraicGeometry.Scheme.Cover.iUnion_range 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover K X) : ⋃ i, Set.range ⇑(𝒰.f i) = Set.univ
AlgebraicGeometry.Scheme.Cover.covers 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x : ↥X) : x ∈ Set.range ⇑(𝒰.f (𝒰.idx x))
AlgebraicGeometry.Scheme.Cover.copy 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X
AlgebraicGeometry.Scheme.Cover.copy_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) : (𝒰.copy J obj map e₁ e₂ h).I₀ = J
AlgebraicGeometry.Scheme.Cover.copy_X 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) (a✝ : J) : (𝒰.copy J obj map e₁ e₂ h).X a✝ = obj a✝
AlgebraicGeometry.Scheme.Cover.copy_f 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) (i : J) : (𝒰.copy J obj map e₁ e₂ h).f i = map i
AlgebraicGeometry.Scheme.Cover.pushforwardIso_f 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : 𝒰.I₀) : (𝒰.pushforwardIso f).f x✝ = CategoryTheory.CategoryStruct.comp (𝒰.f x✝) f
AlgebraicGeometry.Scheme.affineBasisCoverRing 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.I₀) : CommRingCat
AlgebraicGeometry.Scheme.affineOpenCover_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) : X.affineOpenCover.I₀ = X.affineCover.I₀
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_I₀ 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover) : 𝒰.openCover.I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀) : 𝒰.openCover.X j = AlgebraicGeometry.Spec (𝒰.X j)
AlgebraicGeometry.Scheme.affineBasisCover_obj 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.I₀) : X.affineBasisCover.X i = AlgebraicGeometry.Spec (X.affineBasisCoverRing i)
AlgebraicGeometry.Scheme.instFintypeI₀FiniteSubcover 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] : Fintype 𝒰.finiteSubcover.I₀
AlgebraicGeometry.Scheme.instIsOpenImmersionF 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (i : 𝒰.I₀) : AlgebraicGeometry.IsOpenImmersion (𝒰.f i)
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀) : 𝒰.openCover.f j = 𝒰.f j
AlgebraicGeometry.Scheme.affineOpenCover_f 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) (i : X.affineCover.I₀) : X.affineOpenCover.f i = X.affineCover.f i
AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : TopologicalSpace.IsOpenCover fun i => AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i)
AlgebraicGeometry.Scheme.OpenCover.compactSpace 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [Finite 𝒰.I₀] [H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)] : CompactSpace ↥X
AlgebraicGeometry.Scheme.instIsOpenImmersionH₀ 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {𝒱 : X.OpenCover} (f : 𝒰 ⟶ 𝒱) (i : 𝒰.I₀) : AlgebraicGeometry.IsOpenImmersion (f.h₀ i)
AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : ⨆ i, AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i) = ⊤
AlgebraicGeometry.Scheme.affineBasisCover_is_basis 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) : TopologicalSpace.IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
AlgebraicGeometry.Scheme.affineOpenCover_idx 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) (x : ↥X) : X.affineOpenCover.idx x = ⋯.choose
AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] (x : ↥⋯.choose) : 𝒰.finiteSubcover.X x = 𝒰.X (AlgebraicGeometry.Scheme.Cover.idx 𝒰 ↑x)
AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] (x : ↥⋯.choose) : 𝒰.finiteSubcover.f x = 𝒰.f (AlgebraicGeometry.Scheme.Cover.idx 𝒰 ↑x)
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i ≅ (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).X i.snd
AlgebraicGeometry.Scheme.OpenCover.ext_elem 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.I₀), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) f = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) g) : f = g
AlgebraicGeometry.Scheme.zero_of_zero_cover 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.I₀), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) s = 0) : s = 0
AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) [Finite 𝒰.I₀] (h : ∀ (i : 𝒰.I₀), IsNilpotent ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) s)) : IsNilpotent s
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f i) = AlgebraicGeometry.Scheme.Cover.pullbackHom (𝒰.X i.fst).affineCover (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) i.snd
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.affineRefinement.openCover.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f i) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.pullbackHom (𝒰.X i.fst).affineCover (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) i.snd) h
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst) h)
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd) ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
AlgebraicGeometry.Scheme.affineBasisCover_map_range 📋 Mathlib.AlgebraicGeometry.Cover.Open
(X : AlgebraicGeometry.Scheme) (x : ↥X) (r : ↑⋯.choose) : Set.range ⇑(X.affineBasisCover.f ⟨x, r⟩) = ⇑(X.affineCover.f x) '' (PrimeSpectrum.basicOpen r).carrier
AlgebraicGeometry.Scheme.OpenCover.restrict_I₀ 📋 Mathlib.AlgebraicGeometry.Restrict
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) : (𝒰.restrict U).I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_I₀ 📋 Mathlib.AlgebraicGeometry.Restrict
{s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) : (X.openCoverOfIsOpenCover U hU).I₀ = s
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_X 📋 Mathlib.AlgebraicGeometry.Restrict
{s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (i : s) : (X.openCoverOfIsOpenCover U hU).X i = ↑(U i)
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_f 📋 Mathlib.AlgebraicGeometry.Restrict
{s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (i : s) : (X.openCoverOfIsOpenCover U hU).f i = (U i).ι
AlgebraicGeometry.Scheme.OpenCover.restrict_X 📋 Mathlib.AlgebraicGeometry.Restrict
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) (x✝ : 𝒰.I₀) : (𝒰.restrict U).X x✝ = ↑((TopologicalSpace.Opens.map (𝒰.f x✝).base).obj U)
AlgebraicGeometry.Scheme.OpenCover.restrict_f 📋 Mathlib.AlgebraicGeometry.Restrict
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) (x✝ : 𝒰.I₀) : (𝒰.restrict U).f x✝ = 𝒰.f x✝ ∣_ U
AlgebraicGeometry.Scheme.isAffine_affineOpenCover 📋 Mathlib.AlgebraicGeometry.AffineScheme
(X : AlgebraicGeometry.Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.I₀) : AlgebraicGeometry.IsAffine (𝒰.openCover.X i)
AlgebraicGeometry.Scheme.isAffine_affineBasisCover 📋 Mathlib.AlgebraicGeometry.AffineScheme
(X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.I₀) : AlgebraicGeometry.IsAffine (X.affineBasisCover.X i)
AlgebraicGeometry.Scheme.isAffine_affineCover 📋 Mathlib.AlgebraicGeometry.AffineScheme
(X : AlgebraicGeometry.Scheme) (i : X.affineCover.I₀) : AlgebraicGeometry.IsAffine (X.affineCover.X i)
AlgebraicGeometry.instIsAffineXSchemeCover 📋 Mathlib.AlgebraicGeometry.AffineScheme
(P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P S) (i : 𝒰.I₀) : AlgebraicGeometry.IsAffine (𝒰.cover.X i)
AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (i : (AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).I₀) : AlgebraicGeometry.IsAffine ((AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).X i)
AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover 📋 Mathlib.AlgebraicGeometry.AffineScheme
(X : AlgebraicGeometry.Scheme) [CompactSpace ↥X] (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)] (i : 𝒰.finiteSubcover.I₀) : AlgebraicGeometry.IsAffine (𝒰.finiteSubcover.X i)
CategoryTheory.MorphismProperty.IsLocalAtSource.of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : P f
CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.RespectsIso] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : P.IsLocalAtSource K
CategoryTheory.MorphismProperty.of_zeroHypercover_source 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) [𝒰.Small] (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : P f
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) {X' : C} (i : 𝒰.I₀) {fst : X' ⟶ X} {snd : X' ⟶ 𝒰.X i} (h : CategoryTheory.IsPullback fst snd f (𝒰.f i)) (hf : P f) : P snd
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) : P f
CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.IsStableUnderBaseChange] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) : P.IsLocalAtTarget K
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.RespectsIso] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) : P.IsLocalAtTarget K
CategoryTheory.MorphismProperty.of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [𝒰.Small] (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) : P f
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_small 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.RespectsIso] [K.Small] (h₁ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), P f → ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) (h₂ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), (∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) → P f) : P.IsLocalAtSource K
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.RespectsIso] [K.Small] (h₁ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y), P f → ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) (h₂ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y), (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) : P.IsLocalAtTarget K
CategoryTheory.eq_of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) {J : CategoryTheory.Precoverage C} (𝒰 : J.ZeroHypercover S) [J.IsStableUnderBaseChange] [(CategoryTheory.MorphismProperty.isomorphisms C).IsLocalAtTarget J] (H : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) f (CategoryTheory.CategoryStruct.id (𝒰.X i)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ = CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) : f = g
AlgebraicGeometry.Scheme.GlueData.openCover_I₀ 📋 Mathlib.AlgebraicGeometry.Gluing
(D : AlgebraicGeometry.Scheme.GlueData) : D.openCover.I₀ = D.J
AlgebraicGeometry.Scheme.Cover.gluedCover_J 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).J = 𝒰.I₀
AlgebraicGeometry.Scheme.GlueData.openCover_X 📋 Mathlib.AlgebraicGeometry.Gluing
(D : AlgebraicGeometry.Scheme.GlueData) (a✝ : D.J) : D.openCover.X a✝ = D.U a✝
AlgebraicGeometry.Scheme.Cover.gluedCover_U 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).U i = 𝒰.X i
AlgebraicGeometry.Scheme.GlueData.openCover_f 📋 Mathlib.AlgebraicGeometry.Gluing
(D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) : D.openCover.f i = D.ι i
AlgebraicGeometry.Scheme.Cover.ι_fromGlued 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).ι x) (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰) = 𝒰.f x
AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).ι x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰) h) = CategoryTheory.CategoryStruct.comp (𝒰.f x) h
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_I₀ 📋 Mathlib.AlgebraicGeometry.Gluing
{J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover F).I₀ = J
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_X 📋 Mathlib.AlgebraicGeometry.Gluing
{J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] (a✝ : J) : (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover F).X a✝ = F.obj a✝
AlgebraicGeometry.Scheme.Cover.hom_ext 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f₁ f₂ : X ⟶ Y) (h : ∀ (x : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f x) f₁ = CategoryTheory.CategoryStruct.comp (𝒰.f x) f₂) : f₁ = f₂
AlgebraicGeometry.Scheme.Cover.gluedCover_V 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x✝ : 𝒰.I₀ × 𝒰.I₀) : (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).V x✝ = match x✝ with | (x, y) => CategoryTheory.Limits.pullback (𝒰.f x) (𝒰.f y)
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_f 📋 Mathlib.AlgebraicGeometry.Gluing
{J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] (j : J) : (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover F).f j = CategoryTheory.Limits.colimit.ι F j
AlgebraicGeometry.Scheme.Cover.gluedCover_f 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x✝ x✝¹ : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).f x✝ x✝¹ = CategoryTheory.Limits.pullback.fst (𝒰.f x✝) (𝒰.f x✝¹)
AlgebraicGeometry.Scheme.Cover.gluedCover_t 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x✝ x✝¹ : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).t x✝ x✝¹ = (CategoryTheory.Limits.pullbackSymmetry (𝒰.f x✝) (𝒰.f x✝¹)).hom
AlgebraicGeometry.Scheme.Cover.glueMorphisms 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) (hf : ∀ (x y : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) : X ⟶ Y
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) (hf : ∀ (x y : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) (x : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (𝒰.f x) (AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf) = f x
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) (hf : ∀ (x y : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) (x : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.f x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf) h) = CategoryTheory.CategoryStruct.comp (f x) h
AlgebraicGeometry.Scheme.Cover.gluedCoverT' 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)) ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))
AlgebraicGeometry.Scheme.Cover.gluedCover_t' 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).t' x y z = AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y))
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f z))
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y))
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f x))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) h)
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X z ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f z)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f z)) h)
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) h)
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X x ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f x)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) h)
AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x) (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 z x y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 z x y) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))))) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))
AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd 📋 Mathlib.AlgebraicGeometry.Gluing
{X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 z x y) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))))) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀ 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_I₀ 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_I₀ 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).I₀ = 𝒰.I₀
AlgebraicGeometry.Scheme.Pullback.gluing 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : AlgebraicGeometry.Scheme.GlueData
AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : CategoryTheory.Limits.HasPullback f g
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀ 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).I₀ = (𝒰X.I₀ × 𝒰Y.I₀)
AlgebraicGeometry.Scheme.Pullback.p1 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued ⟶ X
AlgebraicGeometry.Scheme.Pullback.p2 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued ⟶ Y
AlgebraicGeometry.Scheme.Pullback.v 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀) : AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Pullback.gluing_J 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).J = 𝒰.I₀
AlgebraicGeometry.Scheme.Pullback.gluedLift 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : s.pt ⟶ (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued
AlgebraicGeometry.Scheme.Pullback.t 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀) : AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j ⟶ AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g j i
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_X 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).X i = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).X i = CategoryTheory.Limits.pullback f (CategoryTheory.CategoryStruct.comp (𝒰.f i) g)
AlgebraicGeometry.Scheme.Pullback.gluedIsLimit 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) ⋯)
AlgebraicGeometry.Scheme.Pullback.t_id 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i i = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i i)
AlgebraicGeometry.Scheme.Pullback.diagonalCover 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) : (CategoryTheory.Limits.pullback.diagonalObj f).OpenCover
AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) : (CategoryTheory.Limits.pullback.diagonalObj f).Opens
AlgebraicGeometry.Scheme.Pullback.p_comm 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) f = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) g
AlgebraicGeometry.Scheme.Pullback.gluing_t 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).t i j = AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j
AlgebraicGeometry.Scheme.Pullback.gluing_U 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).U i = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
AlgebraicGeometry.Scheme.Pullback.gluedLift_p1 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s) (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) = s.fst
AlgebraicGeometry.Scheme.Pullback.gluedLift_p2 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s) (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) = s.snd
AlgebraicGeometry.Scheme.Pullback.gluing_ι 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (j : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j = CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram j
AlgebraicGeometry.Scheme.Pullback.fV 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀) : AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j ⟶ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
AlgebraicGeometry.Scheme.Pullback.gluing_V 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (x✝ : 𝒰.I₀ × 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V x✝ = match x✝ with | (i, j) => AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i) ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).X i = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (CategoryTheory.Limits.pullback.snd g (𝒰.f i))
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).f i = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g f g (𝒰.f i) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).f i = CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (𝒰.f i) g) f g (CategoryTheory.CategoryStruct.id X) (𝒰.f i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) (i : Z.affineCover.I₀) : CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f Z.affineCover).f i) f) g
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.I₀ × 𝒰Y.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).X ij = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰X.f ij.1) f) (CategoryTheory.CategoryStruct.comp (𝒰Y.f ij.2) g)
AlgebraicGeometry.Scheme.isPullback_of_openCover 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z W : AlgebraicGeometry.Scheme} (fWX : W ⟶ X) (fWY : W ⟶ Y) (fXZ : X ⟶ Z) (fYZ : Y ⟶ Z) (𝒰 : X.OpenCover) (H : ∀ (i : 𝒰.toPreZeroHypercover.1), CategoryTheory.IsPullback (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 fWX i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i) fWY) (CategoryTheory.CategoryStruct.comp (𝒰.f i) fXZ) fYZ) : CategoryTheory.IsPullback fWX fWY fXZ fYZ
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).f i = CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (CategoryTheory.Limits.pullback.snd g (𝒰.f i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.f i)) (CategoryTheory.Limits.pullback.fst g (𝒰.f i)) (𝒰.f i) ⋯ ⋯
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) = (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j) ⟶ AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g j i
AlgebraicGeometry.Scheme.Pullback.gluing_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (x✝ x✝¹ : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).f x✝ x✝¹ = CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f x✝) f) g) (𝒰.f x✝)) (𝒰.f x✝¹)
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) = CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.I₀ × 𝒰Y.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).f ij = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰X.f ij.1) f) (CategoryTheory.CategoryStruct.comp (𝒰Y.f ij.2) g) f g (𝒰X.f ij.1) (𝒰Y.f ij.2) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram i) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59