LocallyRingedSpace

📁 Source: Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

Statistics

Metric	Count
Definitions locallyRingedSpace	1
Theorems instLocalRing_stalk, isUnit_stalk_iff, nonunits_stalk	3
Total	4

IsManifold

Definitions

Name	Category	Theorems
locallyRingedSpace 📖	CompOp	—

smoothSheafCommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLocalRing_stalk 📖	mathematical	—	IsLocalRing CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instFieldContMDiffRing WithTop.some ENat Top.top instTopENat CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing	—	IsLocalRing.of_nonunits_add CommRingCat.Colimits.hasColimits_commRingCat instFieldContMDiffRing instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing IsLocalRing.toNontrivial Field.instIsLocalRing RingHom.instRingHomClass nonunits_stalk Ideal.add_mem
isUnit_stalk_iff 📖	mathematical	—	IsUnit CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instFieldContMDiffRing WithTop.some ENat Top.top instTopENat MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass eval	—	CommRingCat.Colimits.hasColimits_commRingCat instFieldContMDiffRing RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MulZeroClass.zero_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing TopCat.Presheaf.germ_exist CommRingCat.FilteredColimits.forget_preservesFilteredColimits eval_germ ContinuousAt.eventually_ne T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.continuousAt ContMDiff.continuous eventually_nhds_iff IsOpen.isOpenMap_subtype_val TopologicalSpace.Opens.is_open' Subtype.coe_image_subset Set.ext Set.preimage_image_eq Subtype.coe_injective Set.range_inclusion Set.mem_range_self ContMDiffAt.comp ContDiffAt.contMDiffAt contDiffAt_inv ContMDiff.contMDiffAt ContMDiff.comp ContMDiffMap.contMDiff contMDiff_inclusion mul_inv_cancel₀ RingHom.map_one inv_mul_cancel₀ TopCat.Presheaf.germ_res_apply
nonunits_stalk 📖	mathematical	—	nonunits CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instFieldContMDiffRing WithTop.some ENat Top.top instTopENat MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass eval	—	Set.ext CommRingCat.Colimits.hasColimits_commRingCat instFieldContMDiffRing RingHom.instRingHomClass mem_nonunits_iff not_iff_comm isUnit_stalk_iff

---

← Back to Index