Basic

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

Statistics

Metric	Count
Definitions map, mk, of, val, comp, id, mapKer, toAlgHom, toRingHom, algebra₁, algebra₂, baseChange, commRing, cotangentEquiv, infinitesimal, instAddCommGroupCotangent, instModuleCotangent, instRingOfIsScalarTower, ker, localization, ofSurjective, self, toInfinitesimal, σ	24
Theorems ext, ext_iff, finite, ker_mk, map_comp, map_id, map_mk, mk_eq_mk_iff_sub_mem, mk_eq_zero_iff, mk_surjective, of_add, of_val, of_zero, smul_eq_zero_of_mem, span_eq_top_of_span_eq_ker, val_add, val_mk, val_of, val_smul, val_smul', val_smul'', val_smul''', val_sub, val_zero, algebraMap_toRingHom, comp_id, comp_toRingHom, ext, ext_iff, id_comp, id_toRingHom, mapKer_apply_coe, toAlgHom_apply, toAlgHom_id, toRingHom_algebraMap, algebraMap_surjective, algebraMap_σ, contangentEquiv_tmul, instIsScalarTowerCotangent, instIsScalarTowerRing, instIsScalarTowerRing_1, instIsScalarTowerRing_2, isScalarTower, ker_infinitesimal, ofSurjective_Ring, ofSurjective_σ, self_Ring, self_σ, σ_injective, σ_smul	50
Total	74

Algebra.Extension

Definitions

