ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>g' : (P.drop.B a).Arrow α<VAR>g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α<GOAL>(P.wMk a g' fun i => ⟨f i, g i⟩) = ⟨WType.mk a f, P.wPathCasesOn g' g⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α.Arrow β<VAR>a : P.A<VAR>f' : (P.drop.B a).Arrow α<VAR>f : P.last.B a → P.W α<GOAL>MvFunctor.map g (P.wMk a f' f) = P.wMk a (TypeVec.comp g f') fun i => MvFunctor.map g (f i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α γ : TypeVec.{u} n<VAR>g : α.Arrow γ<VAR>a : P.A<VAR>f' : (P.drop.B a).Arrow α<VAR>f : P.last.B a → P.W α<GOAL>MvFunctor.map (g ::: P.wMap g) (P.objAppend1 a f' f) = P.objAppend1 a (TypeVec.comp g f') fun x => P.wMap g (f x)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f' : (P.drop.B a).Arrow α<VAR>f : P.last.B a → P.W α<GOAL>P.wDest' (P.wMk a f' f) = ⟨a, TypeVec.splitFun f' f⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>x : ↑P (α ::: P.W α)<GOAL>P.wDest' (P.wMk' x) = x
<VAR>A : Type u_1<VAR>B : outParam (Type u_2)<VAR>self : SetLike A B<GOAL>Function.Injective SetLike.coe
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<GOAL>↑↑p = ↥p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>q : ↥p → Prop<GOAL>(∃ x, q x) ↔ ∃ x, ∃ (h : x ∈ p), q ⟨x, h⟩
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>q : ↥p → Prop<GOAL>(∀ (x : ↥p), q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, h⟩
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<GOAL>Function.Injective SetLike.coe
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>↑p = ↑q ↔ p = q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>↑p ≠ ↑q ↔ p ≠ q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<VAR>h : ↑p = ↑q<GOAL>p = q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>p = q ↔ ↑p = ↑q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<VAR>h : ∀ (x : B), x ∈ p ↔ x ∈ q<GOAL>p = q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>x : B<GOAL>x ∈ ↑p ↔ x ∈ p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>x y : ↥p<GOAL>↑x = ↑y ↔ x = y
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>x : ↥p<GOAL>↑x ∈ p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>s : Set B<VAR>hp : s ⊆ ↑p<VAR>x : B<VAR>hx : x ∈ s<GOAL>x ∈ p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p : A<VAR>x : ↥p<VAR>hx : ↑x ∈ p<GOAL>⟨↑x, hx⟩ = x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>S T : A<GOAL>S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>S T : A<GOAL>↑S ⊆ ↑T ↔ S ≤ T
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<GOAL>Monotone SetLike.coe
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>S T : A<GOAL>↑S ⊂ ↑T ↔ S < T
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<GOAL>StrictMono SetLike.coe
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>¬p ≤ q ↔ ∃ x ∈ p, x ∉ q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>p < q → ∃ x ∈ q, x ∉ p
<VAR>R : CommRingCat<GOAL>(CategoryTheory.forget TopCat).obj (AlgebraicGeometry.Spec.topObj R) = PrimeSpectrum ↑R
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Spec.topMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.topObj R)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>AlgebraicGeometry.Spec.topMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.topMap g) (AlgebraicGeometry.Spec.topMap f)
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.Spec.toTop.obj R = AlgebraicGeometry.Spec.topObj (Opposite.unop R)
<VAR>R S : CommRingCatᵒᵖ<VAR>f : R ⟶ S<GOAL>AlgebraicGeometry.Spec.toTop.map f = AlgebraicGeometry.Spec.topMap f.unop
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec.sheafedSpaceObj R).presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).val
<VAR>R : CommRingCat<GOAL>↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace = AlgebraicGeometry.Spec.topObj R
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>(AlgebraicGeometry.Spec.sheafedSpaceMap f).base = AlgebraicGeometry.Spec.topMap f
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ<GOAL>(AlgebraicGeometry.Spec.sheafedSpaceMap f).c.app U = AlgebraicGeometry.StructureSheaf.comap f (Opposite.unop U) ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).obj (Opposite.unop U)) ⋯
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Spec.sheafedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.sheafedSpaceObj R)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>AlgebraicGeometry.Spec.sheafedSpaceMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.sheafedSpaceMap g) (AlgebraicGeometry.Spec.sheafedSpaceMap f)
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.Spec.toSheafedSpace.obj R = AlgebraicGeometry.Spec.sheafedSpaceObj (Opposite.unop R)
<GOAL>∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Spec.toSheafedSpace.map f = AlgebraicGeometry.Spec.sheafedSpaceMap f.unop
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.Spec.toPresheafedSpace.obj R = (AlgebraicGeometry.Spec.sheafedSpaceObj (Opposite.unop R)).toPresheafedSpace
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Spec.toPresheafedSpace.obj (Opposite.op R) = (AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace
<VAR>R S : CommRingCatᵒᵖ<VAR>f : R ⟶ S<GOAL>AlgebraicGeometry.Spec.toPresheafedSpace.map f = AlgebraicGeometry.Spec.sheafedSpaceMap f.unop
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>AlgebraicGeometry.Spec.toPresheafedSpace.map f.op = AlgebraicGeometry.Spec.sheafedSpaceMap f
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>R : CommRingCat<VAR>α β : X ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R<VAR>w : α.base = β.base<VAR>h : ∀ (r : ↑R), let U := PrimeSpectrum.basicOpen r; CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑R) U) (α.c.app (Opposite.op U))) (X.presheaf.map (CategoryTheory.eqToHom ⋯)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑R) U) (β.c.app (Opposite.op U))<GOAL>α = β
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj R).presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).val
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj R).toSheafedSpace = AlgebraicGeometry.Spec.sheafedSpaceObj R
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj R).sheaf = AlgebraicGeometry.Spec.structureSheaf ↑R
<VAR>R : Type u<VAR>CommRing R<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).sheaf = AlgebraicGeometry.Spec.structureSheaf R
<VAR>R : CommRingCat<VAR>U V : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj R).toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj R).presheaf.map i = (AlgebraicGeometry.Spec.structureSheaf ↑R).val.map i
<VAR>R : Type u<VAR>CommRing R<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).presheaf = (AlgebraicGeometry.Spec.structureSheaf R).val
<VAR>R : Type u<VAR>CommRing R<VAR>U V : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).presheaf.map i = (AlgebraicGeometry.Spec.structureSheaf R).val.map i
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑S<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) ((PrimeSpectrum.comap f) p)) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p) = CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toStalk (↑S) p)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑S<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap f) p)).hom (CategoryTheory.CategoryStruct.comp (Localization.localRingHom ((PrimeSpectrum.comap f) p).asIdeal p.asIdeal f ⋯) (AlgebraicGeometry.StructureSheaf.stalkIso (↑S) p).inv) = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>(AlgebraicGeometry.Spec.locallyRingedSpaceMap f).val = AlgebraicGeometry.Spec.sheafedSpaceMap f
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.locallyRingedSpaceObj R)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.locallyRingedSpaceMap g) (AlgebraicGeometry.Spec.locallyRingedSpaceMap f)
<GOAL>∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Spec.toLocallyRingedSpace.map f = AlgebraicGeometry.Spec.locallyRingedSpaceMap f.unop
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.Spec.toLocallyRingedSpace.obj R = AlgebraicGeometry.Spec.locallyRingedSpaceObj (Opposite.unop R)
<VAR>R : CommRingCat<VAR>f : ↑(CommRingCat.of ↑R)<VAR>x : ↥(Opposite.unop (Opposite.op ⊤))<GOAL>↑((AlgebraicGeometry.toSpecΓ R) f) x = (algebraMap (↑R) (AlgebraicGeometry.StructureSheaf.Localizations ↑R ↑x)) f
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.toSpecΓ S) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ R) (AlgebraicGeometry.LocallyRingedSpace.Γ.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.map f.op).op)
<VAR>X : CommRingCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.hom.app X = CategoryTheory.inv (AlgebraicGeometry.toSpecΓ X)
<VAR>X : CommRingCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.inv.app X = AlgebraicGeometry.toSpecΓ X
<VAR>R : CommRingCat<VAR>M : Submonoid ↑R<VAR>x : PrimeSpectrum (Localization M)<GOAL>CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<GOAL>CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p) ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).c)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<GOAL>algebraMap ↑R ↑(((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj (AlgebraicGeometry.Spec.structureSheaf ↑S).val).stalk p) = CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p)
<VAR>R S : CommRingCat<VAR>p : PrimeSpectrum ↑R<VAR>Algebra ↑R ↑S<GOAL>∀ (a : ↑S), (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) a = (((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap (algebraMap ↑R ↑S))).obj (AlgebraicGeometry.Spec.structureSheaf ↑S).val).germ ⟨p, trivial⟩) ((AlgebraicGeometry.StructureSheaf.toOpen ↑S ⊤) a)
<VAR>R S : CommRingCat<VAR>p : PrimeSpectrum ↑R<VAR>Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap (algebraMap ↑R ↑S))).obj (AlgebraicGeometry.Spec.structureSheaf ↑S).val).stalk p)<GOAL>∃ x, x.2 • y = (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) x.1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a b : (x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal<VAR>ha : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred a<VAR>hb : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred b<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred (a + b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a : (x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal<VAR>ha : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred a<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred (-a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a b : (x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal<VAR>ha : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred a<VAR>hb : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred b<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred (a * b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>∀ {X Y : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ} (i : X ⟶ Y) (a : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType 𝒜).val.obj X), ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing 𝒜).map i) a = (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType 𝒜).val.map i a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing 𝒜).obj U = CommRingCat.of ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType 𝒜).val.obj U)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>i : V ⟶ U<VAR>s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj V)<VAR>x : ↥(Opposite.unop U)<GOAL>↑(((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.map i) s) x = ↑s ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj V)<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj V)<VAR>x : ↥(Opposite.unop V)<GOAL>↑(s + t) x = ↑s x + ↑t x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj V)<VAR>x : ↥(Opposite.unop V)<GOAL>↑(s * t) x = ↑s x * ↑t x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj V)<VAR>x : ↥(Opposite.unop V)<GOAL>↑(s - t) x = ↑s x - ↑t x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj V)<VAR>x : ↥(Opposite.unop V)<VAR>n : ℕ<GOAL>↑(s ^ n) x = ↑s x ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>x : ↥(Opposite.unop V)<GOAL>↑0 x = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>x : ↥(Opposite.unop V)<GOAL>↑1 x = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>x : ↥U<GOAL>CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ x) (AlgebraicGeometry.stalkToFiberRingHom 𝒜 ↑x) = AlgebraicGeometry.openToLocalization 𝒜 U ↑x ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>hx : x ∈ U<VAR>s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.stalkToFiberRingHom 𝒜 x) (((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hx⟩) s) = ↑s ⟨x, hx⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>x : ↥U<VAR>s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.stalkToFiberRingHom 𝒜 ↑x) (((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ x) s) = ↑s x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl<GOAL>x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>z : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.stalk x)<GOAL>AlgebraicGeometry.homogeneousLocalizationToStalk 𝒜 x ((AlgebraicGeometry.stalkToFiberRingHom 𝒜 x) z) = z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>z : HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal<GOAL>(AlgebraicGeometry.stalkToFiberRingHom 𝒜 x) (AlgebraicGeometry.homogeneousLocalizationToStalk 𝒜 x z) = z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>hx : x ∈ U<VAR>s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Proj.stalkIso' 𝒜 x) (((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hx⟩) s) = ↑s ⟨x, hx⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>x : ↥U<VAR>s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Proj.stalkIso' 𝒜 ↑x) (((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ x) s) = ↑s x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl<GOAL>(AlgebraicGeometry.Proj.stalkIso' 𝒜 x).symm (HomogeneousLocalization.mk f) = ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ ⟨x, ⋯⟩) (AlgebraicGeometry.sectionInBasicOpen 𝒜 x f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsAffine X<GOAL>CategoryTheory.IsIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<GOAL>X.isoSpec.hom = AlgebraicGeometry.ΓSpec.adjunction.unit.app X
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>AlgebraicGeometry.IsAffine Y<VAR>f : X ⟶ Y<GOAL>X.isoSpec.hom ≫ AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f ⊤) = f ≫ Y.isoSpec.hom
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>AlgebraicGeometry.IsAffine Y<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f ⊤) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
<VAR>X : AlgebraicGeometry.Scheme<GOAL>∀ (x : AlgebraicGeometry.IsAffine X), (AlgebraicGeometry.AffineScheme.mk X x).obj = X
<VAR>X : AlgebraicGeometry.Scheme<GOAL>X ∈ AlgebraicGeometry.Scheme.Spec.essImage ↔ AlgebraicGeometry.IsAffine X
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>h : AlgebraicGeometry.IsAffine Y<GOAL>AlgebraicGeometry.IsAffine X
<GOAL>∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.Scheme CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), AlgebraicGeometry.AffineScheme.forgetToScheme.map f = f
<VAR>self : CategoryTheory.FullSubcategory AlgebraicGeometry.Scheme.Spec.essImage<GOAL>AlgebraicGeometry.AffineScheme.forgetToScheme.obj self = self.obj
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Scheme.Hom.opensRange f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<GOAL>AlgebraicGeometry.IsAffineOpen ⊤
<VAR>X : AlgebraicGeometry.Scheme<GOAL>TopologicalSpace.Opens.IsBasis X.affineOpens
<VAR>X : AlgebraicGeometry.Scheme<GOAL>⨆ i, ↑i = ⊤
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>f : ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))<GOAL>(TopologicalSpace.Opens.map X.isoSpec.hom.val.base).obj (PrimeSpectrum.basicOpen f) = X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<GOAL>TopologicalSpace.Opens.IsBasis (Set.range X.basicOpen)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>Set.range ⇑hU.fromSpec.val.base = ↑U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>AlgebraicGeometry.Scheme.Hom.opensRange hU.fromSpec = U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>V : X.Opens<VAR>hV : AlgebraicGeometry.IsAffineOpen V<VAR>f : Opposite.op U ⟶ Opposite.op V<GOAL>AlgebraicGeometry.Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>IsCompact ↑U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)