Basic

📁 Source: Mathlib/RingTheory/Unramified/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `base_change`, `comp`, `comp_injective`, `ext`, `ext'`, `ext_of_iInf`, `iff_comp_injective`, `iff_comp_injective_of_small`, `iff_of_equiv`, `inst`, `instLocalization`, `lift_unique`, `lift_unique'`, `lift_unique_of_ringHom`, `localization_base`, `localization_map`, `of_comp`, `of_equiv`, `of_isLocalization`, `of_restrictScalars`, `of_surjective`, `quotient`, `subsingleton_kaehlerDifferential`, `baseChange`, `comp`, `finiteType`, `formallyUnramified`, `of_equiv`, `of_isLocalization_Away`, `formallyUnramified_iff`	30
Total	30

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`formallyUnramified_iff` 📖	mathematical	—	`FormallyUnramified` `KaehlerDifferential`	—	—

Algebra.FormallyUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_change` 📖	mathematical	—	`Algebra.FormallyUnramified` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `Ideal.instIsTwoSided_1` `iff_comp_injective` `Algebra.TensorProduct.ext` `IsScalarTower.right` `IsScalarTower.of_algebraMap_eq'` `AlgHom.subsingleton` `Unique.instSubsingleton` `IsScalarTower.to_smulCommClass` `ext` `TensorProduct.isScalarTower_left` `AlgHom.congr_fun`
`comp` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`Ideal.instIsTwoSided_1` `iff_comp_injective` `lift_unique` `IsScalarTower.right` `AlgHom.comp_assoc` `AlgHom.congr_fun` `AlgHom.ext` `ext`
`comp_injective` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`AlgHom` `Ring.toSemiring` `CommRing.toRing` `HasQuotient.Quotient` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `AlgHom.comp` `Ideal.Quotient.mkₐ`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.isScalarTower` `IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Function.Surjective.subsingleton` `Algebra.to_smulCommClass` `IsScalarTower.right` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `Submodule.isScalarTower'` `RingHomInvPair.ids` `Unique.instSubsingleton` `subsingleton_kaehlerDifferential` `Equiv.surjective`
`ext` 📖	—	`IsNilpotent` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `AlgHom` `AlgHom.funLike`	—	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `lift_unique` `AlgHom.ext`
`ext'` 📖	—	`IsNilpotent` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `RingHom.ker` `RingHom` `Ring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	—	—	`IsScalarTower.right` `RingHom.instRingHomClass` `lift_unique_of_ringHom` `RingHom.ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`ext_of_iInf` 📖	—	`iInf` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `AlgHom` `AlgHom.funLike`	—	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `AlgHom.ext` `pow_zero` `Ideal.one_eq_top` `Unique.instSubsingleton` `ext` `RingHom.instRingHomClass` `Ideal.map_quotient_self` `Ideal.Quotient.eq` `map_sub` `RingHomClass.toAddMonoidHomClass` `Ideal.mem_comap` `Ideal.comap_map_of_surjective'` `Ideal.Quotient.mk_surjective` `sup_eq_left` `Ideal.mk_ker` `Ideal.pow_le_self` `sub_eq_zero` `Ideal.mem_bot` `Ideal.mem_iInf` `Ideal.Quotient.eq_zero_iff_mem` `DFunLike.congr_fun`
`iff_comp_injective` 📖	mathematical	—	`Algebra.FormallyUnramified` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `CommRing.toRing` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `AlgHom.comp` `Ideal.Quotient.mkₐ`	—	`iff_comp_injective_of_small` `UnivLE.small` `UnivLE.self`
`iff_comp_injective_of_small` 📖	mathematical	—	`Algebra.FormallyUnramified` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `CommRing.toRing` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `AlgHom.comp` `Ideal.Quotient.mkₐ`	—	`Ideal.instIsTwoSided_1` `comp_injective` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `EquivLike.toEmbeddingLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Ideal.map_symm` `IsScalarTower.right` `Ideal.map_pow` `Ideal.map_bot` `equivShrink_symm_sub` `Equiv.symm_apply_apply` `RingHom.instRingHomClass` `Function.Injective.nontrivial` `Algebra.to_smulCommClass` `Module.End.instNontrivial` `Equiv.injective` `Submodule.Quotient.instSmallQuotient` `TensorProduct.instSmall` `AlgHom.ker_kerSquareLift` `Ideal.cotangentIdeal_square` `AlgHom.ext` `RingHom.kerLift_injective` `RingHom.instIsTwoSidedKer` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `DFunLike.congr_fun`
`iff_of_equiv` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`of_equiv`
`inst` 📖	mathematical	—	`Algebra.FormallyUnramified` `Algebra.id` `CommRing.toCommSemiring`	—	`Ideal.instIsTwoSided_1` `iff_comp_injective` `AlgHom.subsingleton` `Unique.instSubsingleton`
`instLocalization` 📖	mathematical	—	`Algebra.FormallyUnramified` `Localization` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`of_isLocalization` `Localization.isLocalization` `comp` `OreLocalization.instIsScalarTower` `IsScalarTower.right`
`lift_unique` 📖	—	`IsNilpotent` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `AlgHom.comp` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `Ideal.Quotient.mkₐ`	—	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `Ideal.IsNilpotent.induction_on` `comp_injective` `AlgHom.ext` `AlgHom.congr_fun` `Ideal.Quotient.eq` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Ideal.mem_quotient_iff_mem`
`lift_unique'` 📖	—	`IsNilpotent` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `RingHom.ker` `RingHom` `Ring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp`	—	—	`IsScalarTower.right` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `ext'` `AlgHom.congr_fun`
`lift_unique_of_ringHom` 📖	—	`IsNilpotent` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `RingHom.ker` `RingHom` `Ring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `RingHom.comp` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	—	—	`IsScalarTower.right` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `lift_unique` `AlgHom.ext` `Ideal.instIsTwoSided_1` `RingHom.congr_fun` `map_sub` `RingHomClass.toAddMonoidHomClass`
`localization_base` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`of_restrictScalars`
`localization_map` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `localization_base` `comp` `of_isLocalization`
`of_comp` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`of_restrictScalars`
`of_equiv` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`Ideal.instIsTwoSided_1` `iff_comp_injective` `AlgHom.comp_id` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.comp_symm` `AlgHom.comp_assoc` `comp_injective`
`of_isLocalization` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`Ideal.instIsTwoSided_1` `iff_comp_injective` `AlgHom.coe_ringHom_injective` `IsLocalization.ringHom_ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.ext` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left`
`of_restrictScalars` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	`Ideal.instIsTwoSided_1` `iff_comp_injective` `AlgHom.restrictScalars_injective` `IsScalarTower.of_algebraMap_eq'` `ext` `IsScalarTower.right` `AlgHom.congr_fun`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Algebra.FormallyUnramified`	—	`Ideal.instIsTwoSided_1` `iff_comp_injective` `AlgHom.ext` `AlgHom.comp_apply` `comp_injective` `DFunLike.congr_fun`
`quotient` 📖	mathematical	—	`Algebra.FormallyUnramified` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient`	—	`of_surjective` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `Ideal.Quotient.mk_surjective` `Ideal.instIsTwoSided_1`
`subsingleton_kaehlerDifferential` 📖	mathematical	—	`KaehlerDifferential`	—	—

Algebra.Unramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange` 📖	mathematical	—	`Algebra.Unramified` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `Algebra.FormallyUnramified.base_change` `formallyUnramified` `Algebra.FiniteType.baseChange` `finiteType`
`comp` 📖	mathematical	—	`Algebra.Unramified`	—	`Algebra.FormallyUnramified.comp` `formallyUnramified` `Algebra.FiniteType.trans` `finiteType`
`finiteType` 📖	mathematical	—	`Algebra.FiniteType` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	—
`formallyUnramified` 📖	mathematical	—	`Algebra.FormallyUnramified`	—	—
`of_equiv` 📖	mathematical	—	`Algebra.Unramified`	—	`Algebra.FormallyUnramified.of_equiv` `formallyUnramified` `Algebra.FiniteType.equiv` `finiteType`
`of_isLocalization_Away` 📖	mathematical	—	`Algebra.Unramified`	—	`Algebra.FormallyUnramified.of_isLocalization` `Algebra.FiniteType.of_finitePresentation` `IsLocalization.Away.finitePresentation`

---

← Back to Index