Topology

📁 Source: Mathlib/Algebra/Category/Ring/Topology.lean

Statistics

Metric	Count
Definitions instTopologicalSpaceHom, mvPolynomialHomeomorph, precompHomeomorph	3
Theorems continuous_apply, continuous_precomp, instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier, instT2SpaceHomOfCarrier, isClosedEmbedding_hom, isClosedEmbedding_precomp_of_surjective, isEmbedding_hom, isEmbedding_precomp_of_surjective, isEmbedding_pushout, isHomeomorph_precomp, mvPolynomialHomeomorph_apply_fst, mvPolynomialHomeomorph_apply_snd, mvPolynomialHomeomorph_symm_apply_hom, precompHomeomorph_apply, precompHomeomorph_symm_apply	15
Total	18

CommRingCat.HomTopology

Definitions

Name	Category	Theorems
instTopologicalSpaceHom 📖	CompOp	15 math math: isEmbedding_precomp_of_surjective, isClosedEmbedding_precomp_of_surjective, mvPolynomialHomeomorph_apply_snd, instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier, continuous_precomp, precompHomeomorph_apply, isEmbedding_pushout, instT2SpaceHomOfCarrier, precompHomeomorph_symm_apply, isClosedEmbedding_hom, mvPolynomialHomeomorph_symm_apply_hom, isEmbedding_hom, continuous_apply, isHomeomorph_precomp, mvPolynomialHomeomorph_apply_fst
mvPolynomialHomeomorph 📖	CompOp	3 math math: mvPolynomialHomeomorph_apply_snd, mvPolynomialHomeomorph_symm_apply_hom, mvPolynomialHomeomorph_apply_fst
precompHomeomorph 📖	CompOp	2 math math: precompHomeomorph_apply, precompHomeomorph_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_apply 📖	mathematical	—	Continuous Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.carrier instTopologicalSpaceHom DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom	—	Continuous.comp continuous_apply continuous_induced_dom
continuous_precomp 📖	mathematical	—	Continuous Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom CategoryTheory.CategoryStruct.comp	—	continuous_induced_rng Continuous.comp Pi.continuous_precomp continuous_induced_dom
instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier 📖	mathematical	—	CompactSpace Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom	—	Topology.IsClosedEmbedding.compactSpace Function.compactSpace isClosedEmbedding_hom
instT2SpaceHomOfCarrier 📖	mathematical	—	T2Space Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom	—	Topology.IsEmbedding.t2Space Pi.t2Space isEmbedding_hom
isClosedEmbedding_hom 📖	mathematical	—	Topology.IsClosedEmbedding Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom Pi.topologicalSpace CommRingCat.carrier DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat Finite.of_fintype Function.LeftInverse.surjective MvPolynomial.eval₂Hom_X' MvPolynomial.comp_eval₂Hom Topology.IsClosedEmbedding.comp Homeomorph.isClosedEmbedding isClosedEmbedding_precomp_of_surjective
isClosedEmbedding_precomp_of_surjective 📖	mathematical	CommRingCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom CommRingCat CommRingCat.instCategory RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier	Topology.IsClosedEmbedding Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instTopologicalSpaceHom CategoryTheory.CategoryStruct.comp	—	isEmbedding_precomp_of_surjective RingHom.instRingHomClass isClosed_iInter IsClosed.preimage continuous_apply isClosed_singleton Set.ext map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CommRingCat.hom_ext RingHom.ext RingHom.liftOfRightInverse_comp_apply
isEmbedding_hom 📖	mathematical	—	Topology.IsEmbedding Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom Pi.topologicalSpace CommRingCat.carrier DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom	—	Topology.IsInducing.induced CommRingCat.hom_ext RingHom.ext
isEmbedding_precomp_of_surjective 📖	mathematical	CommRingCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom CommRingCat CommRingCat.instCategory RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier	Topology.IsEmbedding Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instTopologicalSpaceHom CategoryTheory.CategoryStruct.comp	—	Topology.IsEmbedding.of_comp continuous_precomp Topology.IsInducing.continuous Topology.IsInducing.induced Function.Surjective.isEmbedding_comp Topology.IsEmbedding.comp Topology.IsEmbedding.induced CommRingCat.hom_ext RingHom.ext
isEmbedding_pushout 📖	mathematical	—	Topology.IsEmbedding Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Limits.pushout CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span instTopologicalSpaceHom instTopologicalSpaceProd CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr	—	MvPolynomial.eval₂Hom_X' Topology.IsEmbedding.prodMap isEmbedding_precomp_of_surjective CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat Topology.IsEmbedding.of_comp_iff RingHom.range_eq_top top_le_iff CommRingCat.closure_range_union_range_eq_top_of_isPushout CategoryTheory.IsPushout.of_hasPushout Subring.closure_le Topology.IsEmbedding.comp Homeomorph.isEmbedding isEmbedding_graph continuous_id CategoryTheory.Limits.pushout.condition CommRingCat.hom_ext MvPolynomial.ringHom_ext' RingHom.ext MvPolynomial.comp_eval₂Hom MvPolynomial.eval₂_C
isHomeomorph_precomp 📖	mathematical	—	IsHomeomorph Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom CategoryTheory.CategoryStruct.comp	—	Homeomorph.isHomeomorph
mvPolynomialHomeomorph_apply_fst 📖	mathematical	—	Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory DFunLike.coe Homeomorph CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing MvPolynomial.instCommRingMvPolynomial instTopologicalSpaceHom instTopologicalSpaceProd Pi.topologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike mvPolynomialHomeomorph CategoryTheory.CategoryStruct.comp CommRingCat.ofHom MvPolynomial.C	—	—
mvPolynomialHomeomorph_apply_snd 📖	mathematical	—	Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory DFunLike.coe Homeomorph CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing MvPolynomial.instCommRingMvPolynomial instTopologicalSpaceHom instTopologicalSpaceProd Pi.topologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike mvPolynomialHomeomorph RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier MvPolynomial.X	—	—
mvPolynomialHomeomorph_symm_apply_hom 📖	mathematical	—	CommRingCat.Hom.hom CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing MvPolynomial.instCommRingMvPolynomial DFunLike.coe Homeomorph Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceProd instTopologicalSpaceHom Pi.topologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm mvPolynomialHomeomorph MvPolynomial.eval₂Hom	—	—
precompHomeomorph_apply 📖	mathematical	—	DFunLike.coe Homeomorph Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom EquivLike.toFunLike Homeomorph.instEquivLike precompHomeomorph CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom	—	—
precompHomeomorph_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory instTopologicalSpaceHom EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm precompHomeomorph CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv	—	—

---

← Back to Index