Extension

📁 Source: Mathlib/Algebra/Lie/Extension.lean

Statistics

Metric	Count
Definitions Extension, L, incl, instLieAlgebra, instLieRing, ofAlg, ofTwoCocycle, oneCochainOfTwoSplitting, proj, ringModuleOf, toKer, twoCocycleOf, IsExtension, extension, kerEquivRange, ofCoboundary, instAddCommGroupOfTwoCocycle, instL, instLieRingL, instLieRingOfTwoCocycle, instModuleOfTwoCocycle, instOfTwoCocycle, ofProd, ofTwoCocycle, carrier	25
Theorems IsExtension, bracket, d₁₂_oneCochainOfTwoSplitting, incl_apply_mem_ker, incl_injective, instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, lieModuleOf, lie_apply_proj_of_leftInverse_eq, lie_incl_mem_ker, lie_toKer_apply, ofTwoCocycle_incl_apply, ofTwoCocycle_proj_apply, oneCochainOfTwoSplitting_apply, proj_incl, proj_surjective, ringModuleOf_bracket, ringModuleOf_bracket_proj, toKer_bracket, twoCocycleOf_coe_coe, exact, extension_L, extension_incl, extension_instLieAlgebra, extension_instLieRing, extension_proj, ker_eq_bot, range_eq_top, ofCoboundary_invFun, ofCoboundary_toFun, bracket_ofTwoCocycle, isExtension_of_surjective, of_add, of_nsmul, of_smul, of_symm_add, of_symm_nsmul, of_symm_smul, of_symm_zero, of_zero, range_eq_ker_iff	40
Total	65

Algebra

Definitions

Name	Category	Theorems
Extension 📖	CompData	—

LieAlgebra

Definitions

Name	Category	Theorems
IsExtension 📖	CompData	2 math math: isExtension_of_surjective, Extension.IsExtension
instAddCommGroupOfTwoCocycle 📖	CompOp	8 math math: of_smul, of_zero, of_add, of_symm_nsmul, of_symm_zero, of_symm_add, of_symm_smul, of_nsmul
instL 📖	CompOp	1 math math: Extension.bracket
instLieRingL 📖	CompOp	4 math math: Extension.lie_incl_mem_ker, Extension.bracket, Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, Extension.lie_toKer_apply
instLieRingOfTwoCocycle 📖	CompOp	4 math math: bracket_ofTwoCocycle, LieEquiv.ofCoboundary_toFun, Extension.bracket, LieEquiv.ofCoboundary_invFun
instModuleOfTwoCocycle 📖	CompOp	2 math math: of_smul, of_symm_smul
instOfTwoCocycle 📖	CompOp	3 math math: LieEquiv.ofCoboundary_toFun, Extension.bracket, LieEquiv.ofCoboundary_invFun
ofProd 📖	CompOp	11 math math: of_smul, bracket_ofTwoCocycle, LieEquiv.ofCoboundary_toFun, of_zero, of_add, LieEquiv.ofCoboundary_invFun, of_symm_nsmul, of_symm_zero, of_symm_add, of_symm_smul, of_nsmul
ofTwoCocycle 📖	CompData	12 math math: of_smul, bracket_ofTwoCocycle, LieEquiv.ofCoboundary_toFun, of_zero, Extension.bracket, of_add, LieEquiv.ofCoboundary_invFun, of_symm_nsmul, of_symm_zero, of_symm_add, of_symm_smul, of_nsmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_ofTwoCocycle 📖	mathematical	—	Bracket.bracket ofTwoCocycle LieRingModule.toBracket instLieRingOfTwoCocycle LieRing.toAddCommGroup lieRingSelfModule DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofProd Equiv.symm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain Submodule.addCommMonoid Submodule.module LieModule.Cohomology.twoCocycle	—	smulCommClass_self LinearMap.instSMulCommClass
isExtension_of_surjective 📖	mathematical	DFunLike.coe LieHom LieHom.instFunLike	IsExtension LieSubmodule LieRing.toAddCommGroup toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker LieIdeal.lieRing LieIdeal.lieAlgebra LieIdeal.incl	—	LieIdeal.ker_incl LieHom.range_eq_top LieIdeal.incl_range
of_add 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike ofProd Prod.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup instAddCommGroupOfTwoCocycle	—	smulCommClass_self LinearMap.instSMulCommClass
of_nsmul 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike ofProd AddMonoid.toNatSMul Prod.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup instAddCommGroupOfTwoCocycle	—	smulCommClass_self LinearMap.instSMulCommClass
of_smul 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike ofProd Prod.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid toModule instAddCommGroupOfTwoCocycle instModuleOfTwoCocycle	—	smulCommClass_self LinearMap.instSMulCommClass
of_symm_add 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofProd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupOfTwoCocycle Prod.instAdd LieRing.toAddCommGroup	—	smulCommClass_self LinearMap.instSMulCommClass
of_symm_nsmul 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofProd AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupOfTwoCocycle Prod.instAddMonoid LieRing.toAddCommGroup	—	smulCommClass_self LinearMap.instSMulCommClass
of_symm_smul 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofProd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupOfTwoCocycle DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleOfTwoCocycle Prod.instSMul LieRing.toAddCommGroup toModule	—	smulCommClass_self LinearMap.instSMulCommClass
of_symm_zero 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofProd NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupOfTwoCocycle Prod.instZero LieRing.toAddCommGroup	—	smulCommClass_self LinearMap.instSMulCommClass
of_zero 📖	mathematical	—	DFunLike.coe Equiv ofTwoCocycle EquivLike.toFunLike Equiv.instEquivLike ofProd Prod.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup instAddCommGroupOfTwoCocycle	—	smulCommClass_self LinearMap.instSMulCommClass

