ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>AlgebraicGeometry.IsReduced Y<GOAL>AlgebraicGeometry.IsReduced X
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.IsReduced (AlgebraicGeometry.Spec R) ↔ IsReduced ↑R
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>IsReduced ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>AlgebraicGeometry.IsReduced X
<VAR>P : {X : AlgebraicGeometry.Scheme} → X.Opens → Prop<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>h₁ : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U<VAR>h₂ : ∀ (X Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y) [hf : AlgebraicGeometry.IsOpenImmersion f], ∃ U V, ∃ (hU : U = ⊤) (hV : V = Set.range ⇑f.val.base), P { carrier := U, is_open' := ⋯ } → P { carrier := V, is_open' := ⋯ }<VAR>h₃ : ∀ (R : CommRingCat), P ⊤<GOAL>P U
<VAR>P : (X : AlgebraicGeometry.Scheme) → ↑↑X.toPresheafedSpace → Prop<VAR>h₁ : ∀ (R : CommRingCat) (x : ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace), P (AlgebraicGeometry.Spec R) x<VAR>h₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace), P X x → P Y (f.val.base x)<VAR>X : AlgebraicGeometry.Scheme<VAR>x : ↑↑X.toPresheafedSpace<GOAL>P X x
<VAR>X : AlgebraicGeometry.Scheme<VAR>hX : AlgebraicGeometry.IsReduced X<VAR>U : X.Opens<VAR>s : ↑(X.presheaf.obj (Opposite.op U))<VAR>hs : X.basicOpen s = ⊥<GOAL>s = 0
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsReduced X<VAR>U : X.Opens<VAR>s : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.basicOpen s = ⊥ ↔ s = 0
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsIntegral X<GOAL>Nonempty ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsIntegral X<VAR>U : X.Opens<VAR>Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>IsDomain ↑(X.presheaf.obj (Opposite.op U))
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsReduced X<VAR>H : IrreducibleSpace ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.IsIntegral X
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.IsIntegral X ↔ IrreducibleSpace ↑↑X.toPresheafedSpace ∧ AlgebraicGeometry.IsReduced X
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>AlgebraicGeometry.IsIntegral Y<VAR>Nonempty ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.IsIntegral X
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Spec R) ↔ IsDomain ↑R
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>Nonempty ↑↑X.toPresheafedSpace<VAR>IsDomain ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>AlgebraicGeometry.IsIntegral X
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>Function.Injective ⇑(X.presheaf.map i.op)
<VAR>self : AlgebraicGeometry.Scheme<VAR>x : ↑self.toTopCat<GOAL>∃ U R, Nonempty (self.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>Continuous ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>i : Opposite.op U' ⟶ Opposite.op U<GOAL>Y.presheaf.map i ≫ f.app U = f.app U' ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.val.base).map i.unop).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<VAR>i : Opposite.op V ⟶ Opposite.op V'<GOAL>f.appLE U V e ≫ X.presheaf.map i = f.appLE U V' ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<VAR>i : V = V'<GOAL>f.appLE U V' ⋯ ≫ X.presheaf.map (CategoryTheory.eqToHom i).op = f.appLE U V e
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<VAR>i : Opposite.op U' ⟶ Opposite.op U<GOAL>Y.presheaf.map i ≫ f.appLE U V e = f.appLE U' V ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<VAR>i : U' = U<GOAL>Y.presheaf.map (CategoryTheory.eqToHom i).op ≫ f.appLE U' V ⋯ = f.appLE U V e
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U : Y.Opens<GOAL>f.app U = f.appLE U ((TopologicalSpace.Opens.map f.val.base).obj U) ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U : Y.Opens<GOAL>f.appLE U ((TopologicalSpace.Opens.map f.val.base).obj U) ⋯ = f.app U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<VAR>e₁ : U = U'<VAR>e₂ : V = V'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>P (f.appLE U V e) ↔ P (f.appLE U' V' ⋯)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f g : X ⟶ Y<VAR>h_base : f.val.base = g.val.base<VAR>h_app : ∀ (U : Y.Opens), AlgebraicGeometry.Scheme.Hom.app f U ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op = AlgebraicGeometry.Scheme.Hom.app g U<GOAL>f = g
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<GOAL>(TopologicalSpace.Opens.map f.val.base).obj (iSup U) = ⨆ i, (TopologicalSpace.Opens.map f.val.base).obj (U i)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<GOAL>⨆ i, (TopologicalSpace.Opens.map f.val.base).obj (U i) = ⊤
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<GOAL>(TopologicalSpace.Opens.map (f ≫ g).val.base).obj U = (TopologicalSpace.Opens.map f.val.base).obj ((TopologicalSpace.Opens.map g.val.base).obj U)
<GOAL>∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f = f
<VAR>self : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.obj self = self.toLocallyRingedSpace
<GOAL>∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace} (f : (CategoryTheory.inducedFunctor AlgebraicGeometry.Scheme.toLocallyRingedSpace).obj X ⟶ (CategoryTheory.inducedFunctor AlgebraicGeometry.Scheme.toLocallyRingedSpace).obj Y), AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace.preimage f = f
<GOAL>∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToTop.map f = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map f.val
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.Scheme.forgetToTop.obj X = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<GOAL>(𝟙 X).val.base = 𝟙 ↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (𝟙 X) U = 𝟙 (X.presheaf.obj (Opposite.op U))
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).val = f.val ≫ g.val
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).val.base = f.val.base ≫ g.val.base
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : ↑↑X.toPresheafedSpace<GOAL>(f ≫ g).val.base x = g.val.base (f.val.base x)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (f ≫ g) U = AlgebraicGeometry.Scheme.Hom.app g U ≫ AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map g.val.base).obj U)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<VAR>V : Y.Opens<VAR>W : X.Opens<VAR>e₁ : V ≤ (TopologicalSpace.Opens.map g.val.base).obj U<VAR>e₂ : W ≤ (TopologicalSpace.Opens.map f.val.base).obj V<GOAL>AlgebraicGeometry.Scheme.Hom.appLE g U V e₁ ≫ AlgebraicGeometry.Scheme.Hom.appLE f V W e₂ = AlgebraicGeometry.Scheme.Hom.appLE (f ≫ g) U W ⋯
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<VAR>V : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map (f ≫ g).val.base).obj U<GOAL>AlgebraicGeometry.Scheme.Hom.appLE (f ≫ g) U V e = AlgebraicGeometry.Scheme.Hom.app g U ≫ AlgebraicGeometry.Scheme.Hom.appLE f ((TopologicalSpace.Opens.map g.val.base).obj U) V e
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f g : X ⟶ Y<VAR>e : f = g<VAR>U : Y.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app f U = AlgebraicGeometry.Scheme.Hom.app g U ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U V : Y.Opens<VAR>e : U = V<GOAL>AlgebraicGeometry.Scheme.Hom.app f U = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op ≫ AlgebraicGeometry.Scheme.Hom.app f V ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X = Y<VAR>U : Y.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.eqToHom e) U = CategoryTheory.eqToHom ⋯
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>i : U = V<GOAL>X.presheaf.map (CategoryTheory.eqToHom i).op = CategoryTheory.eqToHom ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>U : X.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.inv f) U = X.presheaf.map (CategoryTheory.eqToHom ⋯).op ≫ CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map (CategoryTheory.inv f).val.base).obj U))
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.inv f) ⊤ = CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.app f ⊤)
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec R).toLocallyRingedSpace = AlgebraicGeometry.Spec.locallyRingedSpaceObj R
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Spec.map (𝟙 R) = 𝟙 (AlgebraicGeometry.Spec R)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>AlgebraicGeometry.Spec.map (f ≫ g) = AlgebraicGeometry.Spec.map g ≫ AlgebraicGeometry.Spec.map f
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.Scheme.Spec.obj R = AlgebraicGeometry.Spec (Opposite.unop R)
<GOAL>∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Scheme.Spec.map f = AlgebraicGeometry.Spec.map f.unop
<VAR>R S : CommRingCat<VAR>e : R = S<GOAL>AlgebraicGeometry.Spec.map (CategoryTheory.eqToHom e) = CategoryTheory.eqToHom ⋯
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>CategoryTheory.IsIso f<GOAL>AlgebraicGeometry.Spec.map (CategoryTheory.inv f) = CategoryTheory.inv (AlgebraicGeometry.Spec.map f)
<VAR>R : CommRingCat<GOAL>↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace = PrimeSpectrum ↑R
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec R).sheaf = AlgebraicGeometry.Spec.structureSheaf ↑R
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Spec R).presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).val
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>(AlgebraicGeometry.Spec.map f).val.base = PrimeSpectrum.comap f
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>U : (AlgebraicGeometry.Spec R).Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) U = AlgebraicGeometry.StructureSheaf.comap f U ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).val.base).obj U) ⋯
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>U : (AlgebraicGeometry.Spec S).Opens<VAR>V : (AlgebraicGeometry.Spec R).Opens<VAR>e : U ≤ (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).val.base).obj V<GOAL>AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Spec.map f) V U e = AlgebraicGeometry.StructureSheaf.comap f V U e
<GOAL>AlgebraicGeometry.Scheme.empty.presheaf = (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑(TopCat.of PEmpty.{u_1 + 1}))ᵒᵖ).obj (CommRingCat.of PUnit.{u_1 + 1})
<GOAL>↑AlgebraicGeometry.Scheme.empty.toPresheafedSpace = TopCat.of PEmpty.{u_1 + 1}
<GOAL>AlgebraicGeometry.Scheme.Γ = (CategoryTheory.inducedFunctor AlgebraicGeometry.Scheme.toLocallyRingedSpace).op ⋙ AlgebraicGeometry.LocallyRingedSpace.Γ
<VAR>X : AlgebraicGeometry.Schemeᵒᵖ<GOAL>AlgebraicGeometry.Scheme.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
<VAR>X Y : AlgebraicGeometry.Schemeᵒᵖ<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.Scheme.Γ.map f = AlgebraicGeometry.Scheme.Hom.app f.unop ⊤
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.Scheme.Γ.map f.op = AlgebraicGeometry.Scheme.Hom.app f ⊤
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Scheme.SpecΓIdentity.app R = AlgebraicGeometry.Scheme.ΓSpecIso R
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Scheme.SpecΓIdentity.hom.app R = (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Scheme.SpecΓIdentity.inv.app R = (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) ⊤ ≫ (AlgebraicGeometry.Scheme.ΓSpecIso S).hom = (AlgebraicGeometry.Scheme.ΓSpecIso R).hom ≫ f
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>f ≫ (AlgebraicGeometry.Scheme.ΓSpecIso S).inv = (AlgebraicGeometry.Scheme.ΓSpecIso R).inv ≫ AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) ⊤
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.Scheme.ΓSpecIso R).inv = AlgebraicGeometry.StructureSheaf.toOpen ↑R ⊤
<VAR>R : CommRingCat<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)<GOAL>AlgebraicGeometry.StructureSheaf.toOpen (↑R) U = (AlgebraicGeometry.Scheme.ΓSpecIso R).inv ≫ (AlgebraicGeometry.Spec R).presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>x : ↥U<GOAL>↑x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ x) f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ X.basicOpen f ↔ ∃ (m : x ∈ U), IsUnit ((X.presheaf.germ ⟨x, m⟩) f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>f : ↑(X.presheaf.obj (Opposite.op ⊤))<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ ⟨x, trivial⟩) f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>V U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>i : Opposite.op U ⟶ Opposite.op V<GOAL>X.basicOpen ((X.presheaf.map i) f) = V ⊓ X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>V U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>i : Opposite.op U ⟶ Opposite.op V<VAR>CategoryTheory.IsIso i<GOAL>X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.basicOpen f ≤ U
<VAR>X : AlgebraicGeometry.Scheme<VAR>V U : X.Opens<VAR>i : V ⟶ U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.basicOpen (TopCat.Presheaf.restrict f i) ≤ X.basicOpen f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>r : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>(TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r) = X.basicOpen ((AlgebraicGeometry.Scheme.Hom.app f U) r)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : X.Opens<VAR>V : Y.Opens<VAR>e : U ≤ (TopologicalSpace.Opens.map f.val.base).obj V<VAR>s : ↑(Y.presheaf.obj (Opposite.op V))<GOAL>X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f V U e) s) = U ⊓ (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen s)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>X.basicOpen 0 = ⊥
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f g : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>n : ℕ<VAR>h : 0 < n<GOAL>X.basicOpen (f ^ n) = X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>hf : IsUnit f<GOAL>X.basicOpen f = U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.zeroLocus s = ⋂ f ∈ s, (X.basicOpen f).carrierᶜ
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<GOAL>IsClosed (X.zeroLocus s)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.zeroLocus {f} = (X.basicOpen f).carrierᶜ
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>X.zeroLocus ∅ = Set.univ
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f
<VAR>R : CommRingCat<VAR>f : ↑R<GOAL>(AlgebraicGeometry.Spec R).basicOpen ((AlgebraicGeometry.Scheme.ΓSpecIso R).inv f) = PrimeSpectrum.basicOpen f
<VAR>R : CommRingCat<VAR>f : ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤))<GOAL>(AlgebraicGeometry.Spec R).basicOpen f = PrimeSpectrum.basicOpen ((AlgebraicGeometry.Scheme.ΓSpecIso R).hom f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>h : U = V<VAR>W : (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op V))).Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op)) W = CategoryTheory.eqToHom ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<GOAL>e.hom.val.base ≫ e.inv.val.base = 𝟙 ↑X.toPresheafedSpace
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<VAR>x : ↑↑X.toPresheafedSpace<GOAL>e.inv.val.base (e.hom.val.base x) = x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<GOAL>e.inv.val.base ≫ e.hom.val.base = 𝟙 ↑Y.toPresheafedSpace
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<VAR>y : ↑↑Y.toPresheafedSpace<GOAL>e.hom.val.base (e.inv.val.base y) = y
<VAR>X : AlgebraicGeometry.Scheme<VAR>x : ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap (f ≫ g) x = AlgebraicGeometry.Scheme.Hom.stalkMap g (f.val.base x) ≫ AlgebraicGeometry.Scheme.Hom.stalkMap f x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>x x' : ↑↑X.toPresheafedSpace<VAR>h : x ⤳ x'<GOAL>Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.Scheme.Hom.stalkMap f x = AlgebraicGeometry.Scheme.Hom.stalkMap f x' ≫ X.presheaf.stalkSpecializes h
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>x x' : ↑↑X.toPresheafedSpace<VAR>h : x ⤳ x'<VAR>y : ↑(Y.presheaf.stalk (f.val.base x'))<GOAL>(AlgebraicGeometry.Scheme.Hom.stalkMap f x) ((Y.presheaf.stalkSpecializes ⋯) y) = (X.presheaf.stalkSpecializes h) ((AlgebraicGeometry.Scheme.Hom.stalkMap f x') y)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f g : X ⟶ Y<VAR>hfg : f = g<VAR>x x' : ↑↑X.toPresheafedSpace<VAR>hxx' : x = x'<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.Scheme.Hom.stalkMap g x'
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f g : X ⟶ Y<VAR>hfg : f = g<VAR>x : ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.Scheme.Hom.stalkMap g x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>x x' : ↑↑X.toPresheafedSpace<VAR>hxx' : x = x'<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.Scheme.Hom.stalkMap f x'
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<VAR>y : ↑↑Y.toPresheafedSpace<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap e.hom (e.inv.val.base y) ≫ AlgebraicGeometry.Scheme.Hom.stalkMap e.inv y = Y.presheaf.stalkSpecializes ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<VAR>y : ↑↑Y.toPresheafedSpace<VAR>z : ↑(Y.presheaf.stalk (e.hom.val.base (e.inv.val.base y)))<GOAL>(AlgebraicGeometry.Scheme.Hom.stalkMap e.inv y) ((AlgebraicGeometry.Scheme.Hom.stalkMap e.hom (e.inv.val.base y)) z) = (Y.presheaf.stalkSpecializes ⋯) z
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<VAR>x : ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.Scheme.Hom.stalkMap e.inv (e.hom.val.base x) ≫ AlgebraicGeometry.Scheme.Hom.stalkMap e.hom x = X.presheaf.stalkSpecializes ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>e : X ≅ Y<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑(X.presheaf.stalk (e.inv.val.base (e.hom.val.base x)))<GOAL>(AlgebraicGeometry.Scheme.Hom.stalkMap e.hom x) ((AlgebraicGeometry.Scheme.Hom.stalkMap e.inv (e.hom.val.base x)) y) = (X.presheaf.stalkSpecializes ⋯) y
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>x : ↥((TopologicalSpace.Opens.map f.val.base).obj U)<GOAL>Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩ ≫ AlgebraicGeometry.Scheme.Hom.stalkMap f ↑x = AlgebraicGeometry.Scheme.Hom.app f U ≫ X.presheaf.germ x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>x : ↥((TopologicalSpace.Opens.map f.val.base).obj U)<VAR>y : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Scheme.Hom.stalkMap f ↑x) ((Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩) y) = (X.presheaf.germ x) ((f.val.c.app (Opposite.op U)) y)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : f.val.base x ∈ U<GOAL>Y.presheaf.germ ⟨f.val.base x, hx⟩ ≫ AlgebraicGeometry.Scheme.Hom.stalkMap f x = AlgebraicGeometry.Scheme.Hom.app f U ≫ X.presheaf.germ ⟨x, hx⟩
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : f.val.base x ∈ U<VAR>y : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Scheme.Hom.stalkMap f x) ((Y.presheaf.germ ⟨f.val.base x, hx⟩) y) = (X.presheaf.germ ⟨x, hx⟩) ((f.val.c.app (Opposite.op U)) y)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<GOAL>MonoidAlgebra.single a 0 = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<VAR>b₁ b₂ : k<GOAL>MonoidAlgebra.single a (b₁ + b₂) = MonoidAlgebra.single a b₁ + MonoidAlgebra.single a b₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>a : G<VAR>b : k<VAR>h : G → k → N<VAR>h_zero : h a 0 = 0<GOAL>Finsupp.sum (MonoidAlgebra.single a b) h = h a b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>f : MonoidAlgebra k G<GOAL>Finsupp.sum f MonoidAlgebra.single = f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a a' : G<VAR>b : k<VAR>Decidable (a = a')<GOAL>(MonoidAlgebra.single a b) a' = if a = a' then b else 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>a : G<VAR>b : k<GOAL>MonoidAlgebra.single a b = 0 ↔ b = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>k' : Type u_3<VAR>G' : Type u_4<VAR>Semiring k'<VAR>f : G → G'<VAR>s : MonoidAlgebra k' G<VAR>v : G → k' → MonoidAlgebra k G<GOAL>MonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun a b => MonoidAlgebra.mapDomain f (v a b)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>Semiring k<VAR>NonUnitalNonAssocSemiring R<VAR>f : k →+ R<VAR>g : G → R<VAR>a : G<VAR>b : k<GOAL>(MonoidAlgebra.liftNC f g) (MonoidAlgebra.single a b) = f b * g a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>Mul G<VAR>f g : MonoidAlgebra k G<GOAL>f * g = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>Semiring k<VAR>Mul G<VAR>Semiring R<VAR>g_hom : Type u_3<VAR>FunLike g_hom G R<VAR>MulHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<VAR>a b : MonoidAlgebra k G<VAR>h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)<GOAL>(MonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (MonoidAlgebra.liftNC ↑f ⇑g) a * (MonoidAlgebra.liftNC ↑f ⇑g) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>One G<GOAL>1 = MonoidAlgebra.single 1 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Semiring k<VAR>One G<VAR>g_hom : Type u_3<VAR>FunLike g_hom G R<VAR>OneHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<GOAL>(MonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>MulOneClass G<VAR>n : ℕ<GOAL>↑n = MonoidAlgebra.single 1 ↑n
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Ring k<VAR>MulOneClass G<VAR>z : ℤ<GOAL>↑z = MonoidAlgebra.single 1 ↑z
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>DecidableEq G<VAR>Mul G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0