Documentation

GAGA.SpecComplex

source
def SpecComplex.termSpecℂ :
Lean.ParserDescr
Equations
Instances For
    source
    @[simp]
    theorem SpecComplex.openCover_f :
    ∀ (x : ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℂ))).toPresheafedSpace), SpecComplex.openCover.f x = PUnit.unit
    source
    @[simp]
    theorem SpecComplex.openCover_J :
    SpecComplex.openCover.J = PUnit.{u_1 + 1}
    source
    @[simp]
    theorem SpecComplex.openCover_obj :
    ∀ (x : PUnit.{u_1 + 1} ), SpecComplex.openCover.obj x = AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℂ))
    source
    @[simp]
    theorem SpecComplex.openCover_map :
    ∀ (x : PUnit.{u_1 + 1} ), SpecComplex.openCover.map x = CategoryTheory.CategoryStruct.id ((fun (x : PUnit.{u_1 + 1} ) => AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℂ))) x)
    source
    noncomputable def SpecComplex.openCover :
    AlgebraicGeometry.Scheme.OpenCover (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℂ)))

    the open cover of Spec ℂ by the single open set Spec ℂ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance SpecComplex.isnt_openCover_isAffine (i : SpecComplex.openCover.J) :
      AlgebraicGeometry.IsAffine (SpecComplex.openCover.obj i)
      Equations
      • ⋯ = ⋯
      source
      instance SpecComplex.instUniqueαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceObjOppositeToQuiverToCategoryStructOppositeSchemeInstCategorySchemeToPrefunctorSpecOpOfComplexCommRing :
      Unique ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℂ))).toPresheafedSpace
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance SpecComplex.instIsSimpleOrderOpensαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceObjOppositeToQuiverToCategoryStructOppositeSchemeInstCategorySchemeToPrefunctorSpecOpOfComplexCommRingInstTopologicalSpaceαCarrierToPresheafedSpaceToLEToPreorderToPartialOrderInstOmegaCompletePartialOrderInstCompleteLatticeOpensToBoundedOrder :
      IsSimpleOrder (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℂ))).toPresheafedSpace)
      Equations
      • One or more equations did not get rendered due to their size.