Structures · Geometry
AlgebraicGeometry.IsNoetherian
A scheme X is Noetherian if it is locally Noetherian and compact.
- Defined in
- Mathlib.AlgebraicGeometry.Noetherian
- Shape
- One type argument
Extends2
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- AlgebraicGeometry.Spec
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- AlgebraicGeometry.Scheme.irreducibleComponentOpen
- AlgebraicGeometry.Scheme.irreducibleComponentIdeal
- AlgebraicGeometry.Scheme.irreducibleComponent
- AlgebraicGeometry.Scheme.irreducibleComponentι
- AlgebraicGeometry.Scheme.instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent
- AlgebraicGeometry.IsNoetherian.noetherianSpace
- AlgebraicGeometry.Scheme.instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat
- AlgebraicGeometry.Scheme.instIsClosedImmersionIrreducibleComponentι
- AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian
- AlgebraicGeometry.Scheme.irreducibleComponentOpen_eq_top
- AlgebraicGeometry.IsNoetherian.toIsLocallyNoetherian
- AlgebraicGeometry.IsNoetherian.toCompactSpace
- AlgebraicGeometry.Scheme.irreducibleComponentι_apply
- AlgebraicGeometry.Scheme.irreducibleComponentIdeal_def