LieAlgebra.Extension

Definitions

Name	Category	Theorems
L 📖	CompOp	15 math math: incl_apply_mem_ker, toKer_bracket, incl_injective, LieAlgebra.IsExtension.extension_L, lie_incl_mem_ker, ringModuleOf_bracket, ofTwoCocycle_proj_apply, bracket, ofTwoCocycle_incl_apply, proj_incl, ringModuleOf_bracket_proj, proj_surjective, instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, lie_toKer_apply, IsExtension
incl 📖	CompOp	8 math math: incl_apply_mem_ker, LieAlgebra.IsExtension.extension_incl, incl_injective, lie_incl_mem_ker, ofTwoCocycle_incl_apply, proj_incl, lie_toKer_apply, IsExtension
instLieAlgebra 📖	CompOp	14 math math: incl_apply_mem_ker, toKer_bracket, incl_injective, lie_incl_mem_ker, ringModuleOf_bracket, LieAlgebra.IsExtension.extension_instLieAlgebra, ofTwoCocycle_proj_apply, ofTwoCocycle_incl_apply, proj_incl, ringModuleOf_bracket_proj, proj_surjective, instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, lie_toKer_apply, IsExtension
instLieRing 📖	CompOp	14 math math: incl_apply_mem_ker, toKer_bracket, incl_injective, lie_incl_mem_ker, LieAlgebra.IsExtension.extension_instLieRing, ringModuleOf_bracket, ofTwoCocycle_proj_apply, ofTwoCocycle_incl_apply, proj_incl, ringModuleOf_bracket_proj, proj_surjective, instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, lie_toKer_apply, IsExtension
ofAlg 📖	CompOp	1 math math: bracket
ofTwoCocycle 📖	CompOp	3 math math: ofTwoCocycle_proj_apply, bracket, ofTwoCocycle_incl_apply
oneCochainOfTwoSplitting 📖	CompOp	2 math math: d₁₂_oneCochainOfTwoSplitting, oneCochainOfTwoSplitting_apply
proj 📖	CompOp	12 math math: incl_apply_mem_ker, toKer_bracket, lie_incl_mem_ker, ringModuleOf_bracket, ofTwoCocycle_proj_apply, proj_incl, LieAlgebra.IsExtension.extension_proj, ringModuleOf_bracket_proj, proj_surjective, instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, lie_toKer_apply, IsExtension
ringModuleOf 📖	CompOp	6 math math: toKer_bracket, lieModuleOf, ringModuleOf_bracket, d₁₂_oneCochainOfTwoSplitting, ringModuleOf_bracket_proj, twoCocycleOf_coe_coe
toKer 📖	CompOp	6 math math: toKer_bracket, ringModuleOf_bracket, ringModuleOf_bracket_proj, twoCocycleOf_coe_coe, lie_toKer_apply, oneCochainOfTwoSplitting_apply
twoCocycleOf 📖	CompOp	2 math math: d₁₂_oneCochainOfTwoSplitting, twoCocycleOf_coe_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsExtension 📖	mathematical	—	LieAlgebra.IsExtension L instLieRing instLieAlgebra incl proj	—	—
bracket 📖	mathematical	—	Bracket.bracket L ofTwoCocycle LieRingModule.toBracket LieAlgebra.instLieRingL LieRing.toAddCommGroup lieRingSelfModule DFunLike.coe LieEquiv LieAlgebra.ofTwoCocycle LieAlgebra.toModule LieAlgebra.instLieRingOfTwoCocycle LieAlgebra.instOfTwoCocycle LieAlgebra.instL EquivLike.toFunLike LieEquiv.instEquivLike ofAlg LieEquiv.symm	—	smulCommClass_self LinearMap.instSMulCommClass
d₁₂_oneCochainOfTwoSplitting 📖	mathematical	L DFunLike.coe LieHom instLieRing instLieAlgebra LieHom.instFunLike proj LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.instLieRingL LieAlgebra.toModule LieAlgebra.instL LinearMap.instFunLike	LieModule.Cohomology.oneCochain LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain Submodule.addCommMonoid Submodule.module LieModule.Cohomology.d₁₂ ringModuleOf lieModuleOf oneCochainOfTwoSplitting AddSubgroupClass.sub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.addCommGroup Submodule.addSubgroupClass LieModule.Cohomology.twoCocycle twoCocycleOf	—	smulCommClass_self LinearMap.instSMulCommClass lieModuleOf Submodule.addSubgroupClass LinearMap.ext LieHom.mem_ker map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass sub_eq_zero AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass trivial_lie_zero instIsLieAbelianSubtypeLMemLieSubmoduleKerProj LieIdeal.coe_bracket_of_module lie_sub sub_lie sub_sub ringModuleOf_bracket_proj LieEquiv.apply_symm_apply EmbeddingLike.apply_eq_iff_eq EquivLike.toEmbeddingLike SemilinearEquivClass.instSemilinearMapClass RingHomInvPair.ids LieEquiv.instLinearEquivClass lie_skew Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg proj_surjective
incl_apply_mem_ker 📖	mathematical	—	L LieIdeal instLieRing instLieAlgebra SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieHom.ker proj DFunLike.coe LieHom LieHom.instFunLike incl	—	Function.Exact.apply_apply_eq_zero LieHom.range_eq_ker_iff LieAlgebra.IsExtension.exact IsExtension
incl_injective 📖	mathematical	—	L DFunLike.coe LieHom instLieRing instLieAlgebra LieHom.instFunLike incl	—	LieHom.ker_eq_bot LieAlgebra.IsExtension.ker_eq_bot IsExtension
instIsLieAbelianSubtypeLMemLieSubmoduleKerProj 📖	mathematical	—	IsLieAbelian L LieSubmodule instLieRing LieRing.toAddCommGroup LieAlgebra.toModule instLieAlgebra lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker proj LieRingModule.toBracket LieIdeal.lieRing LieIdeal.lieRingModule LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieAlgebra.instLieRingL AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass	—	lie_abelian_iff_equiv_lie_abelian
lieModuleOf 📖	mathematical	—	LieModule LieRing.toAddCommGroup LieAlgebra.toModule ringModuleOf	—	Function.Surjective.hasRightInverse proj_surjective ringModuleOf_bracket map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass RingHomInvPair.ids LieEquiv.instLinearEquivClass LieSubmodule.instAddSubgroupClass smul_lie LieSubmodule.instLieModule lieAlgebraSelfModule EquivLike.apply_eq_iff_eq sub_eq_zero sub_lie trivial_lie_zero AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instIsLieAbelianSubtypeLMemLieSubmoduleKerProj map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass sub_self lie_smul
lie_apply_proj_of_leftInverse_eq 📖	mathematical	L DFunLike.coe LieHom instLieRing instLieAlgebra LieHom.instFunLike proj LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.instLieRingL LieAlgebra.toModule LieAlgebra.instL LinearMap.instFunLike	Bracket.bracket LieSubmodule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker LieRingModule.toBracket AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem	—	LieSubmodule.instAddSubgroupClass sub_eq_zero sub_lie trivial_lie_zero AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instIsLieAbelianSubtypeLMemLieSubmoduleKerProj map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass Function.LeftInverse.eq sub_self
lie_incl_mem_ker 📖	mathematical	—	L LieIdeal instLieRing instLieAlgebra SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieHom.ker proj Bracket.bracket LieRingModule.toBracket LieAlgebra.instLieRingL DFunLike.coe LieHom LieHom.instFunLike incl	—	LieHom.mem_ker LieHom.map_lie proj_incl lie_zero
lie_toKer_apply 📖	mathematical	—	Bracket.bracket L LieRingModule.toBracket LieAlgebra.instLieRingL LieRing.toAddCommGroup lieRingSelfModule LieSubmodule instLieRing LieAlgebra.toModule instLieAlgebra SetLike.instMembership LieSubmodule.instSetLike LieHom.ker proj DFunLike.coe LieEquiv LieIdeal.lieRing LieIdeal.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike toKer LieHom LieHom.instFunLike incl	—	—
ofTwoCocycle_incl_apply 📖	mathematical	—	DFunLike.coe LieHom L ofTwoCocycle instLieRing instLieAlgebra LieHom.instFunLike incl LieRing.toAddCommGroup LieAlgebra.toModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smulCommClass_self LinearMap.instSMulCommClass
ofTwoCocycle_proj_apply 📖	mathematical	—	DFunLike.coe LieHom L ofTwoCocycle instLieRing instLieAlgebra LieHom.instFunLike proj LieAlgebra.ofTwoCocycle.carrier LieRing.toAddCommGroup LieAlgebra.toModule	—	smulCommClass_self LinearMap.instSMulCommClass
oneCochainOfTwoSplitting_apply 📖	mathematical	L DFunLike.coe LieHom instLieRing instLieAlgebra LieHom.instFunLike proj LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.instLieRingL LieAlgebra.toModule LieAlgebra.instL LinearMap.instFunLike	oneCochainOfTwoSplitting LieEquiv LieSubmodule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker LieIdeal.lieRing LieIdeal.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike LieEquiv.symm toKer SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
proj_incl 📖	mathematical	—	DFunLike.coe LieHom L instLieRing instLieAlgebra LieHom.instFunLike proj incl NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	LieHom.mem_ker incl_apply_mem_ker
proj_surjective 📖	mathematical	—	L DFunLike.coe LieHom instLieRing instLieAlgebra LieHom.instFunLike proj	—	LieHom.range_eq_top LieAlgebra.IsExtension.range_eq_top IsExtension
ringModuleOf_bracket 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup ringModuleOf DFunLike.coe LieEquiv L LieSubmodule instLieRing LieAlgebra.toModule instLieAlgebra lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker proj LieIdeal.lieRing LieIdeal.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike LieEquiv.symm toKer AddSubgroupClass.toAddCommGroup LieSubmodule.instLieRingModuleSubtypeMem LieHom LieHom.instFunLike	—	—
ringModuleOf_bracket_proj 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup ringModuleOf DFunLike.coe LieHom L instLieRing instLieAlgebra LieHom.instFunLike proj LieEquiv LieSubmodule LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker LieIdeal.lieRing LieIdeal.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike LieEquiv.symm toKer AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem	—	Function.Surjective.hasRightInverse proj_surjective LieSubmodule.instAddSubgroupClass LieAlgebra.IsExtension.exact IsExtension map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass sub_self ringModuleOf_bracket EmbeddingLike.apply_eq_iff_eq EquivLike.toEmbeddingLike sub_eq_zero sub_lie LieSubmodule.coe_bracket lie_toKer_apply AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass ZeroMemClass.coe_zero LieHom.coe_toLinearMap LieHom.map_lie trivial_lie_zero map_zero AddMonoidHomClass.toZeroHomClass
toKer_bracket 📖	mathematical	—	DFunLike.coe LieEquiv L LieSubmodule instLieRing LieRing.toAddCommGroup LieAlgebra.toModule instLieAlgebra lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieHom.ker proj LieIdeal.lieRing LieIdeal.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike toKer Bracket.bracket LieRingModule.toBracket ringModuleOf LieEquiv.symm AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem LieHom LieHom.instFunLike Function.Surjective.hasRightInverse proj_surjective	—	LieSubmodule.instAddSubgroupClass Function.Surjective.hasRightInverse proj_surjective LieEquiv.apply_symm_apply
twoCocycleOf_coe_coe 📖	mathematical	L DFunLike.coe LieHom instLieRing instLieAlgebra LieHom.instFunLike proj LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.instLieRingL LieAlgebra.toModule LieAlgebra.instL LinearMap.instFunLike	LinearMap.addCommMonoid LinearMap.module Submodule SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.addCommMonoid Submodule.module LieModule.Cohomology.twoCocycle ringModuleOf lieModuleOf twoCocycleOf LinearMap.compr₂ LieSubmodule lieRingSelfModule LieSubmodule.instSetLike LieHom.ker LieIdeal.lieRing LieIdeal.lieAlgebra LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra Algebra.id LinearEquiv.toLinearMap LieEquiv.toLinearEquiv LieEquiv.symm toKer	—	smulCommClass_self LinearMap.instSMulCommClass lieModuleOf