Name	Category	Theorems
algebra₁ 📖	CompOp	2 math math: isScalarTower, Algebra.Generators.toExtension_algebra₁
algebra₂ 📖	CompOp	80 math math: Algebra.Presentation.differentials.comm₁₂_single, Cotangent.span_eq_top_of_span_eq_ker, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, H1Cotangent.equiv_apply, Algebra.Generators.cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, formallySmooth_iff_split_injection, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, CotangentSpace.map_id, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Cotangent.val_mk, subsingleton_h1Cotangent, Algebra.Generators.toExtension_algebra₂, Algebra.Generators.exists_presentation_of_free_cotangent, CotangentSpace.map_tmul, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, algebraMap_surjective, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, isScalarTower, Hom.sub_one_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, CotangentSpace.map_toInfinitesimal_bijective, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Cotangent.mk_eq_zero_iff, CotangentSpace.map_sub_map, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', Cotangent.val_smul', contangentEquiv_tmul, Algebra.Generators.cMulXSubOneCotangent_eq, h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, Cotangent.mk_eq_mk_iff_sub_mem, toKaehler_surjective, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Cotangent.mk_surjective, Algebra.Generators.CotangentSpace.exact, Algebra.Generators.repr_CotangentSpaceMap, H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Hom.algebraMap_toRingHom, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, tensorCotangentInvFun_smul_mk, algebraMap_σ, Hom.sub_aux, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.Generators.cotangentRestrict_mk, Algebra.Generators.CotangentSpace.map_toComp_injective, Hom.sub_tmul, Algebra.SubmersivePresentation.sectionCotangent_comp, σ_smul, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.Generators.instFreeCotangentSpaceToExtension, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, instIsScalarTowerRing_2, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, CotangentSpace.map_comp, exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.ker_mk, Cotangent.map_sub_map, cotangentComplex_mk
baseChange 📖	CompOp	—
commRing 📖	CompOp	95 math math: Algebra.Presentation.differentials.comm₁₂_single, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, H1Cotangent.equiv_apply, Algebra.Generators.cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, Cotangent.val_sub, formallySmooth_iff_split_injection, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, CotangentSpace.map_id, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Cotangent.val_mk, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, subsingleton_h1Cotangent, Algebra.Generators.exists_presentation_of_free_cotangent, CotangentSpace.map_tmul, H1Cotangent.val_zero, Cotangent.val_smul''', Cotangent.val_add, instIsScalarTowerRing, algebraMap_surjective, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, isScalarTower, Hom.sub_one_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, Hom.id_toRingHom, CotangentSpace.map_toInfinitesimal_bijective, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Cotangent.mk_eq_zero_iff, CotangentSpace.map_sub_map, Hom.toRingHom_algebraMap, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', Cotangent.val_smul', contangentEquiv_tmul, ker_infinitesimal, Algebra.Generators.cMulXSubOneCotangent_eq, h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, Cotangent.mk_eq_mk_iff_sub_mem, instIsScalarTowerRing_1, toKaehler_surjective, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Cotangent.mk_surjective, Algebra.Generators.CotangentSpace.exact, Hom.subToKer_apply_coe, Algebra.Generators.repr_CotangentSpaceMap, H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Cotangent.val_smul, Hom.algebraMap_toRingHom, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, algebraMap_σ, Hom.sub_aux, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.Generators.cotangentRestrict_mk, Algebra.Generators.CotangentSpace.map_toComp_injective, Cotangent.val_zero, Hom.sub_tmul, Cotangent.of_add, Algebra.SubmersivePresentation.sectionCotangent_comp, σ_smul, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.Generators.instFreeCotangentSpaceToExtension, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, instIsScalarTowerRing_2, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, CotangentSpace.map_comp, exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.ker_mk, Hom.comp_toRingHom, Hom.toAlgHom_id, Hom.toAlgHom_apply, Cotangent.map_sub_map, Cotangent.of_zero, cotangentComplex_mk, Algebra.Generators.toExtension_commRing, Cotangent.val_smul''
cotangentEquiv 📖	CompOp	3 math math: lTensor_cotangentComplex_eq_cotangentComplexBaseChange, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, contangentEquiv_tmul
infinitesimal 📖	CompOp	4 math math: CotangentSpace.map_toInfinitesimal_bijective, ker_infinitesimal, Cotangent.map_toInfinitesimal_bijective, H1Cotangent.map_toInfinitesimal_bijective
instAddCommGroupCotangent 📖	CompOp	75 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, Algebra.Presentation.differentials.comm₁₂_single, Cotangent.span_eq_top_of_span_eq_ker, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, H1Cotangent.equiv_apply, Cotangent.val_sub, formallySmooth_iff_split_injection, h1Cotangentι_injective, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, Cotangent.val_mk, subsingleton_h1Cotangent, Algebra.Generators.exists_presentation_of_free_cotangent, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Cotangent.val_smul''', Cotangent.val_add, Cotangent.finite, instIsScalarTowerCotangent, Hom.sub_one_tmul, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Cotangent.mk_eq_zero_iff, Algebra.Presentation.differentials.surjective_hom₁, Algebra.Generators.Cotangent.surjective_map_ofComp, CotangentSpace.map_sub_map, Algebra.Generators.cotangentRestrict_bijective_of_isCompl, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Cotangent.val_smul', Cotangent.map_comp, Algebra.Generators.cotangentCompAwaySec_apply, Cotangent.map_id, Algebra.Generators.Cotangent.exact, contangentEquiv_tmul, Algebra.Generators.cMulXSubOneCotangent_eq, h1Cotangentι_ext_iff, Cotangent.map_toInfinitesimal_bijective, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, Cotangent.mk_eq_mk_iff_sub_mem, Cotangent.mk_surjective, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, H1Cotangent.map_apply_coe, Cotangent.val_smul, tensorCotangentInvFun_smul_mk, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.Generators.cotangentRestrict_mk, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, Cotangent.val_zero, Hom.sub_tmul, Cotangent.of_add, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.SubmersivePresentation.free_cotangent, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.instFreeCotangentToExtensionUnitLocalizationAway, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, exact_cotangentComplex_toKaehler, Algebra.Generators.basisCotangentAway_apply, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.ker_mk, Algebra.SubmersivePresentation.cotangentEquiv_apply, Cotangent.map_sub_map, Cotangent.of_zero, cotangentComplex_mk, Cotangent.val_smul''
instModuleCotangent 📖	CompOp	88 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, Algebra.Presentation.differentials.comm₁₂_single, Cotangent.span_eq_top_of_span_eq_ker, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, H1Cotangent.equiv_apply, H1Cotangent.map_id, formallySmooth_iff_split_injection, h1Cotangentι_injective, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, Cotangent.val_mk, subsingleton_h1Cotangent, Algebra.Generators.exists_presentation_of_free_cotangent, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Cotangent.val_smul''', Cotangent.finite, Algebra.Generators.H1Cotangent.exact_map_δ, instIsScalarTowerCotangent, Hom.sub_one_tmul, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Cotangent.mk_eq_zero_iff, Algebra.Presentation.differentials.surjective_hom₁, Algebra.Generators.Cotangent.surjective_map_ofComp, Algebra.Generators.H1Cotangent.exact_δ_map, CotangentSpace.map_sub_map, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, Algebra.Generators.cotangentRestrict_bijective_of_isCompl, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Cotangent.val_smul', Cotangent.map_comp, Algebra.Generators.cotangentCompAwaySec_apply, H1Cotangent.equivOfFormallySmooth_apply, Cotangent.map_id, Algebra.Generators.Cotangent.exact, H1Cotangent.equivOfFormallySmooth_symm, contangentEquiv_tmul, Algebra.Generators.cMulXSubOneCotangent_eq, h1Cotangentι_ext_iff, Cotangent.map_toInfinitesimal_bijective, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, Cotangent.mk_eq_mk_iff_sub_mem, Algebra.Generators.H1Cotangent.exact_map_δ', Cotangent.mk_surjective, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, H1Cotangent.map_apply_coe, Cotangent.val_smul, tensorCotangentInvFun_smul_mk, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.H1Cotangent.isLocalizedModule, Algebra.Generators.cotangentRestrict_mk, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, H1Cotangent.equivOfFormallySmooth_toLinearMap, Hom.sub_tmul, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δ_comp_equiv, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.SubmersivePresentation.free_cotangent, Algebra.smoothLocus_eq_compl_support_inter, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.instFreeCotangentToExtensionUnitLocalizationAway, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, exact_cotangentComplex_toKaehler, Algebra.Generators.basisCotangentAway_apply, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.ker_mk, Algebra.H1Cotangent.exact_δ_mapBaseChange, Algebra.SubmersivePresentation.cotangentEquiv_apply, Algebra.Generators.H1Cotangent.δ_map, Cotangent.map_sub_map, Algebra.etaleLocus_eq_compl_support, H1Cotangent.map_comp, cotangentComplex_mk, H1Cotangent.map_toInfinitesimal_bijective, Cotangent.val_smul''
instRingOfIsScalarTower 📖	CompOp	65 math math: Algebra.Presentation.differentials.comm₁₂_single, H1Cotangent.equiv_apply, Algebra.Generators.cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, formallySmooth_iff_split_injection, CotangentSpace.map_id, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, subsingleton_h1Cotangent, CotangentSpace.map_tmul, H1Cotangent.val_zero, Algebra.FormallySmooth.iff_injective_lTensor_residueField, instIsScalarTowerRing, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Hom.sub_one_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, CotangentSpace.map_toInfinitesimal_bijective, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, CotangentSpace.map_sub_map, Hom.toRingHom_algebraMap, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, instIsScalarTowerRing_1, toKaehler_surjective, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Algebra.Generators.CotangentSpace.exact, Hom.subToKer_apply_coe, Algebra.Generators.repr_CotangentSpaceMap, H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, Hom.sub_aux, h1Cotangentι_apply, cotangentComplex_injective_iff, Algebra.Generators.CotangentSpace.map_toComp_injective, Hom.sub_tmul, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.Generators.instFreeCotangentSpaceToExtension, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, instIsScalarTowerRing_2, Algebra.SubmersivePresentation.cotangentComplex_injective, Cotangent.map_mk, CotangentSpace.map_comp, exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Hom.toAlgHom_id, Hom.toAlgHom_apply, Cotangent.map_sub_map, cotangentComplex_mk, Cotangent.val_smul''
ker 📖	CompOp	33 math math: Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Cotangent.val_sub, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Cotangent.val_mk, Algebra.Generators.exists_presentation_of_free_cotangent, Cotangent.val_smul''', Cotangent.val_add, Hom.sub_one_tmul, Cotangent.mk_eq_zero_iff, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Cotangent.val_smul', Hom.mapKer_apply_coe, contangentEquiv_tmul, ker_infinitesimal, Algebra.Generators.cMulXSubOneCotangent_eq, Cotangent.mk_eq_mk_iff_sub_mem, Cotangent.mk_surjective, Hom.subToKer_apply_coe, Cotangent.val_smul, Hom.sub_aux, Algebra.Generators.cotangentRestrict_mk, Cotangent.val_zero, Hom.sub_tmul, Cotangent.of_add, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, Cotangent.ker_mk, Cotangent.of_zero, cotangentComplex_mk, Cotangent.val_smul''
localization 📖	CompOp	—
ofSurjective 📖	CompOp	2 math math: ofSurjective_Ring, ofSurjective_σ
self 📖	CompOp	2 math math: self_σ, self_Ring
toInfinitesimal 📖	CompOp	3 math math: CotangentSpace.map_toInfinitesimal_bijective, Cotangent.map_toInfinitesimal_bijective, H1Cotangent.map_toInfinitesimal_bijective
σ 📖	CompOp	9 math math: Algebra.Generators.toExtension_σ, Cotangent.val_smul''', self_σ, ofSurjective_σ, Cotangent.val_smul, algebraMap_σ, Hom.sub_aux, σ_injective, σ_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_surjective 📖	mathematical	—	Ring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring commRing RingHom.instFunLike algebraMap algebra₂	—	algebraMap_σ
algebraMap_σ 📖	mathematical	—	DFunLike.coe RingHom Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring commRing RingHom.instFunLike algebraMap algebra₂ σ	—	—
contangentEquiv_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Ring commRing Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Algebra.toModule algebra₂ Submodule.module Cotangent TensorProduct.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCotangent TensorProduct.leftModule Algebra.to_smulCommClass instModuleCotangent Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cotangentEquiv TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap LinearMap.instFunLike	—	RingHomInvPair.ids Algebra.to_smulCommClass
instIsScalarTowerCotangent 📖	mathematical	—	IsScalarTower Cotangent Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleCotangent	—	Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass SemigroupAction.mul_smul IsScalarTower.algebraMap_apply
instIsScalarTowerRing 📖	mathematical	—	IsScalarTower Ring Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring commRing instRingOfIsScalarTower Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	—	IsScalarTower.of_algebraMap_eq' IsScalarTower.left
instIsScalarTowerRing_1 📖	mathematical	—	IsScalarTower Ring Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring commRing instRingOfIsScalarTower	—	IsScalarTower.of_algebraMap_eq' IsScalarTower.left IsScalarTower.algebraMap_eq instIsScalarTowerRing RingHom.comp_assoc
instIsScalarTowerRing_2 📖	mathematical	—	IsScalarTower Ring Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring commRing instRingOfIsScalarTower algebra₂	—	IsScalarTower.of_algebraMap_eq' IsScalarTower.left IsScalarTower.algebraMap_eq instIsScalarTowerRing_1 IsScalarTower.right RingHom.comp_assoc isScalarTower
isScalarTower 📖	mathematical	—	IsScalarTower Ring Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra₁ algebra₂	—	—
ker_infinitesimal 📖	mathematical	—	ker infinitesimal Ideal.cotangentIdeal Ring commRing	—	AlgHom.ker_kerSquareLift
ofSurjective_Ring 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Ring ofSurjective	—	—
ofSurjective_σ 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	σ ofSurjective	—	—
self_Ring 📖	mathematical	—	Ring self	—	—
self_σ 📖	mathematical	—	σ self	—	—
σ_injective 📖	mathematical	—	Ring σ	—	algebraMap_σ
σ_smul 📖	mathematical	—	Ring Algebra.toSMul CommRing.toCommSemiring commRing CommSemiring.toSemiring algebra₂ σ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Algebra.smul_def algebraMap_σ

Algebra.Extension.Cotangent

Definitions

Name	Category	Theorems
map 📖	CompOp	14 math math: Algebra.Extension.H1Cotangent.equiv_apply, Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, Algebra.Generators.Cotangent.surjective_map_ofComp, Algebra.Extension.CotangentSpace.map_cotangentComplex, map_comp, map_id, Algebra.Generators.Cotangent.exact, map_toInfinitesimal_bijective, Algebra.Extension.H1Cotangent.map_apply_coe, map_mk, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.Extension.CotangentSpace.map_comp_cotangentComplex, map_sub_map
mk 📖	CompOp	—
of 📖	CompOp	4 math math: of_val, of_add, val_of, of_zero
val 📖	CompOp	11 math math: val_sub, val_mk, val_smul''', val_add, val_smul', of_val, val_smul, ext_iff, val_zero, val_of, val_smul''

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	val	—	—	—
ext_iff 📖	mathematical	—	val	—	ext
finite 📖	mathematical	Ideal.FG Algebra.Extension.Ring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing Algebra.Extension.ker	Module.Finite Algebra.Extension.Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id	—	Submodule.FG.of_restrictScalars Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right Submodule.restrictScalars_top RingHomSurjective.ids LinearMap.range_eq_top mk_surjective Submodule.map_top Submodule.FG.map Submodule.fg_top
ker_mk 📖	mathematical	—	LinearMap.ker Algebra.Extension.Ring Ideal CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Extension.ker Algebra.Extension.Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Submodule.module Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ RingHom.id Submodule Submodule.instSMul Submodule.isScalarTower' Algebra.toSMul Algebra.id SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsScalarTower.right Top.top Submodule.instTop	—	Submodule.ext Submodule.isScalarTower' IsScalarTower.right sq
map_comp 📖	mathematical	—	map Algebra.Extension.Hom.comp LinearMap.comp Algebra.Extension.Cotangent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right	—	LinearMap.ext RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right ext mk_surjective IsScalarTower.left
map_id 📖	mathematical	—	map Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule Algebra.Extension.Hom.id LinearMap.id Algebra.Extension.Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent	—	LinearMap.ext IsScalarTower.left ext mk_surjective Algebra.Extension.Hom.toAlgHom_id Subtype.coe_eta
map_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Algebra.Extension.Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id LinearMap.instFunLike map Algebra.Extension.Ring Algebra.Extension.commRing Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ AlgHom Algebra.Extension.instRingOfIsScalarTower IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike Algebra.Extension.Hom.toAlgHom	—	—
mk_eq_mk_iff_sub_mem 📖	mathematical	—	DFunLike.coe LinearMap Algebra.Extension.Ring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Algebra.Extension.Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Submodule.module Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ LinearMap.instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	—
mk_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap Algebra.Extension.Ring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Algebra.Extension.Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Submodule.module Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id	—	—
mk_surjective 📖	mathematical	—	Algebra.Extension.Ring Ideal CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Extension.ker Algebra.Extension.Cotangent DFunLike.coe LinearMap RingHom.id Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Submodule.module Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ LinearMap.instFunLike	—	Ideal.toCotangent_surjective
of_add 📖	mathematical	—	of Ideal.Cotangent Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.ker AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent Algebra.Extension.Cotangent Algebra.Extension.instAddCommGroupCotangent	—	—
of_val 📖	mathematical	—	of val	—	—
of_zero 📖	mathematical	—	of Ideal.Cotangent Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.ker NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ideal.instAddCommGroupCotangent Algebra.Extension.Cotangent Algebra.Extension.instAddCommGroupCotangent	—	—
smul_eq_zero_of_mem 📖	mathematical	Algebra.Extension.Ring Ideal CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Extension.ker	Ideal.Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ideal.instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid Ideal.instModuleCotangentOfAlgebra Algebra.id NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Ideal.Cotangent.smul_eq_zero_of_mem
span_eq_top_of_span_eq_ker 📖	mathematical	Ideal.span Algebra.Extension.Ring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing Set.range Algebra.Extension.ker	Submodule.span Algebra.Extension.Cotangent AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ LinearMap.instFunLike Eq.le PartialOrder.toPreorder Submodule.instPartialOrder Ideal.subset_span Top.top Submodule Submodule.instTop	—	Submodule.span_eq_top_of_span_eq_top Algebra.Extension.instIsScalarTowerCotangent IsScalarTower.right Eq.le Ideal.subset_span Set.range_comp RingHomSurjective.ids Submodule.map_span Ideal.span.eq_1 Submodule.span_range_subtype_eq_top_iff Submodule.map_top LinearMap.range_eq_top_of_surjective mk_surjective
val_add 📖	mathematical	—	val Algebra.Extension.Cotangent AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Ideal.Cotangent Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.ker Ideal.instAddCommGroupCotangent	—	—
val_mk 📖	mathematical	—	val DFunLike.coe LinearMap Algebra.Extension.Ring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Algebra.Extension.Cotangent Submodule.addCommMonoid AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Submodule.module Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ LinearMap.instFunLike Ideal.Cotangent Ideal.instAddCommGroupCotangent Ideal.instModuleCotangentOfAlgebra Algebra.id Ideal.toCotangent	—	—
val_of 📖	mathematical	—	val of	—	—
val_smul 📖	mathematical	—	val Algebra.Extension.Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Algebra.Extension.instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Algebra.Extension.instModuleCotangent Algebra.id Algebra.Extension.Ring Ideal.Cotangent Algebra.Extension.commRing Algebra.Extension.ker Ideal.instAddCommGroupCotangent Ideal.instModuleCotangentOfAlgebra Algebra.Extension.σ	—	—
val_smul' 📖	mathematical	—	val Algebra.Extension.Ring Algebra.Extension.Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Algebra.Extension.instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid Algebra.Extension.instModuleCotangent Algebra.Extension.algebra₂ Ideal.Cotangent Algebra.Extension.ker Ideal.instAddCommGroupCotangent Ideal.instModuleCotangentOfAlgebra Algebra.id	—	val_smul''' sub_eq_zero sub_smul smul_eq_zero_of_mem map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Algebra.Extension.algebraMap_σ sub_self
val_smul'' 📖	mathematical	—	val Algebra.Extension.Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Algebra.Extension.instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Algebra.Extension.instModuleCotangent Ideal.Cotangent Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.ker Ideal.instAddCommGroupCotangent Ideal.instModuleCotangentOfAlgebra Algebra.Extension.instRingOfIsScalarTower Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	IsScalarTower.left algebraMap_smul Algebra.Extension.instIsScalarTowerCotangent Algebra.Extension.instIsScalarTowerRing_2 val_smul' IsScalarTower.right
val_smul''' 📖	mathematical	—	val Algebra.Extension.Cotangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Algebra.Extension.instAddCommGroupCotangent DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Algebra.Extension.instModuleCotangent Algebra.Extension.Ring Ideal.Cotangent Algebra.Extension.commRing Algebra.Extension.ker Ideal.instAddCommGroupCotangent Ideal.instModuleCotangentOfAlgebra Algebra.id Algebra.Extension.σ DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	—
val_sub 📖	mathematical	—	val Algebra.Extension.Cotangent SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Algebra.Extension.instAddCommGroupCotangent Ideal.Cotangent Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.ker Ideal.instAddCommGroupCotangent	—	—
val_zero 📖	mathematical	—	val Algebra.Extension.Cotangent NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Ideal.Cotangent Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.ker Ideal.instAddCommGroupCotangent	—	—

Algebra.Extension.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	8 math math: comp_id, Algebra.Extension.Cotangent.map_comp, Algebra.Generators.Hom.toExtensionHom_comp, id_comp, Algebra.Extension.CotangentSpace.map_comp, Algebra.Extension.CotangentSpace.map_comp_apply, comp_toRingHom, Algebra.Extension.H1Cotangent.map_comp
id 📖	CompOp	8 math math: Algebra.Extension.H1Cotangent.map_id, Algebra.Extension.CotangentSpace.map_id, comp_id, id_toRingHom, Algebra.Generators.Hom.toExtensionHom_id, Algebra.Extension.Cotangent.map_id, id_comp, toAlgHom_id
mapKer 📖	CompOp	1 math math: mapKer_apply_coe
toAlgHom 📖	CompOp	6 math math: Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, Algebra.Extension.CotangentSpace.map_tmul, sub_aux, Algebra.Extension.Cotangent.map_mk, toAlgHom_id, toAlgHom_apply
toRingHom 📖	CompOp	8 math math: id_toRingHom, toRingHom_algebraMap, Algebra.Generators.Hom.toExtensionHom_toRingHom, subToKer_apply_coe, algebraMap_toRingHom, ext_iff, comp_toRingHom, toAlgHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_toRingHom 📖	mathematical	—	DFunLike.coe RingHom Algebra.Extension.Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing RingHom.instFunLike algebraMap Algebra.Extension.algebra₂ toRingHom	—	—
comp_id 📖	mathematical	—	comp Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule id	—	ext IsScalarTower.left RingHom.ext RingHomCompTriple.comp_eq RingHomCompTriple.ids
comp_toRingHom 📖	mathematical	—	toRingHom comp RingHom.comp Algebra.Extension.Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing	—	—
ext 📖	—	toRingHom	—	—	IsScalarTower.left
ext_iff 📖	mathematical	—	toRingHom	—	ext
id_comp 📖	mathematical	—	comp Algebra.id CommRing.toCommSemiring IsScalarTower.right CommSemiring.toSemiring id	—	ext IsScalarTower.right RingHom.ext RingHomCompTriple.comp_eq RingHomCompTriple.right_ids
id_toRingHom 📖	mathematical	—	toRingHom Algebra.id CommRing.toCommSemiring id RingHom.id Algebra.Extension.Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.Extension.commRing	—	—
mapKer_apply_coe 📖	mathematical	algebraMap Algebra.Extension.Ring CommRing.toCommSemiring Algebra.Extension.commRing CommSemiring.toSemiring toRingHom	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Extension.ker DFunLike.coe LinearMap RingHom.id Submodule.addCommMonoid Submodule.module Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right LinearMap.instFunLike mapKer RingHom RingHom.instFunLike	—	IsScalarTower.right
toAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Extension.Ring CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Extension.commRing Algebra.Extension.instRingOfIsScalarTower Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike toAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike toRingHom	—	IsScalarTower.left
toAlgHom_id 📖	mathematical	—	toAlgHom Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule id AlgHom.id Algebra.Extension.Ring Algebra.Extension.commRing Algebra.Extension.instRingOfIsScalarTower	—	AlgHom.ext IsScalarTower.left
toRingHom_algebraMap 📖	mathematical	—	DFunLike.coe RingHom Algebra.Extension.Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Algebra.Extension.commRing RingHom.instFunLike toRingHom algebraMap Algebra.Extension.instRingOfIsScalarTower Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	—	—

---

← Back to Index