IrreducibleComponent

📁 Source: Mathlib/AlgebraicGeometry/IdealSheaf/IrreducibleComponent.lean

Statistics

Metric	Count
Definitions irreducibleComponent, irreducibleComponentIdeal, irreducibleComponentOpen, irreducibleComponentι	4
Theorems instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent, instIsClosedImmersionIrreducibleComponentι, instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat, irreducibleComponentIdeal_def, irreducibleComponentOpen_eq_top, irreducibleComponentι_apply	6
Total	10

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
irreducibleComponent 📖	CompOp	4 math math: instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent, irreducibleComponentι_apply, instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat, instIsClosedImmersionIrreducibleComponentι
irreducibleComponentIdeal 📖	CompOp	2 math math: irreducibleComponentIdeal_def, irreducibleComponentι_apply
irreducibleComponentOpen 📖	CompOp	2 math math: irreducibleComponentOpen_eq_top, irreducibleComponentIdeal_def
irreducibleComponentι 📖	CompOp	3 math math: irreducibleComponentι_apply, instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat, instIsClosedImmersionIrreducibleComponentι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	IrreducibleSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace irreducibleComponent AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	Subtype.irreducibleSpace
instIsClosedImmersionIrreducibleComponentι 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	AlgebraicGeometry.IsClosedImmersion irreducibleComponent irreducibleComponentι	—	—
instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.IsIso AlgebraicGeometry.Scheme instCategory irreducibleComponent irreducibleComponentι	—	irreducibleComponentOpen_eq_top CategoryTheory.Iso.isIso_hom irreducibleComponentι.eq_1 isIso_subschemeι_iff_eq_bot irreducibleComponentIdeal_def Hom.ker_eq_bot_of_isIso
irreducibleComponentIdeal_def 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	irreducibleComponentIdeal Hom.ker Opens.toScheme irreducibleComponentOpen Opens.ι	—	IdealSheafData.ext Ideal.ext
irreducibleComponentOpen_eq_top 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	irreducibleComponentOpen Top.top Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	irreducibleComponents_eq_singleton Set.mem_singleton_iff sdiff_self Set.sUnion_empty Set.compl_empty
irreducibleComponentι_apply 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace irreducibleComponent TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' irreducibleComponentι TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Closeds.instSetLike IdealSheafData.support irreducibleComponentIdeal	—	—

---

← Back to Index