Documentation Verification Report

SurjectiveOnStalks

📁 Source: Mathlib/RingTheory/SurjectiveOnStalks.lean

Statistics

Metric	Count
Definitions `SurjectiveOnStalks`	1
Theorems `surjectiveOnStalks`, `baseChange`, `baseChange'`, `comp`, `exists_mul_eq_tmul`, `localRingHom_surjective`, `of_comp`, `tensorProductMap`, `surjectiveOnStalks_iff_forall_ideal`, `surjectiveOnStalks_iff_forall_maximal`, `surjectiveOnStalks_iff_forall_maximal'`, `surjectiveOnStalks_iff_of_isLocalHom`, `surjectiveOnStalks_of_exists_div`, `surjectiveOnStalks_of_isLocalization`, `surjectiveOnStalks_of_surjective`, `surjective_localRingHom_iff`	16
Total	17

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjectiveOnStalks` 📖	mathematical	—	`RingHom.SurjectiveOnStalks` `toRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`RingHom.surjectiveOnStalks_of_surjective` `surjective`

RingHom

Definitions

Name	Category	Theorems
`SurjectiveOnStalks` 📖	MathDef	14 math math: `AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine`, `surjectiveOnStalks_of_surjective`, `AlgebraicGeometry.SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks`, `AlgebraicGeometry.IsPreimmersion.Spec_map_iff`, `Ideal.surjectiveOnStalks_residueField`, `surjectiveOnStalks_of_exists_div`, `surjectiveOnStalks_iff_forall_maximal'`, `AlgebraicGeometry.SurjectiveOnStalks.Spec_iff`, `AlgebraicGeometry.IsPreimmersion.SpecMap_iff`, `RingEquiv.surjectiveOnStalks`, `surjectiveOnStalks_iff_of_isLocalHom`, `surjectiveOnStalks_iff_forall_ideal`, `surjectiveOnStalks_of_isLocalization`, `surjectiveOnStalks_iff_forall_maximal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjectiveOnStalks_iff_forall_ideal` 📖	mathematical	—	`SurjectiveOnStalks` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`instRingHomClass` `Ideal.IsPrime.comap` `Ideal.exists_le_maximal` `Ideal.IsMaximal.isPrime` `Ideal.IsPrime.ne_top`
`surjectiveOnStalks_iff_forall_maximal` 📖	mathematical	—	`SurjectiveOnStalks` `Localization.AtPrime` `CommRing.toCommSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `instRingHomClass` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'` `DFunLike.coe` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom` `Ideal`	—	`instRingHomClass` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'` `Ideal.IsMaximal.isPrime` `Ideal.exists_le_maximal` `Ideal.IsPrime.ne_top`
`surjectiveOnStalks_iff_forall_maximal'` 📖	mathematical	—	`SurjectiveOnStalks` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`instRingHomClass` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'`
`surjectiveOnStalks_iff_of_isLocalHom` 📖	mathematical	—	`SurjectiveOnStalks` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike`	—	`instRingHomClass` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `surjective_localRingHom_iff` `isUnit_of_map_unit` `IsUnit.mul_right_injective` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsUnit.mul_val_inv` `one_mul` `surjectiveOnStalks_of_surjective`
`surjectiveOnStalks_of_exists_div` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`SurjectiveOnStalks`	—	`surjectiveOnStalks_iff_forall_ideal` `Ideal.eq_top_of_isUnit_mem` `one_mul`
`surjectiveOnStalks_of_isLocalization` 📖	mathematical	—	`SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`surjectiveOnStalks_of_exists_div` `IsLocalization.exists_mk'_eq` `IsLocalization.map_units` `IsLocalization.mk'_spec'`
`surjectiveOnStalks_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike`	`SurjectiveOnStalks`	—	`surjectiveOnStalks_iff_forall_ideal` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass` `mul_one` `one_mul`
`surjective_localRingHom_iff` 📖	mathematical	—	`Localization.AtPrime` `CommRing.toCommSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `instRingHomClass` `Ideal.IsPrime.comap` `DFunLike.coe` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`instRingHomClass` `Ideal.IsPrime.comap` `Localization.isLocalization` `IsLocalization.exists_mk'_eq` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Localization.le_comap_primeCompl_iff` `ge_of_eq` `IsLocalization.eq_iff_exists` `one_mul` `Submonoid.coe_one` `IsLocalization.mk'_eq_iff_eq` `Localization.localRingHom_mk'` `Localization.ind` `Submonoid.mul_mem` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `Ideal.mul_mem_left` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Localization.mk_eq_mk'` `IsLocalization.mk'.congr_simp` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`

RingHom.SurjectiveOnStalks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange` 📖	mathematical	`RingHom.SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `RingHom.surjective_localRingHom_iff` `exists_mul_eq_tmul` `RingHom.map_mul` `Algebra.smul_def` `Ideal.mem_comap` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Algebra.algebraMap_eq_smul_one` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `smulCommClass_self` `TensorProduct.tmul_smul` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `Algebra.smul_mul_assoc` `one_mul` `mul_one` `TensorProduct.smul_tmul'` `smul_mul_assoc`
`baseChange'` 📖	mathematical	`RingHom.SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommRing` `AlgHom.toRingHom` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	—	`Algebra.to_smulCommClass` `comp` `RingHom.surjectiveOnStalks_of_surjective` `AlgEquiv.surjective` `baseChange`
`comp` 📖	mathematical	`RingHom.SurjectiveOnStalks`	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Localization.localRingHom_comp` `RingHom.coe_comp`
`exists_mul_eq_tmul` 📖	mathematical	`RingHom.SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.toSMul` `TensorProduct` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`TensorProduct.induction_on` `Algebra.to_smulCommClass` `IsScalarTower.right` `one_smul` `Submonoid.one_mem` `MulZeroClass.mul_zero` `TensorProduct.zero_tmul` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `RingHom.surjective_localRingHom_iff` `Algebra.smul_def` `Submonoid.mul_mem` `Algebra.TensorProduct.tmul_mul_tmul` `one_mul` `mul_comm` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `smul_smul_smul_comm` `mul_add` `Distrib.leftDistribClass` `mul_assoc` `smul_mul_assoc` `TensorProduct.add_tmul`
`localRingHom_surjective` 📖	mathematical	`RingHom.SurjectiveOnStalks` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`Localization.AtPrime` `DFunLike.coe` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom`	—	`RingHom.instRingHomClass`
`of_comp` 📖	—	`RingHom.SurjectiveOnStalks` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—	`Function.Surjective.of_comp` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `RingHom.coe_comp` `Localization.localRingHom_comp`
`tensorProductMap` 📖	mathematical	`RingHom.SurjectiveOnStalks` `AlgHom.toRingHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.TensorProduct.map`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.left` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Algebra.TensorProduct.ext` `TensorProduct.isScalarTower` `AlgHom.ext` `Algebra.TensorProduct.map_comp_includeLeft` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `TensorProduct.isScalarTower_left` `Algebra.TensorProduct.map_restrictScalars_comp_includeRight` `comp` `RingEquiv.surjectiveOnStalks`

---

← Back to Index