Documentation Verification Report

IntegralClosure

📁 Source: Mathlib/RingTheory/Smooth/IntegralClosure.lean

Statistics

Metric	Count
Definitions `toIntegralClosure`	1
Theorems `toIntegralClosure_bijective_of_isLocalization`, `toIntegralClosure_bijective_of_isLocalizationAway`, `toIntegralClosure_bijective_of_smooth`, `toIntegralClosure_bijective_of_tower`, `toIntegralClosure_injective_of_flat`, `toIntegralClosure_mvPolynomial_bijective`, `exists_derivative_mul_eq_and_isIntegral_coeff`, `mem_adjoin_map_integralClosure_of_isStandardEtale`	8
Total	9

TensorProduct

Definitions

Name	Category	Theorems
`toIntegralClosure` 📖	CompOp	4 math math: `toIntegralClosure_bijective_of_isLocalization`, `toIntegralClosure_bijective_of_smooth`, `toIntegralClosure_mvPolynomial_bijective`, `toIntegralClosure_injective_of_flat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIntegralClosure_bijective_of_isLocalization` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Algebra.toModule` `Subalgebra.instModuleSubtypeMem` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `toIntegralClosure`	—	`Algebra.to_smulCommClass` `isScalarTower_left` `IsScalarTower.right` `RingHom.IsIntegralElem.of_comp` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left` `isScalarTower` `RingHom.IsIntegralElem.map` `IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `IsLocalization.integralClosure` `Algebra.TensorProduct.right_isScalarTower` `IsLocalization.tensorRight` `Subalgebra.instIsScalarTowerSubtypeMem` `AlgHom.coe_restrictScalars'` `AlgEquiv.coe_restrictScalars'` `AlgEquiv.coe_algHom` `Algebra.TensorProduct.ext` `IsLocalization.algHom_ext` `IsScalarTower.to_smulCommClass` `Algebra.ext_id` `AlgHom.ext` `IsLocalization.map_eq` `AlgEquiv.bijective`
`toIntegralClosure_bijective_of_isLocalizationAway` 📖	—	`Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsScalarTower` `Algebra.toSMul` `IsLocalization.Away` `Set` `Set.instMembership` `Function.Bijective` `TensorProduct` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Algebra.toModule` `Subalgebra.instModuleSubtypeMem` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `toIntegralClosure`	—	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.of_algHom` `isLocalizedModule_iff_isLocalization` `IsLocalization.tensorProduct_tensorProduct` `RingHom.ext` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `isScalarTower_left` `IsIntegral.tower_top` `IsIntegral.map` `IsScalarTower.left` `AlgHom.algHomClass` `IsScalarTower.of_algebraMap_eq'` `IsLocalization.integralClosure` `bijective_of_isLocalized_span` `smulCommClass_self` `LinearMap.IsScalarTower.compatibleSMul` `Subalgebra.instIsScalarTowerSubtypeMem` `IsLocalizedModule.ext` `IsLocalizedModule.map_units` `AlgebraTensorModule.curry_injective` `Subalgebra.isScalarTower_right` `RingHomCompTriple.ids` `LinearMap.ext_ring` `LinearMap.ext` `IsLocalizedModule.map_apply`
`toIntegralClosure_bijective_of_smooth` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Algebra.toModule` `Subalgebra.instModuleSubtypeMem` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `toIntegralClosure`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial` `PrimeSpectrum.isPrime` `Algebra.Smooth.finitePresentation` `Algebra.FormallySmooth.instLocalization` `Algebra.Smooth.formallySmooth` `toIntegralClosure_bijective_of_tower` `toIntegralClosure_mvPolynomial_bijective` `toIntegralClosure_bijective_of_isLocalizationAway` `Ideal.exists_le_maximal` `Ideal.IsMaximal.isPrime'` `Ideal.subset_span` `Set.mem_range_self` `OreLocalization.instIsScalarTower` `Localization.isLocalization` `Set.forall_subtype_range_iff`
`toIntegralClosure_bijective_of_tower` 📖	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Algebra.toModule` `Subalgebra.instModuleSubtypeMem` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `toIntegralClosure`	—	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `AlgEquiv.coe_algHom` `Algebra.TensorProduct.ext` `isScalarTower_left` `Subalgebra.instIsScalarTowerSubtypeMem` `Algebra.ext_id` `AlgHom.ext` `Algebra.TensorProduct.cancelBaseChange_symm_tmul` `Algebra.TensorProduct.cancelBaseChange_tmul` `one_smul` `AlgEquiv.bijective`
`toIntegralClosure_injective_of_flat` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Algebra.toModule` `Subalgebra.instModuleSubtypeMem` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `toIntegralClosure`	—	`Function.Injective.of_comp` `Algebra.to_smulCommClass` `AlgHom.coe_comp` `toIntegralClosure.eq_1` `AlgHom.val_comp_codRestrict` `Module.Flat.lTensor_preserves_injective_linearMap` `Subtype.val_injective`
`toIntegralClosure_mvPolynomial_bijective` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `MvPolynomial` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Subalgebra.toCommRing` `Algebra.toModule` `MvPolynomial.algebra` `Algebra.id` `Subalgebra.instModuleSubtypeMem` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `toIntegralClosure`	—	`Algebra.to_smulCommClass` `toIntegralClosure_injective_of_flat` `Module.Flat.of_free` `MvPolynomial.instFree` `RingEquiv.map_mul'` `RingEquiv.map_add'` `IsScalarTower.right` `MvPolynomial.ringHom_ext'` `RingHom.ext` `MvPolynomial.ext` `MvPolynomial.smulCommClass` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `MvPolynomial.rTensorAlgEquiv_apply` `MvPolynomial.coeff_map` `MvPolynomial.coeff_rTensorAlgHom_tmul` `MvPolynomial.coeff_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MvPolynomial.map_comp_C` `MvPolynomial.coeff_X'` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MvPolynomial.map_X` `MvPolynomial.isIntegral_iff_isIntegral_coeff` `IsIntegral.map` `isScalarTower_left` `IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `MvPolynomial.mem_range_map_iff_coeffs_subset` `Subtype.range_coe_subtype` `AlgEquiv.injective` `AlgEquiv.surjective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgEquiv.symm_apply_apply` `IsScalarTower.to_smulCommClass` `MvPolynomial.isScalarTower` `Algebra.TensorProduct.ext` `MvPolynomial.algHom_ext` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.ext`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_derivative_mul_eq_and_isIntegral_coeff` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.Monic` `IsIntegral` `CommRing.toRing` `Polynomial.coeff` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom` `Ideal.span` `Set` `Set.instSingletonSet`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative`	—	`RingHom.instRingHomClass` `subsingleton_or_nontrivial` `Polynomial.Monic.natDegree_eq_zero` `Ideal.span_singleton_one` `Ne.trans_eq` `RingHom.ker_ne_top` `RingHom.domain_nontrivial` `Polynomial.Monic.exists_splits_map` `Polynomial.splits_iff_exists_multiset` `IsScalarTower.of_algebraMap_eq'` `IsIntegral.of_aeval_monic_of_isIntegral_coeff` `Polynomial.Monic.map` `Polynomial.Monic.natDegree_map` `Polynomial.Monic.leadingCoeff` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_mul` `Polynomial.eval_multiset_prod` `Multiset.prod_eq_zero` `Multiset.map_map` `Multiset.map_congr` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `sub_self` `isIntegral_zero` `Polynomial.coeff_map` `IsIntegral.algebraMap` `Polynomial.natDegree_multiset_prod_X_sub_C_eq_card` `Polynomial.map_mul` `Polynomial.derivative_map` `Polynomial.derivative_prod` `Multiset.sum_map_mul_right` `Multiset.sum_map_sub` `Multiset.dvd_sum` `Polynomial.derivative_sub` `Polynomial.derivative_X` `Polynomial.derivative_C` `sub_zero` `mul_one` `Multiset.cons_erase` `Multiset.map_cons` `Multiset.prod_cons` `mul_comm` `mul_dvd_mul_left` `Polynomial.eval_map_algebraMap` `Polynomial.map_modByMonic` `Polynomial.div_modByMonic_unique` `sub_eq_iff_eq_add'` `Polynomial.degree_lt_degree` `Ne.bot_lt` `LE.le.trans` `instLeftCommutativeOfCommutativeOfAssociative` `Polynomial.natDegree_multiset_sum_le` `Multiset.max_le_of_forall_le` `Polynomial.natDegree_mul_C_le` `Polynomial.natDegree_multiset_prod_le` `Polynomial.natDegree_sub_C` `Polynomial.natDegree_X` `Multiset.map_const'` `Multiset.card_erase_of_mem` `Multiset.sum_replicate` `Polynomial.isScalarTower` `IsScalarTower.right` `Ideal.span_le` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.liftOfSurjective_apply` `IsIntegral.map` `IsScalarTower.left` `IsIntegral.tower_bot` `instIsScalarTowerPolynomial_1` `Polynomial.map_injective` `FaithfulSMul.algebraMap_injective` `Module.FaithfullyFlat.faithfulSMul` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsIntegral.multiset_sum` `IsIntegral.mul` `IsIntegral.multiset_prod` `Polynomial.coeff_sub` `IsIntegral.sub` `Polynomial.coeff_X` `Polynomial.coeff_C` `Multiset.mem_of_mem_erase` `Polynomial.modByMonic_eq_sub_mul_div` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Eq.ge` `Ideal.mem_span_singleton_self` `MulZeroClass.zero_mul` `Polynomial.isIntegral_iff_isIntegral_coeff`
`mem_adjoin_map_integralClosure_of_isStandardEtale` 📖	mathematical	`IsIntegral` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instRing` `CommRing.toRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	`Subalgebra` `Algebra.TensorProduct.instSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `SetLike.coe` `Algebra.TensorProduct.instAlgebra` `Subalgebra.map` `Algebra.TensorProduct.includeRight` `integralClosure`	—	`Algebra.to_smulCommClass` `Algebra.IsStandardEtale.nonempty_standardEtalePresentation` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsLocalization.isLocalization_of_algEquiv` `Localization.isLocalization` `RingEquiv.map_mul'` `RingEquiv.map_add'` `IsScalarTower.to_smulCommClass` `IsScalarTower.of_algHom` `IsIntegral.exists_multiple_integral_of_isLocalization` `TensorProduct.isScalarTower_left` `IsIntegral.mul` `isIntegral_algebraMap` `Polynomial.Monic.finite_adjoinRoot` `StandardEtalePair.monic_f` `IsLocalization.lift_eq` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `StandardEtalePresentation.equivRing_symm_X` `isIntegral_trans` `Algebra.IsIntegral.of_finite` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.algebraMap_smul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `add_comm` `AlgEquiv.surjective` `IsLocalization.exists_mk'_eq` `dvd_refl` `Polynomial.ringHom_ext'` `RingHom.ext` `Polynomial.map_C` `AdjoinRoot.map_of` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.map_X` `AdjoinRoot.map_root` `IsIntegral.map` `AdjoinRoot.instIsScalarTower` `IsScalarTower.left` `Algebra.IsIntegral.isIntegral` `Algebra.TensorProduct.includeRight_apply` `Polynomial.aeval_algHom_apply` `Polynomial.aeval_map_algebraMap` `AlgEquiv.eq_symm_apply` `Algebra.TensorProduct.tmul_pow` `one_pow` `TensorProduct.isScalarTower` `IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap` `map_mul` `mul_assoc` `pow_add` `Algebra.smul_def` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquiv.symm_apply_apply` `AlgEquiv.apply_symm_apply` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Polynomial.isScalarTower` `exists_derivative_mul_eq_and_isIntegral_coeff` `AdjoinRoot.mk_surjective` `Polynomial.coeff_map` `Ideal.mk_ker` `Ideal.instIsTwoSided_1` `Subalgebra.mem_toSubmodule` `Submodule.smul_mem_iff_of_isUnit` `IsUnit.mul` `StandardEtalePair.HasMap.isUnit_derivative_f` `StandardEtalePresentation.hasMap` `IsUnit.pow` `AlgEquiv.injective` `IsLocalization.mk'.congr_simp` `Polynomial.eval₂_C` `AdjoinRoot.lift_of` `AlgEquiv.commutes` `Polynomial.eval₂_X` `AdjoinRoot.lift_root` `Polynomial.eval₂_eq_sum_range` `sum_mem` `Submodule.addSubmonoidClass` `Subalgebra.mul_mem` `Algebra.subset_adjoin` `pow_mem` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `Subalgebra.algebraMap_mem`

---

← Back to Index