FreeAlgebra

📁 Source: Mathlib/Algebra/FreeAlgebra.lean

Statistics

Metric	Count
Definitions `Pre`, `hasAdd`, `hasCoeGenerator`, `hasCoeSemiring`, `hasMul`, `hasOne`, `hasSMul`, `hasZero`, `instInhabited`, `algebraMapInv`, `equivMonoidAlgebraFreeMonoid`, `instAdd`, `instAddCommMonoid`, `instAlgebra`, `instDistrib`, `instInhabited`, `instMonoidWithZero`, `instMul`, `instOne`, `instRing`, `instSMul`, `instSemiring`, `instZero`, `liftFun`, `ι`	25
Theorems `adjoin_eq_range_freeAlgebra_lift`, `adjoin_range_eq_range_freeAlgebra_lift`, `adjoin_range_ι`, `algebraMap_eq_one_iff`, `algebraMap_eq_zero_iff`, `algebraMap_inj`, `algebraMap_leftInverse`, `hom_ext`, `hom_ext_iff`, `induction`, `instIsDomain`, `instIsScalarTower`, `instNoZeroDivisors`, `instNontrivial`, `instSMulCommClass`, `liftAux_eq`, `lift_comp_ι`, `lift_symm_apply`, `lift_unique`, `lift_ι_apply`, `quot_mk_eq_ι`, `ι_comp_lift`, `ι_def`, `ι_inj`, `ι_injective`, `ι_ne_algebraMap`, `ι_ne_one`, `ι_ne_zero`	28
Total	53

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_eq_range_freeAlgebra_lift` 📖	mathematical	—	`adjoin` `AlgHom.range` `FreeAlgebra` `Set` `Set.instMembership` `FreeAlgebra.instSemiring` `FreeAlgebra.instAlgebra` `id` `DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAlgebra.lift`	—	`adjoin_range_eq_range_freeAlgebra_lift` `Subtype.range_coe`
`adjoin_range_eq_range_freeAlgebra_lift` 📖	mathematical	—	`adjoin` `Set.range` `AlgHom.range` `FreeAlgebra` `FreeAlgebra.instSemiring` `FreeAlgebra.instAlgebra` `id` `DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAlgebra.lift`	—	`AlgHom.map_adjoin` `FreeAlgebra.lift_ι_apply`

FreeAlgebra

Definitions

Name	Category	Theorems
`Pre` 📖	CompData	2 math math: `ι_def`, `quot_mk_eq_ι`
`algebraMapInv` 📖	CompOp	1 math math: `algebraMap_leftInverse`
`equivMonoidAlgebraFreeMonoid` 📖	CompOp	—
`instAdd` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	3 math math: `instFree`, `rank_eq`, `Module.Basis.tensorAlgebra_repr_apply`
`instAlgebra` 📖	CompOp	32 math math: `lift_comp_ι`, `TensorAlgebra.ι_def`, `instFree`, `star_algebraMap`, `TensorAlgebra.equivFreeAlgebra_symm_ι`, `liftAux_eq`, `TensorAlgebra.equivFreeAlgebra_ι_apply`, `lift_ι_apply`, `Algebra.FiniteType.iff_quotient_freeAlgebra`, `Algebra.adjoin_range_eq_range_freeAlgebra_lift`, `MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `toTensor_ι`, `Algebra.FiniteType.instFreeAlgebraOfFinite`, `AlgCat.free_obj`, `rank_eq`, `algebraMap_inj`, `ι_comp_lift`, `adjoin_range_ι`, `Algebra.FiniteType.iff_quotient_freeAlgebra'`, `lift_unique`, `Module.Basis.tensorAlgebra_repr_apply`, `lift_symm_apply`, `AlgCat.free_map`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `Algebra.adjoin_eq_range_freeAlgebra_lift`, `algebraMap_eq_one_iff`, `TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`, `hom_ext_iff`, `algebraMap_leftInverse`, `algebraMap_eq_zero_iff`, `AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure`
`instDistrib` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	—
`instMul` 📖	CompOp	1 math math: `instNoZeroDivisors`
`instOne` 📖	CompOp	1 math math: `algebraMap_eq_one_iff`
`instRing` 📖	CompOp	3 math math: `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `AlgCat.free_obj`, `AlgCat.free_map`
`instSMul` 📖	CompOp	2 math math: `instSMulCommClass`, `instIsScalarTower`
`instSemiring` 📖	CompOp	35 math math: `lift_comp_ι`, `TensorAlgebra.ι_def`, `instFree`, `star_algebraMap`, `instIsDomain`, `TensorAlgebra.equivFreeAlgebra_symm_ι`, `liftAux_eq`, `TensorAlgebra.equivFreeAlgebra_ι_apply`, `lift_ι_apply`, `star_ι`, `Algebra.FiniteType.iff_quotient_freeAlgebra`, `Algebra.adjoin_range_eq_range_freeAlgebra_lift`, `MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `toTensor_ι`, `Algebra.FiniteType.instFreeAlgebraOfFinite`, `rank_eq`, `algebraMap_inj`, `ι_comp_lift`, `adjoin_range_ι`, `Algebra.FiniteType.iff_quotient_freeAlgebra'`, `lift_unique`, `Module.Basis.tensorAlgebra_repr_apply`, `lift_symm_apply`, `AlgCat.free_map`, `charZero`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `charP`, `Algebra.adjoin_eq_range_freeAlgebra_lift`, `algebraMap_eq_one_iff`, `TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`, `hom_ext_iff`, `algebraMap_leftInverse`, `algebraMap_eq_zero_iff`, `AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure`
`instZero` 📖	CompOp	2 math math: `instNoZeroDivisors`, `algebraMap_eq_zero_iff`
`liftFun` 📖	CompOp	—
`ι` 📖	CompOp	19 math math: `lift_comp_ι`, `ι_inj`, `TensorAlgebra.ι_def`, `TensorAlgebra.equivFreeAlgebra_symm_ι`, `ι_injective`, `TensorAlgebra.equivFreeAlgebra_ι_apply`, `lift_ι_apply`, `star_ι`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `toTensor_ι`, `ι_comp_lift`, `adjoin_range_ι`, `lift_unique`, `lift_symm_apply`, `AlgCat.free_map`, `ι_def`, `quot_mk_eq_ι`, `TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`, `hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_range_ι` 📖	mathematical	—	`Algebra.adjoin` `FreeAlgebra` `instSemiring` `instAlgebra` `Algebra.id` `Set.range` `ι` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`top_unique` `induction` `Subalgebra.algebraMap_mem` `Algebra.subset_adjoin` `Set.mem_range_self` `Subalgebra.mul_mem` `Subalgebra.add_mem`
`algebraMap_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`map_eq_one_iff` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_leftInverse`
`algebraMap_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_leftInverse`
`algebraMap_inj` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	`algebraMap_leftInverse`
`algebraMap_leftInverse` 📖	mathematical	—	`FreeAlgebra` `DFunLike.coe` `AlgHom` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `algebraMapInv` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`AlgHom.commutes`
`hom_ext` 📖	—	`FreeAlgebra` `DFunLike.coe` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `ι`	—	—	`Equiv.injective` `lift_symm_apply`
`hom_ext_iff` 📖	mathematical	—	`FreeAlgebra` `DFunLike.coe` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `ι`	—	`hom_ext`
`induction` 📖	—	`DFunLike.coe` `RingHom` `FreeAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `ι` `instMul` `instAdd`	—	—	`RingHom.map_one` `RingHom.map_zero` `hom_ext` `lift_ι_apply` `Subtype.prop`
`instIsDomain` 📖	mathematical	—	`IsDomain` `FreeAlgebra` `CommRing.toCommSemiring` `instSemiring`	—	`NoZeroDivisors.to_isDomain` `instNontrivial` `IsDomain.toNontrivial` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `FreeAlgebra` `instSMul`	—	`smul_assoc` `IsScalarTower.left` `Algebra.algebraMap_eq_smul_one` `smul_one_mul` `IsScalarTower.right`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `FreeAlgebra` `instMul` `instZero`	—	`MulEquiv.noZeroDivisors` `MonoidAlgebra.instNoZeroDivisorsOfUniqueProds` `TwoUniqueProds.toUniqueProds` `FreeMonoid.instTwoUniqueProds`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `FreeAlgebra`	—	`Function.Surjective.nontrivial` `MonoidAlgebra.nontrivial` `AlgEquiv.surjective`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `FreeAlgebra` `instSMul`	—	`SMulCommClass.smul_comm` `smulCommClass_self`
`liftAux_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `FreeAlgebra` `instSemiring` `instAlgebra` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`lift.eq_1`
`lift_comp_ι` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `FreeAlgebra` `instSemiring` `instAlgebra` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `AlgHom.funLike` `ι`	—	`lift_symm_apply` `Equiv.apply_symm_apply`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `FreeAlgebra` `instSemiring` `instAlgebra` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `AlgHom.funLike` `ι`	—	`lift.eq_1`
`lift_unique` 📖	mathematical	—	`FreeAlgebra` `DFunLike.coe` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `ι` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`Equiv.symm_apply_eq` `lift.eq_1`
`lift_ι_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `FreeAlgebra` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `ι`	—	`ι_def` `lift.eq_1`
`quot_mk_eq_ι` 📖	mathematical	—	`Pre` `Rel` `Pre.of` `ι`	—	`ι_def`
`ι_comp_lift` 📖	mathematical	—	`FreeAlgebra` `DFunLike.coe` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `ι`	—	`ι_def` `lift.eq_1`
`ι_def` 📖	mathematical	—	`ι` `Pre` `Rel` `Pre.of`	—	—
`ι_inj` 📖	mathematical	—	`ι`	—	`ι_injective`
`ι_injective` 📖	mathematical	—	`FreeAlgebra` `ι`	—	`by_contradiction` `lift_ι_apply` `one_ne_zero` `NeZero.one`
`ι_ne_algebraMap` 📖	—	—	—	—	`lift_ι_apply` `zero_ne_one` `NeZero.one` `Algebra.algebraMap_self_apply` `AlgHom.commutes`
`ι_ne_one` 📖	—	—	—	—	`ι_ne_algebraMap`
`ι_ne_zero` 📖	—	—	—	—	`ι_ne_algebraMap`

FreeAlgebra.Pre

Definitions

Name	Category	Theorems
`hasAdd` 📖	CompOp	—
`hasCoeGenerator` 📖	CompOp	—
`hasCoeSemiring` 📖	CompOp	—
`hasMul` 📖	CompOp	—
`hasOne` 📖	CompOp	—
`hasSMul` 📖	CompOp	—
`hasZero` 📖	CompOp	—
`instInhabited` 📖	CompOp	—

---

← Back to Index