LieAlgebra.IsExtension

Definitions

Name	Category	Theorems
extension 📖	CompOp	5 math math: extension_incl, extension_L, extension_instLieRing, extension_instLieAlgebra, extension_proj
kerEquivRange 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact 📖	mathematical	—	LieHom.range LieIdeal.toLieSubalgebra LieHom.ker	—	—
extension_L 📖	mathematical	—	LieAlgebra.Extension.L extension	—	—
extension_incl 📖	mathematical	—	LieAlgebra.Extension.incl extension	—	—
extension_instLieAlgebra 📖	mathematical	—	LieAlgebra.Extension.instLieAlgebra extension	—	—
extension_instLieRing 📖	mathematical	—	LieAlgebra.Extension.instLieRing extension	—	—
extension_proj 📖	mathematical	—	LieAlgebra.Extension.proj extension	—	—
ker_eq_bot 📖	mathematical	—	LieHom.ker Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	—
range_eq_top 📖	mathematical	—	LieHom.range Top.top LieSubalgebra LieSubalgebra.instTop	—	—

LieAlgebra.LieEquiv

Definitions

Name	Category	Theorems
ofCoboundary 📖	CompOp	2 math math: ofCoboundary_toFun, ofCoboundary_invFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofCoboundary_invFun 📖	mathematical	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain Submodule.addCommMonoid Submodule.module LieModule.Cohomology.twoCocycle Submodule.add DFunLike.coe LieModule.Cohomology.oneCochain LinearMap.instFunLike LieModule.Cohomology.d₁₂	LieEquiv.invFun LieAlgebra.ofTwoCocycle LieAlgebra.instLieRingOfTwoCocycle LieAlgebra.instOfTwoCocycle ofCoboundary Equiv EquivLike.toFunLike Equiv.instEquivLike LieAlgebra.ofProd Equiv.symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self LinearMap.instSMulCommClass
ofCoboundary_toFun 📖	mathematical	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain Submodule.addCommMonoid Submodule.module LieModule.Cohomology.twoCocycle Submodule.add DFunLike.coe LieModule.Cohomology.oneCochain LinearMap.instFunLike LieModule.Cohomology.d₁₂	LieEquiv LieAlgebra.ofTwoCocycle LieAlgebra.instLieRingOfTwoCocycle LieAlgebra.instOfTwoCocycle EquivLike.toFunLike LieEquiv.instEquivLike ofCoboundary Equiv Equiv.instEquivLike LieAlgebra.ofProd Equiv.symm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	smulCommClass_self LinearMap.instSMulCommClass

LieAlgebra.ofTwoCocycle

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1 math math: LieAlgebra.Extension.ofTwoCocycle_proj_apply

LieHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_eq_ker_iff 📖	mathematical	—	range LieIdeal.toLieSubalgebra ker Function.Exact DFunLike.coe LieHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	LieSubalgebra.ext

---

← Back to Index