AlgebraicCurve.exists_isAffineOpen_forall_mem_of_finset_of_field
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isAffineOpen_forall_mem_of_finset_of_field
attribute [-instance]
AlgebraicCurve.Place.instIsScalarTowerSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Divisor.instDistribMulActionAlgEquiv AlgebraicCurve.Place.instSMulAlgEquiv
AlgebraicCurve.Place.instIsPrincipalIdealRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Place.instIsDiscreteValuationRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Pic0.instDistribMulActionAlgEquiv
AlgebraicCurve.Place.instAlgebraSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Place.instMulActionAlgEquiv AlgebraicCurve.Pic0.instSMulAlgEquiv
AlgebraicCurve.CurveModel.isProper AlgebraicCurve.CurveModel.isIntegral
AlgebraicCurve.CurveModel.smooth
attribute [-simp] AlgebraicCurve.Place.mk.injEq AlgebraicCurve.Divisor.degree_single
AlgebraicCurve.Divisor.smul_single AlgebraicCurve.Place.smul_toValuationSubring
AlgebraicCurve.Place.heightOneSpectrum_asIdeal AlgebraicCurve.Place.coe_algebraMap
AlgebraicCurve.Place.ord_one AlgebraicCurve.Place.coe_smulRingEquiv_apply
AlgebraicCurve.Pic0.coe_degZeroSMulHom AlgebraicCurve.Place.deg_smul AlgebraicCurve.Pic0.mk_zero
AlgebraicCurve.Place.mk.sizeOf_spec AlgebraicCurve.Divisor.degree_smul AlgebraicCurve.Pic0.mk_add
AlgebraicCurve.Place.ord_zero AlgebraicCurve.Place.ofHeightOneSpectrum_toValuationSubring
AlgebraicCurve.CurveModel.mk.injEq AlgebraicCurve.CurveModel.mk.sizeOf_spec
noncomputable section
open CategoryTheory AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicCurve.exists_isAffineOpen_forall_mem_of_finset_of_field {K : Type u} [Field
K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
[IsIntegral C] [IsProper c] [SmoothOfRelativeDimension 1 c]
(F : Finset C) :
∃ U : C.Opens, IsAffineOpen U ∧ ∀ x ∈ F, x ∈ U