Skip to content

Instantly share code, notes, and snippets.

@ericrbg

ericrbg/output.txt Secret

Created April 5, 2022 09:49
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ericrbg/e78cd06e2930763a07fd2f22c14a67d0 to your computer and use it in GitHub Desktop.
Save ericrbg/e78cd06e2930763a07fd2f22c14a67d0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
output.txt
C:\Users\ericr\repos\mathlib\src\all.lean:1:0: error: cyclic import: C:\Users\ericr\repos\mathlib\src\run_tests.lean
C:\Users\ericr\repos\mathlib\src\all.lean:2334:0: error: invalid import: run_tests
could not resolve import: run_tests
C:\Users\ericr\repos\mathlib\src\run_tests.lean:2:0: error: invalid import: run_tests
could not resolve import: run_tests
WARNING types not equal
<def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_right : Π {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.SheafedSpace C} {Y : algebraic_geometry.SheafedSpace C} {Z : algebraic_geometry.SheafedSpace C}
(f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f],
category_theory.limits.preserves_limit (category_theory.limits.cospan g f)
(algebraic_geometry.SheafedSpace.forget C) := λ {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.limits.has_products C] {X : algebraic_geometry.SheafedSpace C}
{Y : algebraic_geometry.SheafedSpace C} {Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z)
[H : algebraic_geometry.SheafedSpace.is_open_immersion f],
category_theory.limits.preserves_pullback_symmetry (algebraic_geometry.SheafedSpace.forget C) f g>
WARNING types not equal
<def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom : Π
{X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme)
(f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f ⟶ Y := λ
{X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme)
(f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom Y.to_LocallyRingedSpace f>
WARNING types not equal
<def algebraic_geometry.Scheme.open_cover.finite_subcover : Π {X : algebraic_geometry.Scheme},
X.open_cover →
Π [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)], X.open_cover := λ
{X : algebraic_geometry.Scheme} (𝒰 : X.open_cover)
[H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)],
let t : finset ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) := _.some
in {J := ↥t,
obj := λ (x : ↥t), 𝒰.obj (𝒰.f x.val),
map := λ (x : ↥t), 𝒰.map (𝒰.f x.val),
f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), Exists.some _,
covers := _,
is_open := _}>
WARNING types not equal
<def category_theory.triangulated.pretriangulated.triangulated_functor.inhabited : Π (C : Type u₁)
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_zero_object C]
[_inst_3 : category_theory.has_shift C ℤ] [_inst_4 : category_theory.preadditive C]
[_inst_5 : ∀ (n : ℤ), (category_theory.shift_functor C n).additive]
[_inst_11 : category_theory.triangulated.pretriangulated C],
inhabited (category_theory.triangulated.pretriangulated.triangulated_functor C C) := λ (C : Type u₁)
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_zero_object C]
[_inst_3 : category_theory.has_shift C ℤ] [_inst_4 : category_theory.preadditive C]
[_inst_5 : ∀ (n : ℤ), (category_theory.shift_functor C n).additive]
[_inst_11 : category_theory.triangulated.pretriangulated C],
{default := {to_triangulated_functor_struct := {to_functor := {obj := λ (X : C), X,
map := λ (_x _x_1 : C) (f : _x ⟶ _x_1), f,
map_id' := _,
map_comp' := _},
comm_shift := category_theory.iso.refl
(category_theory.shift_functor C 1 ⋙
{obj := λ (X : C), X,
map := λ (_x _x_1 : C) (f : _x ⟶ _x_1), f,
map_id' := _,
map_comp' := _})},
map_distinguished' := _}}>
WARNING types not equal
<def category_theory.exp_terminal_iso_self : Π {C : Type u} [_inst_1 : category_theory.category C] {X : C}
[_inst_2 : category_theory.limits.has_finite_products C] [_inst_4 : category_theory.exponentiable (⊤_ C)],
(category_theory.exp (⊤_ C)).obj X ≅ X := λ {C : Type u} [_inst_1 : category_theory.category C] {X : C}
[_inst_2 : category_theory.limits.has_finite_products C] [_inst_4 : category_theory.exponentiable (⊤_ C)],
category_theory.yoneda.ext ((category_theory.exp (⊤_ C)).obj X) X
(λ (Y : C) (f : Y ⟶ (category_theory.exp (⊤_ C)).obj X),
(category_theory.limits.prod.left_unitor Y).inv ≫ category_theory.cartesian_closed.uncurry f)
(λ (Y : C) (f : Y ⟶ X),
category_theory.cartesian_closed.curry ((category_theory.limits.prod.left_unitor Y).hom ≫ f))
category_theory.exp_terminal_iso_self._proof_9
category_theory.exp_terminal_iso_self._proof_10
category_theory.exp_terminal_iso_self._proof_11>
WARNING types not equal
<theorem category_theory.limits.image_map.map_ι : ∀ {C : Type u} [_inst_1 : category_theory.category C]
{f g : category_theory.arrow C} [_inst_2 : category_theory.limits.has_image f.hom]
[_inst_3 : category_theory.limits.has_image g.hom] {sq : f ⟶ g} (self : category_theory.limits.image_map sq),
self.map ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right := λ
(C : Type u) [_inst_1 : category_theory.category C] (f g : category_theory.arrow C)
[_inst_2 : category_theory.limits.has_image f.hom] [_inst_3 : category_theory.limits.has_image g.hom] (sq : f ⟶ g)
(self : category_theory.limits.image_map sq), [category_theory.limits.image_map.map_ι' self]>
WARNING types not equal
<theorem category_theory.limits.image_map.map_ι : ∀ {C : Type u} [_inst_1 : category_theory.category C]
{f g : category_theory.arrow C} [_inst_2 : category_theory.limits.has_image f.hom]
[_inst_3 : category_theory.limits.has_image g.hom] {sq : f ⟶ g} (self : category_theory.limits.image_map sq),
self.map ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right := λ
(C : Type u) [_inst_1 : category_theory.category C] (f g : category_theory.arrow C)
[_inst_2 : category_theory.limits.has_image f.hom] [_inst_3 : category_theory.limits.has_image g.hom] (sq : f ⟶ g)
(self : category_theory.limits.image_map sq), [category_theory.limits.image_map.map_ι' self]>
WARNING types not equal
<def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom : Π {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f ⟶ Y := λ {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f], f>
WARNING types not equal
<def algebraic_geometry.stalk_function_field_algebra : Π (X : algebraic_geometry.Scheme)
[_inst_1 : irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)]
(x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)),
algebra ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x) ↥(X.function_field) := λ
(X : algebraic_geometry.Scheme)
[_inst_1 : irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)]
(x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)),
ring_hom.to_algebra (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk_specializes _)>
WARNING types not equal
<def category_theory.limits.coprod_comparison_nat_iso : Π {C : Type u} [_inst_1 : category_theory.category C]
{D : Type u₂} [_inst_2 : category_theory.category D] (F : C ⥤ D)
[_inst_7 : category_theory.limits.has_binary_coproducts C] [_inst_8 : category_theory.limits.has_binary_coproducts D]
(A : C) [_inst_9 : ∀ (B : C), category_theory.is_iso (category_theory.limits.coprod_comparison F A B)],
F ⋙ category_theory.limits.coprod.functor.obj (F.obj A) ≅ category_theory.limits.coprod.functor.obj A ⋙ F := λ
{C : Type u} [_inst_1 : category_theory.category C] {D : Type u₂} [_inst_2 : category_theory.category D] (F : C ⥤ D)
[_inst_7 : category_theory.limits.has_binary_coproducts C] [_inst_8 : category_theory.limits.has_binary_coproducts D]
(A : C) [_inst_9 : ∀ (B : C), category_theory.is_iso (category_theory.limits.coprod_comparison F A B)],
{hom := category_theory.limits.coprod_comparison_nat_trans F A,
inv := (category_theory.as_iso
{app := λ (B : C), category_theory.limits.coprod_comparison F A B, naturality' := _}).inv,
hom_inv_id' := _,
inv_hom_id' := _}>
WARNING types not equal
<def homology_zero_zero : Π {V : Type u} [_inst_1 : category_theory.category V]
[_inst_2 : category_theory.limits.has_zero_morphisms V] {A B C : V} [_inst_6 : category_theory.limits.has_zero_object V]
[_inst_7 : category_theory.limits.has_image 0]
[_inst_8 : category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_3)],
homology 0 0 homology_zero_zero._proof_5 ≅ B := λ {V : Type u} [_inst_1 : category_theory.category V]
[_inst_2 : category_theory.limits.has_zero_morphisms V] {A B C : V} [_inst_6 : category_theory.limits.has_zero_object V]
[_inst_7 : category_theory.limits.has_image 0]
[_inst_8 : category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_8)],
{hom := homology.desc 0 0 homology_zero_zero._proof_12 (category_theory.limits.kernel_subobject 0).arrow
homology_zero_zero._proof_13,
inv := category_theory.inv (category_theory.limits.kernel_subobject 0).arrow ≫
homology.π 0 0 homology_zero_zero._proof_15,
hom_inv_id' := _,
inv_hom_id' := _}>
WARNING types not equal
<def algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace : Π
{X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.LocallyRingedSpace)
(f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
algebraic_geometry.LocallyRingedSpace := λ {X : algebraic_geometry.PresheafedSpace CommRing}
(Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
{to_SheafedSpace := algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y.to_SheafedSpace f H,
local_ring := _}>
WARNING types not equal
<def category_theory.abelian.is_colimit_coimage : Π {C : Type u₁} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g],
category_theory.limits.is_colimit
(category_theory.limits.cokernel_cofork.of_π (category_theory.abelian.coimage.π g) _) := λ {C : Type u₁}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[h : category_theory.exact f g],
category_theory.limits.is_colimit.of_π (category_theory.abelian.coimage.π g) _
(λ (W : C) (u : Y ⟶ W) (hu : f ≫ u = 0),
category_theory.limits.cokernel.desc (category_theory.limits.kernel.ι g) u _)
_
_>
WARNING types not equal
<def category_theory.abelian.is_limit_image' : Π {C : Type u₁} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g],
category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι (category_theory.limits.image.ι f) _) := λ
{C : Type u₁} [_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y)
(g : Y ⟶ Z) [h : category_theory.exact f g],
category_theory.limits.is_kernel.iso_kernel g (category_theory.limits.image.ι f)
(category_theory.abelian.is_limit_image f g)
(category_theory.abelian.image_iso_image f).symm
_>
WARNING types not equal
<def category_theory.biprod.gaussian : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.preadditive C] [_inst_3 : category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
[_inst_4 : category_theory.is_iso (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)],
Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂),
L.hom ≫ f ≫ R.hom =
category_theory.limits.biprod.map (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)
g₂₂ := λ {C : Type u} [_inst_1 : category_theory.category C] [_inst_2 : category_theory.preadditive C]
[_inst_3 : category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C}
(f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
[_inst_4 : category_theory.is_iso (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)],
let this : Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂),
L.hom ≫
category_theory.biprod.of_components
(category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)
(category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd)
(category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst)
(category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) ≫
R.hom =
category_theory.limits.biprod.map
(category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)
g₂₂ :=
category_theory.biprod.gaussian' (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)
(category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd)
(category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst)
(category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd)
in _.mpr (_.mp this)>
WARNING types not equal
<def category_theory.injective_resolution.ι : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] (Z : C) [_inst_3 : category_theory.has_injective_resolution Z],
(cochain_complex.single₀ C).obj Z ⟶ category_theory.injective_resolution Z := λ {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] (Z : C)
[_inst_3 : category_theory.has_injective_resolution Z], _.some.ι>
WARNING types not equal
<def category_theory.limits.prod_comparison_nat_iso : Π {C : Type u} [_inst_1 : category_theory.category C]
{D : Type u₂} [_inst_2 : category_theory.category D] (F : C ⥤ D)
[_inst_7 : category_theory.limits.has_binary_products C] [_inst_8 : category_theory.limits.has_binary_products D]
(A : C) [_inst_9 : ∀ (B : C), category_theory.is_iso (category_theory.limits.prod_comparison F A B)],
category_theory.limits.prod.functor.obj A ⋙ F ≅ F ⋙ category_theory.limits.prod.functor.obj (F.obj A) := λ
{C : Type u} [_inst_1 : category_theory.category C] {D : Type u₂} [_inst_2 : category_theory.category D] (F : C ⥤ D)
[_inst_7 : category_theory.limits.has_binary_products C] [_inst_8 : category_theory.limits.has_binary_products D]
(A : C) [_inst_9 : ∀ (B : C), category_theory.is_iso (category_theory.limits.prod_comparison F A B)],
{hom := category_theory.limits.prod_comparison_nat_trans F A,
inv := (category_theory.as_iso
{app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _}).inv,
hom_inv_id' := _,
inv_hom_id' := _}>
WARNING types not equal
<def category_theory.nat_trans.right_derived : Π {C : Type u} [_inst_1 : category_theory.category C] {D : Type u_1}
[_inst_2 : category_theory.category D] [_inst_3 : category_theory.abelian C]
[_inst_4 : category_theory.has_injective_resolutions C] [_inst_5 : category_theory.abelian D] {F G : C ⥤ D}
[_inst_6 : F.additive] [_inst_7 : G.additive], (F ⟶ G) → Π (n : ℕ), F.right_derived n ⟶ G.right_derived n := λ
{C : Type u} [_inst_1 : category_theory.category C] {D : Type u_1} [_inst_2 : category_theory.category D]
[_inst_3 : category_theory.abelian C] [_inst_4 : category_theory.has_injective_resolutions C]
[_inst_5 : category_theory.abelian D] {F G : C ⥤ D} [_inst_6 : F.additive] [_inst_7 : G.additive] (α : F ⟶ G)
(n : ℕ),
category_theory.whisker_left (category_theory.injective_resolutions C)
(category_theory.whisker_right (category_theory.nat_trans.map_homotopy_category α (complex_shape.up ℕ))
(homotopy_category.homology_functor D (complex_shape.up ℕ) n))>
WARNING types not equal
<def algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_left : Π {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.SheafedSpace C} {Y : algebraic_geometry.SheafedSpace C} {Z : algebraic_geometry.SheafedSpace C}
(f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f],
category_theory.creates_limit (category_theory.limits.cospan f g)
algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace := λ {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.limits.has_products C] {X : algebraic_geometry.SheafedSpace C}
{Y : algebraic_geometry.SheafedSpace C} {Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z)
[H : algebraic_geometry.SheafedSpace.is_open_immersion f],
category_theory.creates_limit_of_fully_faithful_of_iso
(algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y category_theory.limits.pullback.snd)
(category_theory.eq_to_iso _ ≪≫
category_theory.limits.has_limit.iso_of_nat_iso
(category_theory.limits.diagram_iso_cospan
(category_theory.limits.cospan f g ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)).symm)>
WARNING types not equal
<def category_theory.abelian.is_colimit_image : Π {C : Type u₁} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g],
category_theory.limits.is_colimit
(category_theory.limits.cokernel_cofork.of_π (category_theory.limits.factor_thru_image g) _) := λ {C : Type u₁}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[h : category_theory.exact f g],
category_theory.limits.is_cokernel.cokernel_iso f (category_theory.limits.factor_thru_image g)
(category_theory.abelian.is_colimit_coimage f g)
(category_theory.abelian.coimage_iso_image' g)
_>
WARNING types not equal
<def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme : Π
{X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme)
(f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f], algebraic_geometry.Scheme := λ
{X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme)
(f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme
(algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y.to_LocallyRingedSpace f)
_>
WARNING types not equal
<def algebraic_geometry.Scheme.J.fintype : Π {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover)
[H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)],
fintype 𝒰.finite_subcover.J := λ {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover)
[H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)],
id (finset.subtype.fintype _.some)>
WARNING types not equal
<def category_theory.injective_resolution.desc : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] {X Y : C},
(X ⟶ Y) →
Π [_inst_3 : category_theory.has_injective_resolution X] [_inst_4 : category_theory.has_injective_resolution Y],
category_theory.injective_resolution X ⟶ category_theory.injective_resolution Y := λ {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] {X Y : C} (f : X ⟶ Y)
[_inst_3 : category_theory.has_injective_resolution X] [_inst_4 : category_theory.has_injective_resolution Y],
category_theory.InjectiveResolution.desc f _.some _.some>
WARNING types not equal
<def category_theory.injective_resolution.desc : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] {X Y : C},
(X ⟶ Y) →
Π [_inst_3 : category_theory.has_injective_resolution X] [_inst_4 : category_theory.has_injective_resolution Y],
category_theory.injective_resolution X ⟶ category_theory.injective_resolution Y := λ {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] {X Y : C} (f : X ⟶ Y)
[_inst_3 : category_theory.has_injective_resolution X] [_inst_4 : category_theory.has_injective_resolution Y],
category_theory.InjectiveResolution.desc f _.some _.some>
WARNING types not equal
<def is_alg_closure.equiv_of_algebraic : Π (K : Type u_1) (J : Type u_2) [_inst_2 : field K] [_inst_3 : field J]
(L : Type v) (M : Type w) [_inst_5 : field L] [_inst_6 : field M] [_inst_10 : algebra K M]
[_inst_11 : is_alg_closure K M] [_inst_19 : algebra K J] [_inst_20 : algebra J L] [_inst_21 : is_alg_closure J L]
[_inst_22 : algebra K L] [_inst_23 : is_scalar_tower K J L], algebra.is_algebraic K J → (L ≃ₐ[K] M) := λ
(K : Type u_1) (J : Type u_2) [_inst_2 : field K] [_inst_3 : field J] (L : Type v) (M : Type w) [_inst_5 : field L]
[_inst_6 : field M] [_inst_10 : algebra K M] [_inst_11 : is_alg_closure K M] [_inst_19 : algebra K J]
[_inst_20 : algebra J L] [_inst_21 : is_alg_closure J L] [_inst_22 : algebra K L] [_inst_23 : is_scalar_tower K J L]
(hKJ : algebra.is_algebraic K J), is_alg_closure.equiv_of_algebraic' K J L M _>
WARNING types not equal
<def is_alg_closure.equiv_of_algebraic : Π (K : Type u_1) (J : Type u_2) [_inst_2 : field K] [_inst_3 : field J]
(L : Type v) (M : Type w) [_inst_5 : field L] [_inst_6 : field M] [_inst_10 : algebra K M]
[_inst_11 : is_alg_closure K M] [_inst_19 : algebra K J] [_inst_20 : algebra J L] [_inst_21 : is_alg_closure J L]
[_inst_22 : algebra K L] [_inst_23 : is_scalar_tower K J L], algebra.is_algebraic K J → (L ≃ₐ[K] M) := λ
(K : Type u_1) (J : Type u_2) [_inst_2 : field K] [_inst_3 : field J] (L : Type v) (M : Type w) [_inst_5 : field L]
[_inst_6 : field M] [_inst_10 : algebra K M] [_inst_11 : is_alg_closure K M] [_inst_19 : algebra K J]
[_inst_20 : algebra J L] [_inst_21 : is_alg_closure J L] [_inst_22 : algebra K L] [_inst_23 : is_scalar_tower K J L]
(hKJ : algebra.is_algebraic K J), is_alg_closure.equiv_of_algebraic' K J L M _>
WARNING types not equal
<def category_theory.preserves_limit_of_Lan_presesrves_limit : Π {C D : Type u}
[_inst_4 : category_theory.small_category C] [_inst_5 : category_theory.small_category D] (F : C ⥤ D) (J : Type u)
[_inst_6 : category_theory.small_category J]
[_inst_7 : category_theory.limits.preserves_limits_of_shape J (category_theory.Lan F.op)],
category_theory.limits.preserves_limits_of_shape J F := λ {C D : Type u} [_inst_4 : category_theory.small_category C]
[_inst_5 : category_theory.small_category D] (F : C ⥤ D) (J : Type u) [_inst_6 : category_theory.small_category J]
[_inst_7 : category_theory.limits.preserves_limits_of_shape J (category_theory.Lan F.op)],
category_theory.limits.preserves_limits_of_shape_of_reflects_of_preserves F category_theory.yoneda>
WARNING types not equal
<def category_theory.functor.final.colimit_comp_coyoneda_iso : Π {C : Type v}
[_inst_1 : category_theory.small_category C] {D : Type v} [_inst_2 : category_theory.small_category D] (F : C ⥤ D)
[_inst_3 : F.final] (d : D)
[_inst_5 :
category_theory.is_iso (category_theory.limits.colimit.pre (category_theory.coyoneda.obj (opposite.op d)) F)],
category_theory.limits.colimit (F ⋙ category_theory.coyoneda.obj (opposite.op d)) ≅ punit := λ {C : Type v}
[_inst_1 : category_theory.small_category C] {D : Type v} [_inst_2 : category_theory.small_category D] (F : C ⥤ D)
[_inst_3 : F.final] (d : D)
[_inst_5 :
category_theory.is_iso (category_theory.limits.colimit.pre (category_theory.coyoneda.obj (opposite.op d)) F)],
category_theory.as_iso (category_theory.limits.colimit.pre (category_theory.coyoneda.obj (opposite.op d)) F) ≪≫
category_theory.coyoneda.colimit_coyoneda_iso (opposite.op d)>
WARNING types not equal
<def function_field.class_number : Π (Fq F : Type) [_inst_1 : field Fq] [_inst_2 : fintype Fq] [_inst_3 : field F]
[_inst_4 : algebra (polynomial Fq) F] [_inst_5 : algebra (ratfunc Fq) F]
[_inst_6 : is_scalar_tower (polynomial Fq) (ratfunc Fq) F] [_inst_7 : function_field Fq F]
[_inst_8 : is_separable (ratfunc Fq) F], ℕ := λ (Fq F : Type) [_inst_1 : field Fq] [_inst_2 : fintype Fq]
[_inst_3 : field F] [_inst_4 : algebra (polynomial Fq) F] [_inst_5 : algebra (ratfunc Fq) F]
[_inst_6 : is_scalar_tower (polynomial Fq) (ratfunc Fq) F] [_inst_7 : function_field Fq F]
[_inst_8 : is_separable (ratfunc Fq) F], fintype.card (class_group ↥(function_field.ring_of_integers Fq F) F)>
WARNING types not equal
<def algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_right : Π {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.SheafedSpace C} {Y : algebraic_geometry.SheafedSpace C} {Z : algebraic_geometry.SheafedSpace C}
(f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f],
category_theory.creates_limit (category_theory.limits.cospan g f)
algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace := λ {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.limits.has_products C] {X : algebraic_geometry.SheafedSpace C}
{Y : algebraic_geometry.SheafedSpace C} {Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z)
[H : algebraic_geometry.SheafedSpace.is_open_immersion f],
category_theory.creates_limit_of_fully_faithful_of_iso
(algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y category_theory.limits.pullback.fst)
(category_theory.eq_to_iso _ ≪≫
category_theory.limits.has_limit.iso_of_nat_iso
(category_theory.limits.diagram_iso_cospan
(category_theory.limits.cospan g f ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)).symm)>
WARNING types not equal
<def category_theory.abelian.is_limit_image : Π {C : Type u₁} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g],
category_theory.limits.is_limit
(category_theory.limits.kernel_fork.of_ι (category_theory.abelian.image.ι f) _) := λ {C : Type u₁}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[h : category_theory.exact f g],
category_theory.limits.is_limit.of_ι (category_theory.abelian.image.ι f) _
(λ (W : C) (u : W ⟶ Y) (hu : u ≫ g = 0),
category_theory.limits.kernel.lift (category_theory.limits.cokernel.π f) u _)
_
_>
WARNING types not equal
<def category_theory.injective_resolution : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.abelian C] (Z : C) [_inst_3 : category_theory.has_injective_resolution Z],
cochain_complex C ℕ := λ {C : Type u} [_inst_1 : category_theory.category C] [_inst_2 : category_theory.abelian C]
(Z : C) [_inst_3 : category_theory.has_injective_resolution Z], _.some.cocomplex>
WARNING types not equal
<def category_theory.functor.right_derived_obj_injective_succ : Π {C : Type u} [_inst_1 : category_theory.category C]
{D : Type u_1} [_inst_2 : category_theory.category D] [_inst_3 : category_theory.abelian C]
[_inst_4 : category_theory.has_injective_resolutions C] [_inst_5 : category_theory.abelian D] (F : C ⥤ D)
[_inst_6 : F.additive] (n : ℕ) (X : C) [_inst_7 : category_theory.injective X],
(F.right_derived (n + 1)).obj X ≅ 0 := λ {C : Type u} [_inst_1 : category_theory.category C] {D : Type u_1}
[_inst_2 : category_theory.category D] [_inst_3 : category_theory.abelian C]
[_inst_4 : category_theory.has_injective_resolutions C] [_inst_5 : category_theory.abelian D] (F : C ⥤ D)
[_inst_6 : F.additive] (n : ℕ) (X : C) [_inst_7 : category_theory.injective X],
F.right_derived_obj_iso (n + 1) (category_theory.InjectiveResolution.self X) ≪≫
(homology_functor D (complex_shape.up ℕ) (n + 1)).map_iso
((cochain_complex.single₀_map_homological_complex F).app X) ≪≫
(cochain_complex.homology_functor_succ_single₀ D n).app (F.obj X)>
WARNING types not equal
<def category_theory.injective.exact.desc : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.limits.has_zero_morphisms C] [_inst_3 : category_theory.limits.has_images Cᵒᵖ]
[_inst_4 : category_theory.limits.has_equalizers Cᵒᵖ] {J Q R S : C} [_inst_5 : category_theory.injective J]
(h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S) [_inst_6 : category_theory.exact g.op f.op], f ≫ h = 0 → (S ⟶ J) := λ
{C : Type u} [_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_zero_morphisms C]
[_inst_3 : category_theory.limits.has_images Cᵒᵖ] [_inst_4 : category_theory.limits.has_equalizers Cᵒᵖ]
{J Q R S : C} [_inst_5 : category_theory.injective J] (h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S)
[_inst_6 : category_theory.exact g.op f.op] (w : f ≫ h = 0), (category_theory.exact.lift h.op g.op f.op _).unop>
WARNING types not equal
<def category_theory.functor.right_derived_obj_injective_zero : Π {C : Type u} [_inst_1 : category_theory.category C]
{D : Type u_1} [_inst_2 : category_theory.category D] [_inst_3 : category_theory.abelian C]
[_inst_4 : category_theory.has_injective_resolutions C] [_inst_5 : category_theory.abelian D] (F : C ⥤ D)
[_inst_6 : F.additive] (X : C) [_inst_7 : category_theory.injective X], (F.right_derived 0).obj X ≅ F.obj X := λ
{C : Type u} [_inst_1 : category_theory.category C] {D : Type u_1} [_inst_2 : category_theory.category D]
[_inst_3 : category_theory.abelian C] [_inst_4 : category_theory.has_injective_resolutions C]
[_inst_5 : category_theory.abelian D] (F : C ⥤ D) [_inst_6 : F.additive] (X : C)
[_inst_7 : category_theory.injective X],
F.right_derived_obj_iso 0 (category_theory.InjectiveResolution.self X) ≪≫
(homology_functor D (complex_shape.up ℕ) 0).map_iso
((cochain_complex.single₀_map_homological_complex F).app X) ≪≫
(cochain_complex.homology_functor_0_single₀ D).app (F.obj X)>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment