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 CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory 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 CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory 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 AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid 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 AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid instTopologicalSpaceHom instTopologicalSpaceProd Pi.topologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike mvPolynomialHomeomorph RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CategoryTheory.ConcreteCategory.hom RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier MvPolynomial.X	—	—
mvPolynomialHomeomorph_symm_apply_hom 📖	mathematical	—	CommRingCat.Hom.hom CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid 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