Surjective

📁 Source: Mathlib/RingTheory/RingHom/Surjective.lean

Statistics

Metric	Count
Definitions Surjective	1
Theorems surjective_isStableUnderBaseChange, surjective_localRingHom_of_surjective, surjective_localizationPreserves, surjective_ofLocalizationSpan, surjective_respectsIso, surjective_stableUnderComposition	6
Total	7

AlgebraicGeometry

Definitions

Name	Category	Theorems
Surjective 📖	CompData	36 math math: Surjective.instFstScheme, descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, UniversallyInjective.iff_diagonal, Scheme.exists_hom_isAffine_of_isLocalAtSource, descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, surjective_isZariskiLocalAtTarget, Surjective.instIsStableUnderBaseChangeScheme, instIsMultiplicativeSchemeSurjective, instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, Surjective.sigmaDesc_of_union_range_eq_univ, Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, Surjective.of_universallyClosed_of_isDominant, instHasOfPrecompPropertySchemeSurjective, instSurjectiveOfGeometricallyIrreducible, instSurjectiveOfIsIsoScheme, instSurjectiveCompScheme, instRespectsIsoSchemeSurjective, isIso_iff_isOpenImmersion_and_surjective, surjective_iff, instSurjectiveOfNonemptyOfSubsingletonCarrierCarrierCommRingCat, instSurjectiveDescI₀SchemeF, Surjective.of_comp, universallyInjective_eq_diagonal, Surjective.comp_iff, Surjective.instSndScheme, Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, isomorphisms_eq_isOpenImmersion_inf_surjective, instSurjectiveOfGeometricallyIntegral, surjective_eq_topologically, flat_and_surjective_SpecMap_iff, AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass, Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource, surjective_of_isDominant_of_isClosed_range, descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_isStableUnderBaseChange 📖	mathematical	—	IsStableUnderBaseChange DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	—	surjective_respectsIso TensorProduct.induction_on Algebra.to_smulCommClass map_zero MonoidWithZeroHomClass.toZeroHomClass IsScalarTower.right RingHomClass.toMonoidWithZeroHomClass instRingHomClass TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left Algebra.algebraMap_eq_smul_one map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass
surjective_localRingHom_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	Localization.AtPrime Ideal.comap instRingHomClass Ideal.IsPrime.comap OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Localization.localRingHom Ideal	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass Ideal.IsPrime.comap Localization.isLocalization Submonoid.map_comap_eq_of_surjective surjective_localizationPreserves
surjective_localizationPreserves 📖	mathematical	—	LocalizationPreserves DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass IsLocalization.exists_mk'_eq IsLocalization.map_mk'
surjective_ofLocalizationSpan 📖	mathematical	—	OfLocalizationSpan DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	—	Set.range_eq_univ Set.eq_univ_iff_forall Submodule.mem_of_span_eq_top_of_smul_pow_mem RingHomSurjective.ids Localization.isLocalization IsLocalization.exists_mk'_eq IsLocalization.eq_iff_exists map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass instRingHomClass IsLocalization.eq_mk'_iff_mul_eq IsLocalization.map_mk' IsLocalization.Away.map.eq_1 Localization.awayMap.eq_1 pow_add map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mul_assoc mul_comm
surjective_respectsIso 📖	mathematical	—	RespectsIso DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	—	StableUnderComposition.respectsIso surjective_stableUnderComposition RingEquiv.surjective
surjective_stableUnderComposition 📖	mathematical	—	StableUnderComposition DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	—	—

---

← Back to Index