lift

📁 Source: MathlibTest/lift.lean

Statistics

Metric	Count
Definitions lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift	243
Theorems lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift, lift	20
Total	263

Abelianization

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: lift_unique, coe_lift_symm, lift_apply_of, lift_of_comp, lift_of, FreeAbelianGroup.liftAddEquiv_apply_apply, lift_symm_apply, equivOfComm_symm_apply

AddCommGroup.DirectLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_of', lift_comp_of, lift_of, lift_injective

AddCommGrpCat.HasLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: productLimitCone_isLimit_lift, lift_hom_apply

AddCommGrpCat.image

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_fac

AddCon

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: lift_comp_mk', lift_mk', lift_range, lift_surjective_of_surjective, map_apply, lift_apply_mk', lift_unique, lift_coe

AddMagma.FreeAddSemigroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_symm_apply, lift_comp_of, lift_comp_of', lift_of

AddMonoid.Coprod

Definitions

Name	Category	Theorems
lift 📖	CompOp	13 math math: lift_comp_inr, lift_inr_inl, mrange_lift, lift_comp_inl, lift_apply_inl, lift_apply_inr, comp_lift, lift_inl_inr, lift_comp_swap, range_lift, lift_apply_mk, lift_swap, lift_unique

AddMonoidAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: lift_apply', lift_mapRangeRingHom_algebraMap, lift_apply, lift_single, lift_symm_apply, lift_of, lift_unique', lift_of', lift_def

AddSubmonoid.LocalizationMap

Definitions

Name	Category	Theorems
lift 📖	CompOp	22 math math: addEquivOfLocalizations_symm_apply, lift_surjective_iff, lift_injective_iff, lift_eq_iff, lift_of_comp, lift_mk'_spec, lift_apply, lift_eq, lift_spec_add, AddLocalization.addEquivOfQuotient_apply, lift_comp, lift_comp_lift, lift_comp_lift_eq, lift_spec, lift_id, lift_add_right, lift_localizationMap_mk', lift_mk', lift_unique, lift_left_inverse, lift_add_left, addEquivOfLocalizations_apply

AddSubmonoid.LocalizationMap.AwayMap

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp, lift_eq

AdicCompletion

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: IsAdicComplete.of_lift, IsAdicComplete.of_comp_lift, IsAdicComplete.StrictMono.of_comp_lift, IsAdicComplete.StrictMono.of_lift, eval_lift_apply, eval_lift

AdjoinRoot

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: coe_liftHom, lift_comp_of, lift_mk, toRingHom_liftAlgHom, coe_liftAlgHom, lift_of, lift_root

Algebra.FormallySmooth

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: comp_lift, mk_lift

Algebra.GrothendieckAddGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_apply, lift_symm_apply

Algebra.GrothendieckGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_symm_apply, lift_apply

Algebra.TensorProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	17 math math: lift_comp_includeLeft, MvPolynomial.universalFactorizationMap_comp_map, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, Ideal.Fiber.lift_residueField_surjective, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, CommAlgCat.lift_unop_hom, lmul'_comp_map, lift_comp_includeRight, liftEquiv_apply, Algebra.pushoutDesc_apply, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, CommRingCat.coproductCoconeIsColimit_desc, lift_tmul, lift_comp_includeRight', AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective, lift_includeLeft_includeRight

AlgebraicGeometry.IsClosedImmersion

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_fac_assoc, lift_fac, isIso_lift

AlgebraicGeometry.IsOpenImmersion

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: instLift, comp_lift_assoc, isPullback_lift_id, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, lift_fac_assoc, lift_uniq, comp_lift, lift_fac, lift_app

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_fac, lift_fac_assoc, lift_range, lift_uniq

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: isoOfRangeEq_hom, lift_fac_assoc, isoOfRangeEq_inv, lift_fac, lift_uniq

ArchimedeanClass

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_mk

Booleanisation

Definitions

Name	Category	Theorems
lift 📖	CompOp	19 math math: comp_sdiff_comp, not_comp_lt_lift, lift_sup_comp, lift_sdiff_lift, lift_le_lift, lift_inf_comp, compl_comp, compl_lift, lift_sdiff_comp, not_comp_le_lift, lift_lt_lift, comp_sdiff_lift, lift_lt_comp, comp_sup_lift, lift_inf_lift, comp_inf_lift, lift_sup_lift, lift_le_comp, lift_bot

BoundedOrder

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Bundle.Pullback

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: Trivialization.pullback_source, lift_mk, Pullback.continuous_lift, pullbackTopology_def, Trivialization.pullback_apply, lift_snd, lift_proj

Cardinal

Definitions

Name	Category	Theorems
lift 📖	CompOp	318 math math: mk_le_of_module, Ordinal.lift_card_iSup_le_sum_card, ofENat_le_lift, Algebra.lift_cardinalMk_adjoin_le, lift_ofENat, lift_le_ofENat, SymmetricAlgebra.rank_eq, Ordinal.cof_iSup_le_lift, Module.lift_rank_of_isLocalizedModule_of_free, Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic, Module.Basis.mk_eq_rank, ofENat_lt_lift, lift_mk_le, lift_univ, ofENat_eq_lift, lift_rank_mul_lift_rank, Algebraic.cardinalMk_lift_le_mul, LinearIndependent.cardinal_lift_le_rank, Matrix.lift_cRank_submatrix_le, lift_rank_map_le, mk_preimage_of_subset_range_lift, Module.Basis.mk_eq_rank', IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt, mk_preimage_equiv_lift, IsLocalization.lift_cardinalMk, IntermediateField.lift_insepDegree_bot', rank_finsupp, ofNat_le_lift_iff, lift_le_aleph0, rank_finsupp_self, mk_eq_mk_of_basis, LinearMap.lift_rank_le_of_surjective, lift_eq_aleph_one, Module.Basis.dual_rank_eq, Matroid.cRk_comap_lift, lift_zero, LinearMap.le_rank_iff_exists_linearIndependent, Module.rank_baseChange, LinearMap.lift_rank_comp_le_right, mk_finsupp_lift_of_infinite, ofNat_lt_lift_iff, Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_surjective, lift_rank_range_of_injective, Matrix.lift_cRank_submatrix, lift_lift, lift_lt_ofNat_iff, AddMonoidAlgebra.cardinalMk_lift_of_fintype, lift_iInf, rank_matrix_module, Equiv.lift_cardinal_eq, lift_succ, lift_prod, mk_subset_ge_of_subset_image_lift, Computability.Encoding.card_le_card_list, prod_const, Ordinal.card_sInf_range_compl_le_lift, mk_preimage_down, Subfield.lift_relrank_map_map, Ordinal.cof_lsub_le_lift, FirstOrder.Language.card_eq_card_functions_add_card_relations, liftInitialSeg_toFun, LinearEquiv.lift_rank_eq, mk_iUnion_le_sum_mk_lift, mk_image_embedding_lift, Ordinal.cof_blsub_le_lift, lift_monotone, lift_iSup, lift_trdeg_le_of_injective, lift_sSup, lift_rank_le_of_surjective_injective, mk_biUnion_le_lift, mk_range_eq_of_injective, toENat_lift, MonoidAlgebra.cardinalMk_lift_of_infinite, lift_mk_shrink', continuum_lt_lift, WType.cardinalMk_le_max_aleph0_of_finite', lift_le_nat_iff, lift_lt_ofENat, mk_image_eq_of_injOn_lift, aleph1_le_lift, lt_univ, Module.rank_linearMap, WType.cardinalMk_eq_sum_lift, FreeAlgebra.cardinalMk_eq_lift, Module.lift_rank_bot_le_lift_rank_of_isScalarTower, mk_embedding_eq_zero_iff_lift_lt, lift_power_sum, mk_image_eq_lift, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, TensorAlgebra.rank_eq, lift_id', lift_sum, lift_ord, lift_rank_lt_rank_dual', IsTranscendenceBasis.lift_cardinalMk_eq_trdeg, Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_le, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank, lift_lt_univ', lift_rank_add_lift_rank_le_rank_prod, lift_preBeth, Matrix.cRank_diagonal, lift_rank_eq_of_equiv_equiv, LinearMap.lift_rank_le_of_injective, Ordinal.card_iSup_Iio_le_card_mul_iSup, mk_iUnion_eq_sum_mk_lift, IsLocalizedModule.lift_rank_eq, LinearMap.lift_rank_eq_of_surjective, AddMonoidAlgebra.cardinalMk_lift_of_infinite, IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, lift_mk_shrink'', lift_mk_fin, zero_eq_lift_iff, lift_le_ofNat_iff, lift_trdeg_le_of_surjective, lift_eq_aleph0, Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, lift_umax_eq, rank_tensorProduct, nat_eq_lift_iff, lift_mk_shrink, aleph1_lt_lift, IntermediateField.lift_relrank_comap, AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute, rank_ulift, Algebra.IsAlgebraic.lift_cardinalMk_le_max, iSupIndep.subtype_ne_bot_le_rank, Algebra.lift_rank_eq_of_equiv_equiv, lift_mk_eq', lift_mk_eq, lift_iSup_le_sum, Complex.rank_real_complex', ZFSet.lift_card_iUnion_le_sum_card, lift_eq_aleph1, sum_le_lift_mk_mul_iSup, toNat_lift, mk_uLift, ZFSet.lift_card_range_le, lift_lt, mk_range_inr, Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial, lift_rank_lt_rank_dual, aleph0_le_lift, le_lift_iff, Ordinal.lift_cof, OreLocalization.cardinalMk_le_max, OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute, lift_eq_ofNat_iff, Matrix.cRank_one, Matrix.lift_cRank_reindex, Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, nat_lt_lift_iff, mk_congr_lift, IntermediateField.lift_sepDegree_bot', FreeAlgebra.rank_eq, Algebra.lift_rank_le_of_injective_injective, Ordinal.mk_Iio_ordinal, lift_two, lift_lt_univ, mk_arrow, lt_lift_iff, rank_matrix_module', lift_umax, lift_inj, aleph_one_le_lift, IsTranscendenceBasis.lift_cardinalMk_eq, lift_natCast, sum_le_iSup_lift, Subfield.lift_relrank_comap, mk_range_eq_lift, mk_iUnion_le_lift, FirstOrder.Language.empty.nonempty_equiv_iff, lift_le_one_iff, lift_le_aleph1, AddMonoidAlgebra.cardinalMk_lift_of_infinite', mk_range_inl, FirstOrder.Language.Theory.exists_large_model_of_infinite_model, LinearMap.lift_rank_range_add_rank_ker, rank_matrix', RelIso.cof_eq_lift, Module.dual_rank_eq, MonoidAlgebra.cardinalMk_lift_of_fintype, mk_finsupp_lift_of_fintype, lift_uzero, IsRegular.lift, lift_aleph, LinearEquiv.nonempty_equiv_iff_lift_rank_eq, IsBaseChange.lift_rank_eq, continuum_le_lift, small_iff_lift_mk_lt_univ, prod_eq_of_fintype, rank_matrix, lift_two_power, sum_le_lift_mk_mul_iSup_lift, IsAlgClosed.cardinal_le_max_transcendence_basis, lift_trdeg_add_eq, IsLocalization.lift_cardinalMk_le, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, Ordinal.lift_card_sInf_compl_le, Matroid.cRk_map_image_lift, one_lt_lift_iff, Algebra.IsAlgebraic.lift_rank_of_isFractionRing, lift_mk_le_lift_mk_of_injective, lift_ofNat, lift_le_sum, lift_le_aleph_one, cardinalMk_algHom_le_rank, mk_preimage_of_injective_of_subset_range_lift, lift_mk_le', lift_sInf, one_eq_lift_iff, MvPolynomial.cardinalMk_le_max_lift, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_le, mk_sum, lift_mul, FreeAlgebra.cardinalMk_le_max_lift, aleph1_eq_lift, IntermediateField.lift_cardinalMk_adjoin_le, aleph0_lt_lift, lift_lt_aleph0, aleph0_eq_lift, Subfield.lift_rank_comap, MonoidAlgebra.cardinalMk_lift_of_infinite', out_lift_equiv, lift_beth, FirstOrder.Language.card_withConstants, IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, lift_aleph0, IsFractionRing.lift_cardinalMk, lift_one, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf, Field.lift_sepDegree_eq_of_equiv, ZFSet.cardinalMk_coe_sort, ofNat_eq_lift_iff, Field.lift_rank_mul_lift_sepDegree_of_isSeparable, Field.lift_insepDegree_eq_of_equiv, infinite_basis_le_maximal_linearIndependent', Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, AlgebraicIndependent.lift_cardinalMk_le_trdeg, lift_mk_le_lift_mk_of_surjective, aleph_one_eq_lift, AlgEquiv.lift_trdeg_eq, mk_surjective_eq_zero_iff_lift, one_le_lift_iff, FirstOrder.Language.card_functions_sum, lift_lt_continuum, lift_iSup_le_iff, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_surjective, lift_rank_range_le, lift_trdeg_add_le, FirstOrder.Language.card_sum, lift_le_continuum, mk_image_le_lift, LinearEquiv.lift_rank_map_eq, lift_rank_le_of_injective_injective, Ordinal.cof_bsup_le_lift, MvPolynomial.cardinalMk_eq_lift, nat_le_lift_iff, toNat_lift_add_lift, lift_lt_aleph1, lift_rank_le_of_injective_injectiveₛ, rank_fun_eq_lift_mul, IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, lift_eq_ofENat, MvRatFunc.rank_eq_max_lift, lift_strictMono, IntermediateField.lift_rank_comap, lift_add, IntermediateField.lift_relrank_map_map, Ordinal.lift_card, lift_power, aleph_one_lt_lift, IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, lift_eq_nat_iff, mk_preimage_of_injective_lift, Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf, MvPolynomial.trdeg_of_isDomain, lt_univ', mk_finsupp_lift_of_infinite', lift_eq_zero, Algebra.lift_rank_le_of_surjective_injective, rank_prod, isRegular_lift_iff, zero_lt_lift_iff, lift_eq_one, Algebraic.cardinalMk_lift_of_infinite, sum_const, AddOreLocalization.cardinalMk_le_max, Module.rank_linearMap_self, lift_continuum, FirstOrder.Language.card_relations_sum, rank_mvPolynomial_mvPolynomial, HahnSeries.cardSupp_hsum_le, mk_psum, MvPolynomial.rank_eq_lift, MvPolynomial.cardinalMk_eq_max_lift, lift_min, mk_range_le_lift, hasCardinalLT_lift_iff, lift_id, lift_lt_nat_iff, FirstOrder.Language.Substructure.lift_card_closure_le, lift_injective, FirstOrder.Language.card_le_of_model_distinctConstantsTheory, FreeAlgebra.cardinalMk_eq_max_lift, lift_max, mk_prod, lift_preAleph, lift_lt_aleph_one, LinearMap.lift_rank_comp_le, IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors, lift_le, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, FirstOrder.Language.empty.nonempty_embedding_iff

Cardinal.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Cardinal.IsRegular	Cardinal.lift	—	Cardinal.lift_ord Ordinal.lift_cof Cardinal.lift_le

CategoryTheory.Bicategory.LeftLift

Definitions

Name	Category	Theorems
lift 📖	CompOp	17 math math: whiskering_map, w_assoc, CategoryTheory.Bicategory.lanLiftUnit_desc_assoc, IsKan.fac_assoc, CategoryTheory.Bicategory.LanLift.existsUnique, whisker_unit, whiskerHom_right, ofIdComp_right, IsKan.fac, whisker_lift, ofIdComp_hom, whiskerOfIdCompIsoSelf_hom_right, CategoryTheory.Bicategory.lanLiftLeftLift_lift, CategoryTheory.Bicategory.lanLiftUnit_desc, whiskerIdCancel_right, whiskerOfIdCompIsoSelf_inv_right, w

CategoryTheory.Bicategory.RightLift

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

CategoryTheory.CartesianMonoidalCategory

Definitions

Name	Category	Theorems
lift 📖	CompOp	82 math math: CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.GrpObj.lift_inv_right_eq, CategoryTheory.GrpObj.lift_inv_comp_left_assoc, lift_leftUnitor_hom_assoc, CategoryTheory.GrpObj.left_inv_assoc, CategoryTheory.MonObj.lift_comp_one_right, CategoryTheory.Functor.Monoidal.lift_μ_assoc, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, CategoryTheory.GrpObj.lift_inv_comp_right, CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom, CategoryTheory.comul_eq_lift, CategoryTheory.Grp.lift_hom, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.MonObj.lift_comp_one_right_assoc, lift_braiding_hom, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, comp_lift, CategoryTheory.GrpObj.lift_comp_inv_right_assoc, lift_lift_associator_inv_assoc, lift_lift_associator_inv, CategoryTheory.Mon.lift_hom, lift_apply, lift_braiding_inv, CommAlgCat.lift_unop_hom, lift_rightUnitor_hom_assoc, CategoryTheory.Hom.mul_def, CategoryTheory.MonObj.lift_comp_one_left, CategoryTheory.Functor.OplaxMonoidal.lift_δ, CategoryTheory.MonObj.instIsMonHomLift, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, CategoryTheory.forgetAdjToOver_unit_app, lift_lift_associator_hom, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv, CategoryTheory.GrpObj.lift_inv_left_eq, lift_whiskerLeft, lift_fst_snd, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, lift_braiding_hom_assoc, lift_snd, lift_snd_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, CategoryTheory.GrpObj.eq_lift_inv_right, CategoryTheory.GrpObj.left_inv, comp_lift_assoc, CategoryTheory.ChosenPullbacksAlong.Over.lift_left, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc, lift_whiskerRight_assoc, lift_comp_fst_snd, lift_whiskerRight, mono_lift_of_mono_right, CategoryTheory.GrpObj.mulRight_hom, CategoryTheory.GrpObj.lift_comp_inv_left_assoc, lift_fst, lift_leftUnitor_hom, CategoryTheory.GrpObj.mulRight_inv, CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv, lift_fst_assoc, lift_lift_associator_hom_assoc, mono_lift_of_mono_left, CategoryTheory.GrpObj.right_inv, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.GrpObj.eq_lift_inv_left, lift_snd_comp_fst_comp_assoc, lift_map, CategoryTheory.MonObj.lift_comp_one_left_assoc, lift_map_assoc, lift_fst_comp_snd_comp, CategoryTheory.Over.lift_left, fullSubcategory_tensorProductIsBinaryProduct_lift_hom, lift_snd_comp_fst_comp, CategoryTheory.GrpObj.lift_comp_inv_right, CategoryTheory.Functor.Monoidal.lift_μ, CategoryTheory.Functor.OplaxMonoidal.lift_δ_assoc, lift_snd_fst, CategoryTheory.Functor.EssImageSubcategory.lift_def, lift_rightUnitor_hom, CategoryTheory.GrpObj.right_inv_assoc, homEquivToProd_symm_apply, lift_whiskerLeft_assoc, CategoryTheory.GrpObj.lift_inv_comp_right_assoc, lift_braiding_inv_assoc

CategoryTheory.Cat.FreeRefl

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: CategoryTheory.ReflQuiv.adj.homEquiv_symm_apply, lift_map, lift_spec, CategoryTheory.ReflQuiv.adj_counit_app, lift_obj

CategoryTheory.ChosenPullbacksAlong

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_snd, lift_fst, lift_snd_assoc, Over.lift_left, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, lift_fst_assoc

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: fac_right_assoc, fac_right, fac_left_assoc, fac_left

CategoryTheory.CostructuredArrow.IsUniversal

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: fac, fac_assoc, hom_desc

CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: fac

CategoryTheory.Free

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_linear, lift_obj, lift_additive, lift_map_single, lift_map

CategoryTheory.FreeBicategory

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_mapId, lift_mapComp, lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj

CategoryTheory.FreeGroupoid

Definitions

Name	Category	Theorems
lift 📖	CompOp	12 math math: map_comp_lift, lift_comp, lift_map_homMk, mapCompLift_inv_app, lift_obj_mk, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, CategoryTheory.Grpd.freeForgetAdjunction_counit_app, lift_id_comp_of, functorEquiv_symm_apply, lift_unique, lift_spec, mapCompLift_hom_app

CategoryTheory.Functor.Final

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: extendCocone_obj_ι_app, colimit_cocone_comp_aux, extendCocone_map_hom

CategoryTheory.Functor.Initial

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: extendCone_map_hom, limit_cone_comp_aux, extendCone_obj_π_app

CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: fac_assoc, lift_map, lift_map_assoc, fac

CategoryTheory.Functor.WellOrderInductionData

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: map_lift, Extension.map_limit

CategoryTheory.Functor.relativelyRepresentable

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_fst, lift_snd, lift_snd_assoc, lift_fst_assoc

CategoryTheory.FunctorToTypes.prod

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_fst, CategoryTheory.FunctorToTypes.binaryProductLimit_lift, lift_app, lift_snd

CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: fac, fac', fac'_assoc

CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: map_lift, lift_f'

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: comm, hlift, uniq, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux, comm_assoc, lift_self, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W

CategoryTheory.IsKernelPair

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_snd_assoc, lift_snd, lift_fst_assoc, lift_fst

CategoryTheory.IsPullback

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: CategoryTheory.Functor.PullbackObjObj.mapArrowRight_right, of_bot', lift_snd_assoc, of_right', lift_snd, lift_fst, CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_right, lift_fst_assoc

CategoryTheory.IsRegularMono

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: fac, uniq, fac_assoc

CategoryTheory.Limits.Fan.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: fac_assoc, CategoryTheory.Limits.Multifork.toPiFork_π_app_one, fac, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, CategoryTheory.Limits.Multifork.pi_condition_assoc, CategoryTheory.Limits.Multifork.toPiFork_π_app_zero, CategoryTheory.Limits.Multifork.pi_condition

CategoryTheory.Limits.Fork.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_ι'_assoc, lift_ι'

CategoryTheory.Limits.IsImage

Definitions

Name	Category	Theorems
lift 📖	CompOp	14 math math: lift_ι_assoc, lift_fac, ofArrowIso_lift, ofIsoI_lift, isoExt_hom, CategoryTheory.Limits.image.isImage_lift, self_lift, lift_fac_assoc, lift_ι, fac_lift, isoExt_inv, copy_lift, CategoryTheory.PreservesImage.iso_inv, fac_lift_assoc

CategoryTheory.Limits.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	124 math math: ofConeEquiv_symm_apply_desc, CategoryTheory.Limits.inr_of_isLimit, CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f, CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift, CategoryTheory.Limits.kernelBiprodSndIso_hom, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ, CategoryTheory.Limits.BinaryBicone.ofLimitCone_inl, CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom, CategoryTheory.Comma.coneOfPreserves_π_app_right, CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc, CategoryTheory.Limits.kernelBiprodFstIso_hom, CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc, CompHausLike.pullback.isLimit_lift, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift, CategoryTheory.Limits.kernelBiproductπIso_hom, CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe, CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a, CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift, lift_comp_conePointUniqueUpToIso_hom_assoc, CategoryTheory.Mon.limitConeIsLimit_lift_hom, nonempty_isLimit_iff_isIso_lift, liftConeMorphism_hom, lift_comp_conePointsIsoOfNatIso_inv, CategoryTheory.Limits.Types.binaryProductFunctor_obj_map, Profinite.isIso_indexCone_lift, lift_comp_conePointsIsoOfNatIso_hom, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, CategoryTheory.Limits.PullbackCone.combine_π_app, CategoryTheory.Limits.limit.isLimit_lift, AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift, pullbackConeEquivBinaryFanFunctor_lift_left, CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom, ofIsoLimit_lift, CategoryTheory.Limits.BinaryBicone.ofLimitCone_inr, AddCommGrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc, CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift, CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc, CategoryTheory.Limits.inl_of_isLimit, GrpCat.binaryProductLimitCone_isLimit_lift, hom_lift, CategoryTheory.Limits.coneOfConeCurry_π_app, CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc, AddGrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift, ofConeEquiv_apply_desc, CategoryTheory.Limits.BinaryFan.rightUnitor_inv, CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift, CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe, lift_comp_conePointUniqueUpToIso_hom, CategoryTheory.Limits.isLimitConeUnopOfCocone_lift, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc, CategoryTheory.Limits.Types.binaryProductFunctor_map_app, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.FunctorToTypes.binaryProductLimit_lift, uniq, CategoryTheory.Limits.Bicone.ofLimitCone_ι, CategoryTheory.Limits.isLimitConeOfAdj_lift, CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift, CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift, CategoryTheory.Limits.mkFanLimit_lift, lift_comp_conePointUniqueUpToIso_inv_assoc, CategoryTheory.ShortComplex.LeftHomologyData.wπ, CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift, CategoryTheory.Limits.isKernelCompMono_lift, CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift, lift_comp_conePointUniqueUpToIso_inv, CategoryTheory.Limits.coneOfConeUncurry_π_app, CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc, CategoryTheory.Limits.limitConeOfUnique_isLimit_lift, mkConeMorphism_lift, fac_assoc, CategoryTheory.Limits.BinaryFan.assoc_snd, CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift, CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift, CategoryTheory.Comma.coneOfPreserves_pt_hom, CategoryTheory.Limits.Fan.IsLimit.lift_proj, CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc, CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc, CategoryTheory.Limits.PullbackCone.combine_pt_map, CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc, CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, CategoryTheory.Limits.limit.pre_eq, conePointsIsoOfEquivalence_hom, CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc, conePointsIsoOfEquivalence_inv, lift_comp_conePointsIsoOfNatIso_inv_assoc, CategoryTheory.Limits.Fork.IsLimit.mk_lift, ModuleCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Comonad.beckEqualizer_lift, CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc, lift_comp_conePointsIsoOfNatIso_hom_assoc, assoc_lift, lift_self, CategoryTheory.Limits.combineCones_pt_map, CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift, CategoryTheory.Limits.BinaryFan.leftUnitor_inv, CategoryTheory.Limits.Multifork.IsLimit.mk_lift, CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc, CommGrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction, CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift, binaryFanSwap_lift, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc, CategoryTheory.preserves_lift_mapCone, CategoryTheory.Limits.BinaryFan.assocInv_fst, CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f, ModuleCat.HasLimit.productLimitCone_isLimit_lift, CategoryTheory.Limits.Types.binaryProductLimit_lift, Profinite.isIso_asLimitCone_lift, fac, CategoryTheory.Limits.combineCones_π_app_app, CategoryTheory.Comma.coneOfPreserves_π_app_left, CategoryTheory.Limits.Bicone.ι_of_isLimit

CategoryTheory.Limits.Multiequalizer

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_ι_assoc, CategoryTheory.GrothendieckTopology.diagram_map, CategoryTheory.GrothendieckTopology.diagramPullback_app, CategoryTheory.GrothendieckTopology.diagramNatTrans_app, lift_ι

CategoryTheory.Limits.Multifork.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: fac_assoc, fac

CategoryTheory.Limits.Pi

Definitions

Name	Category	Theorems
lift 📖	CompOp	33 math math: CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, CategoryTheory.isCoseparator_iff_mono, lift_π_assoc, CategoryTheory.Limits.Types.pi_lift_π_apply', CategoryTheory.evaluationRightAdjoint_obj_map, CategoryTheory.Equalizer.firstObjEqFamily_inv, CategoryTheory.evaluationAdjunctionLeft_unit_app_app, CategoryTheory.evaluationRightAdjoint_map_app, CategoryTheory.Limits.biproduct.isoProduct_hom, CategoryTheory.Limits.instMonoLiftπ, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, lift_π, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map, CategoryTheory.Limits.piPiIso_hom, CategoryTheory.Limits.FormalCoproduct.evalOp_map_app, CategoryTheory.Pretriangulated.productTriangle.lift_hom₁, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, CategoryTheory.Limits.map_lift_piComparison_assoc, CategoryTheory.Pretriangulated.productTriangle.lift_hom₃, CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app, CategoryTheory.Limits.piPiIso_inv, CategoryTheory.Limits.FormalCoproduct.evalOp_obj_map, CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift, CategoryTheory.Limits.Types.pi_lift_π_apply, CategoryTheory.Pretriangulated.productTriangle.lift_hom₂, CategoryTheory.Limits.FormalCoproduct.mapPower_φ, CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift, CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_hom_app, CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_inv_app_app, CategoryTheory.Limits.map_lift_piComparison, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map

CategoryTheory.Limits.PullbackCone.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_fst, lift_snd, lift_fst_assoc, lift_snd_assoc

CategoryTheory.Limits.Types.Image

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_fac

CategoryTheory.Limits.Wedge.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_ι, lift_ι_assoc

CategoryTheory.Limits.WidePullback

Definitions

Name	Category	Theorems
lift 📖	CompOp	11 math math: CategoryTheory.Arrow.mapCechNerve_app, eq_lift_of_comp_eq, lift_base_assoc, lift_base, hom_eq_lift, CategoryTheory.Arrow.cechNerve_map, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, lift_π_assoc, CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app, lift_π

CategoryTheory.Limits.WidePullbackCone.IsLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_base, lift_π_assoc, lift_base_assoc, lift_π

CategoryTheory.Limits.biprod

Definitions

Name	Category	Theorems
lift 📖	CompOp	34 math math: lift_eq, uniqueUpToIso_hom, HomologicalComplex.biprod_lift_fst_f_assoc, lift_snd, HomologicalComplex.biprod_lift_fst_f, isoProd_inv, symmetry'_assoc, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, CategoryTheory.CommSq.shortComplex_f, symmetry', lift_mapBiprod, associator_hom, lift_fst, mono_lift_of_mono_right, HomologicalComplex.biprod_lift_snd_f, braiding_inv, lift_fst_assoc, map_lift_mapBiprod, conePointUniqueUpToIso_hom, CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition, CategoryTheory.Functor.mapBiprod_hom, add_eq_lift_desc_id, lift_snd_assoc, lift_desc_assoc, braiding_hom, CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition, CategoryTheory.CommSq.shortComplex'_f, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, add_eq_lift_id_desc, mono_lift_of_mono_left, HomologicalComplex.biprod_lift_snd_f_assoc, CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom, lift_desc, associator_inv

CategoryTheory.Limits.biproduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	26 math math: lift_map, CategoryTheory.Limits.biproductBiproductIso_inv, CategoryTheory.Limits.biproductBiproductIso_hom, lift_matrix_assoc, lift_desc_assoc, ι_matrix, reindex_inv, lift_desc, ι_matrix_assoc, CategoryTheory.Mat_.isoBiproductEmbedding_hom, lift_π_assoc, CategoryTheory.Mat_.embeddingLiftIso_inv_app, CategoryTheory.Functor.mapBiproduct_hom, isoProduct_inv, CategoryTheory.Limits.biproductUniqueIso_inv, fromSubtype_eq_lift, lift_map_assoc, uniqueUpToIso_hom, whiskerEquiv_inv_eq_lift, lift_matrix, lift_eq, lift_π, map_lift_mapBiprod, whiskerEquiv_hom_eq_lift, CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_inv_app, conePointUniqueUpToIso_hom

CategoryTheory.Limits.end_

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_π, lift_π_assoc

CategoryTheory.Limits.equalizer

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: lift_ι, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, lift_ι_assoc, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, CategoryTheory.Limits.map_lift_equalizerComparison_assoc, CategoryTheory.Limits.map_lift_equalizerComparison, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, isoSourceOfSelf_inv

CategoryTheory.Limits.image

Definitions

Name	Category	Theorems
lift 📖	CompOp	13 math math: lift_mk_factorThruImage, lift_fac_assoc, CategoryTheory.Limits.HasImage.uniq, fac_lift, CategoryTheory.PreservesImage.iso_hom, CategoryTheory.MonoOver.image_map, lift_mono, fac_lift_assoc, lift_fac, isImage_lift, lift_mk_factorThruImage_assoc, lift_mk_comp_assoc, lift_mk_comp

CategoryTheory.Limits.kernel

Definitions

Name	Category	Theorems
lift 📖	CompOp	39 math math: CategoryTheory.ShortComplex.Exact.epi_kernelLift, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_H, CategoryTheory.cokernelUnopUnop_inv, CategoryTheory.kernelOpUnop_hom, congr_inv, CategoryTheory.Limits.kernelCompMono_hom, CategoryTheory.Abelian.im_map, CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom_assoc, lift_ι_apply, CategoryTheory.kernelUnopUnop_inv, CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom, CategoryTheory.Limits.kernelIsIsoComp_hom, CategoryTheory.cokernelUnopOp_hom, CategoryTheory.Limits.kernelIsIsoComp_inv, CategoryTheory.ShortComplex.cyclesIsoKernel_hom, lift_mono, lift_map, lift_ι_assoc, CategoryTheory.Abelian.imageIsoImage_inv, CategoryTheory.kernelUnopOp_hom, CategoryTheory.Limits.map_lift_kernelComparison, CategoryTheory.Limits.map_lift_kernelComparison_assoc, CategoryTheory.ShortComplex.HasLeftHomology.hasCokernel, CategoryTheory.cokernelOpUnop_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_π, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e, CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift, CategoryTheory.Limits.kernelZeroIsoSource_inv, SheafOfModules.relationsOfIsCokernelFree_s, lift_ι, CategoryTheory.kernelOpOp_inv, lift_zero, CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso, congr_hom, CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv, CategoryTheory.Limits.kernelCompMono_inv, CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv_assoc, CategoryTheory.cokernelOpOp_inv, CategoryTheory.Limits.ker_map

CategoryTheory.Limits.limit

Definitions

Name	Category	Theorems
lift 📖	CompOp	33 math math: CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom, CategoryTheory.Functor.pointwiseRightKanExtension_lift_app, CategoryTheory.Mon.limitConeIsLimit_lift_hom, lift_post, isLimit_lift, CategoryTheory.Limits.kernelBiprodFstIso_inv, CategoryTheory.Limits.productUniqueIso_inv, CategoryTheory.lift_comp_preservesLimitIso_hom_assoc, CategoryTheory.lift_comp_preservesLimitIso_hom, CategoryTheory.Limits.kernelBiproductπIso_inv, lift_π_app, CategoryTheory.Limits.Types.Limit.lift_π_apply, lift_π_apply, lift_pre, coneMorphism_hom, lift_π_assoc, lift_map, CategoryTheory.Functor.pointwiseRightKanExtension_map, CategoryTheory.Limits.kernelBiprodSndIso_inv, CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor, lift_π_app_assoc, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv, lift_map_assoc, CategoryTheory.Limits.Types.Limit.lift_π_apply', lift_π, lift_cone, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom_assoc, CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv, lift_extend, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv_assoc

CategoryTheory.Limits.prod

Definitions

Name	Category	Theorems
lift 📖	CompOp	78 math math: TopCat.isInducing_pullback_to_prod, CategoryTheory.Dial.braiding_inv_f, lift_map, CategoryTheory.Dial.rightUnitorImpl_inv_f, CategoryTheory.Dial.tensorHom_F, CategoryTheory.Limits.isPullback_equalizer_prod, CategoryTheory.monoidalOfHasFiniteProducts.associator_hom, lift_fst_assoc, rightUnitor_inv, CategoryTheory.prodComonad_δ_app, symmetry'_assoc, HomotopicalAlgebra.FibrantBrownFactorization.mk'_i, CategoryTheory.Dial.associator_hom_F, CategoryTheory.Dial.associatorImpl_inv_F, lift_fst, HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z, CategoryTheory.Dial.rightUnitor_hom_F, CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd, CategoryTheory.Dial.comp_le_lemma, mono_lift_of_mono_right, mono_lift_of_mono_left, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, CategoryTheory.Dial.rightUnitorImpl_hom_F, leftUnitor_inv, lift_map_assoc, CategoryTheory.Dial.leftUnitor_inv_f, CategoryTheory.Dial.braiding_inv_F, CategoryTheory.Dial.associator_inv_f, CategoryTheory.Dial.braiding_hom_f, CategoryTheory.Dial.rightUnitor_inv_f, CategoryTheory.overToCoalgebra_map_f, CategoryTheory.Dial.associatorImpl_hom_F, CategoryTheory.Pretriangulated.binaryProductTriangle_mor₁, CategoryTheory.Dial.Hom.le, CategoryTheory.Dial.leftUnitor_hom_F, CategoryTheory.Dial.whiskerRight_F, symmetry', CategoryTheory.NonPreadditiveAbelian.lift_sub_lift, associator_hom, CategoryTheory.Dial.tensorHomImpl_F, TopCat.range_pullback_to_prod, associator_inv, CategoryTheory.Dial.comp_F, AlgebraicGeometry.instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift, CategoryTheory.Dial.associator_inv_F, braiding_hom, CategoryTheory.NonPreadditiveAbelian.lift_map_assoc, CategoryTheory.Limits.biprod.isoProd_hom, TopCat.isEmbedding_pullback_to_prod, CategoryTheory.Dial.leftUnitorImpl_hom_F, HomotopicalAlgebra.FibrantBrownFactorization.mk'_r, comp_lift, CategoryTheory.Dial.braiding_hom_F, lift_snd, CategoryTheory.Dial.associatorImpl_inv_f, CategoryTheory.Dial.whiskerLeft_F, CategoryTheory.overToCoalgebra_obj_a, CategoryTheory.Dial.associator_hom_f, AlgebraicGeometry.IsImmersion.instLiftSchemeId, CategoryTheory.Dial.leftUnitorImpl_inv_f, CategoryTheory.Dial.associatorImpl_hom_f, comp_diag, braiding_inv, CategoryTheory.NonPreadditiveAbelian.sub_def, AlgebraicGeometry.Scheme.instIsClosedImmersionLiftIdOfIsSeparated, CategoryTheory.NonPreadditiveAbelian.lift_map, CategoryTheory.Limits.mono_pullback_to_prod, CategoryTheory.NonPreadditiveAbelian.lift_σ, CategoryTheory.NonPreadditiveAbelian.lift_σ_assoc, HomotopicalAlgebra.FibrantBrownFactorization.mk'_p, CategoryTheory.Over.forgetAdjStar_unit_app_left, lift_snd_assoc, comp_lift_assoc, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, lift_fst_comp_snd_comp, CategoryTheory.monoidalOfHasFiniteProducts.associator_inv, lift_fst_snd

CategoryTheory.Limits.pullback

Definitions

Name	Category	Theorems
lift 📖	CompOp	43 math math: AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, CategoryTheory.Limits.pullbackFstFstIso_hom, CategoryTheory.PreOneHypercover.cylinderHom_h₁, lift_fst_assoc, AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId, CategoryTheory.PreZeroHypercover.interLift_h₀, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, lift_snd, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app, CategoryTheory.MorphismProperty.baseChange_map', AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, CategoryTheory.Limits.pullback_lift_diagonal_isPullback, CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁', lift_snd_assoc, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.Over.mapPullbackAdj_unit_app, CategoryTheory.Over.pullback_map_left, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_π, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, CategoryTheory.PreOneHypercover.sieve₀_cylinder, HomotopicalAlgebra.PathObject.trans_ι, CategoryTheory.MonoOver.inf_map_app, CategoryTheory.MorphismProperty.Over.pullback_map_left, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_right, CategoryTheory.PreOneHypercover.toPullback_cylinder, CategoryTheory.Over.lift_left, CategoryTheory.PreOneHypercover.cylinder_p₁, CategoryTheory.Limits.map_lift_pullbackComparison, CategoryTheory.PreOneHypercover.cylinder_p₂, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f, lift_fst, CategoryTheory.Limits.map_lift_pullbackComparison_assoc, lift_fst_snd, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, CategoryTheory.Limits.pullbackFstFstIso_inv, HomotopicalAlgebra.PrepathObject.RightHomotopy.trans_h, CategoryTheory.Limits.pullback_lift_map_isPullback, HomotopicalAlgebra.PrepathObject.trans_ι, CategoryTheory.PreOneHypercover.cylinderHom_h₀, CategoryTheory.PreOneHypercover.cylinder_Y

CategoryTheory.Limits.wideEqualizer

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_ι_assoc, lift_ι

CategoryTheory.Localization

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: CategoryTheory.Functor.instIsRightDerivedFunctorLiftInvFac, CategoryTheory.Functor.instIsLeftDerivedFunctorLiftHomFac

CategoryTheory.Localization.Construction

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: CategoryTheory.Localization.instIsEquivalenceLocalizationLift, lift_obj, WhiskeringLeftEquivalence.inverse_map_app, lift_map, CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift, fac, CategoryTheory.Functor.IsLocalization.isEquivalence

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: CategoryTheory.Localization.strictUniversalPropertyFixedTargetId_lift, CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift, fac

CategoryTheory.Mat_

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_obj, embeddingLiftIso_hom_app, embeddingLiftIso_inv_app, equivalenceSelfOfHasFiniteBiproducts_functor, lift_additive, lift_map

CategoryTheory.MonoOver

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: congr_unitIso, lift_obj_arrow, congr_functor, congr_inverse, lift_obj_obj, lift_map_hom, congr_counitIso, lift_comm

CategoryTheory.MorphismProperty.Comma

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_obj_toComma, lift_map_hom

CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: fac

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
lift 📖	CompOp	23 math math: CategoryTheory.Equivalence.congrFullSubcategory_inverse, instCommShiftHomFunctorLiftCompιIso, lift_obj_obj, topEquivalence_counitIso, lift_map, CategoryTheory.Equivalence.congrFullSubcategory_counitIso, CategoryTheory.RightExactFunctor.whiskeringLeft_map_app, CategoryTheory.RightExactFunctor.whiskeringRight_map_app, CategoryTheory.LeftExactFunctor.whiskeringRight_map_app, CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app, instFullFullSubcategoryLift, CategoryTheory.ExactFunctor.whiskeringLeft_map_app, CategoryTheory.Equivalence.congrFullSubcategory_unitIso, CategoryTheory.ExactFunctor.whiskeringRight_map_app, CategoryTheory.Functor.instAdditiveFullSubcategoryLift, CategoryTheory.Equivalence.congrFullSubcategory_functor, CategoryTheory.Functor.toEssImageCompι_inv_app, ι_obj_lift_map, CategoryTheory.Functor.toEssImageCompι_hom_app, instFaithfulFullSubcategoryLift, ι_obj_lift_obj, topEquivalence_inverse, isTriangulated_lift

CategoryTheory.Over

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_obj, liftCone_π_app, liftCocone_ι_app, liftCone_pt, liftCocone_pt, lift_map

CategoryTheory.Paths

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_unique, lift_spec, lift_cons, lift_toPath, lift_nil

CategoryTheory.PreservesFiniteLimitsOfFlat

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: fac

CategoryTheory.Presieve.CoverByImageStructure

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: fac, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def, fac_assoc

CategoryTheory.Presieve.FunctorPushforwardStructure

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: fac

CategoryTheory.Pretriangulated.productTriangle

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_hom₁, lift_hom₃, lift_hom₂

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_commutes_zero_assoc, lift_commutes_zero, lift_commutes, lift_commutes_assoc

CategoryTheory.Quiv

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_obj, lift_map

CategoryTheory.Quotient

Definitions

Name	Category	Theorems
lift 📖	CompOp	10 math math: lift.isLift_hom, LiftCommShift.iso_hom_app, liftCommShift_compatibility, lift_map_functor_map, lift_unique, lift_obj_functor_obj, liftCommShift_commShiftIso, lift.isLift_inv, LiftCommShift.iso_inv_app, lift_spec

CategoryTheory.RanIsSheafOfIsCocontinuous

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: fac_assoc, fac', fac

CategoryTheory.ShortComplex.Exact

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_f, lift_f_assoc

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_ι, lift_ι_assoc, lift_app_coe, Subpresheaf.lift_ι

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

CategoryTheory.Subfunctor.Subpresheaf.equalizer

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

CategoryTheory.Subfunctor.equalizer

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_ι', lift_ι'_assoc, lift_ι, lift_ι_assoc, CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift_ι, CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift_ι'

CategoryTheory.Subobject

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply, lift_mk, CategoryTheory.Limits.kernelOrderHom_coe, CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply, CategoryTheory.Limits.cokernelOrderHom_coe

CategoryTheory.Under

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: liftCone_pt, lift_obj, liftCocone_ι_app, liftCone_π_app, liftCocone_pt, lift_map

CategoryTheory.WithInitial

Definitions

Name	Category	Theorems
lift 📖	CompOp	11 math math: liftToInitialUnique_hom_app, inclLift_hom_app, liftStar_lift_map, inclLiftToInitial_inv_app, inclLift_inv_app, inclLiftToInitial_hom_app, lift_map, liftStar_hom, liftToInitialUnique_inv_app, lift_obj, liftStar_inv

CategoryTheory.WithTerminal

Definitions

Name	Category	Theorems
lift 📖	CompOp	11 math math: liftStar_inv, liftStar_hom, lift_map, inclLift_hom_app, lift_obj, liftToTerminalUnique_inv_app, lift_map_liftStar, inclLiftToTerminal_inv_app, inclLift_inv_app, inclLiftToTerminal_hom_app, liftToTerminalUnique_hom_app

CliffordAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: ExteriorAlgebra.lift_symm_apply, lift_ι_apply, range_lift, ι_range_map_lift, ι_comp_lift, lift_unique, lift_symm_apply, lift_comp_ι, GradedAlgebra.lift_ι_eq

CliffordAlgebra.even

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_ι, lift_symm_apply_bilin

CochainComplex.mappingCone

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: lift_f_fst_v, lift_f_fst_v_assoc, ofHom_lift, lift_fst, lift_snd, lift_desc_f, lift_f_snd_v, lift_f, lift_f_snd_v_assoc

CompHaus

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_lifts, lift_lifts_assoc

CompHausLike.pullback

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_fst_assoc, isLimit_lift, lift_fst, lift_snd_assoc, lift_snd

Complex

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_apply, lift_symm_apply_coe

Con

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: lift_surjective_of_surjective, lift_comp_mk', lift_unique, lift_mk', lift_coe, lift_apply_mk', lift_range, map_apply

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	—	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—	smul_le_smul_of_nonneg_right zero_le_one zero_smul add_smul one_smul smul_assoc

CoxeterSystem

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_apply_simple

DirectLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_def, Module.lift_apply, lift_injective

DirectLimit.Module

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_of, lift_apply

DirectLimit.Ring

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_of

DualNumber

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: range_lift, lift_apply_eps, lift_inlAlgHom_eps, lift_smul, lift_apply_apply, coe_lift_symm_apply, lift_apply_inl, lift_op_smul, lift_comp_inlHom

ENat

Definitions

Name	Category	Theorems
lift 📖	CompOp	14 math math: Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, lt_lift_iff, lift_one, lift_zero, lift_le_iff, lift_lt_iff, coe_lift, lift_eq_toNat_of_lt_top, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, lift_coe, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, lift_ofNat, le_lift_iff, lift_add

ExteriorAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_symm_apply, lift_ι_apply, lift_comp_ι, ι_comp_lift, lift_unique

Filter

Definitions

Name	Category	Theorems
lift 📖	CompOp	41 math math: lift_mono', lift_lift_same_eq_lift, uniformity_lift_le_comp, lift_iInf_le, map_lift_eq, lift_le, prod_lift_lift, lift'_lift_assoc, lift_assoc, prod_lift'_lift', le_lift, lift_top, lift_principal, monotone_lift, nhds_nhds_eq_uniformity_uniformity_prod, mem_lift, comap_lift_eq2, lift_iInf_of_map_univ, lift_lift'_same_le_lift', lift_lift'_assoc, lift_map_le, sInter_lift_sets, lift_comm, mem_lift_sets, lift_lift'_same_eq_lift', lift_inf, lift_iInf_of_directed, lift_const, lift_neBot_iff, lift_lift_same_le_lift, lift_iInf, map_lift_eq2, lift_principal2, tendsto_lift, lift_nhds_left, HasBasis.lift, lift_nhds_right, comap_lift_eq, prod_def, lift_mono, HasBasis.mem_lift_iff

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Filter.HasBasis Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.instPartialOrder	Filter.lift	—	mem_lift_iff

FiniteArchimedeanClass

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_mk

FiniteMulArchimedeanClass

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_mk

Finsupp

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: Rep.diagonalSuccIsoFree_inv_hom_single, Rep.leftRegularHom_hom, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, llift_apply, lift_apply, Rep.indResAdjunction_counit_app_hom_hom, lift_symm_apply, Rep.indResHomEquiv_symm_apply_hom

FirstOrder.Language.DirectLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_unique, lift_quotient_mk'_sigma_mk', lift_of, range_lift

FreeAbelianGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	13 math math: lift_add, liftMonoid_coe_addMonoidHom, liftAddGroupHom_apply, lift_unique, lift_comp_apply, mul_def, liftMonoid_coe, lift_comp, lift_add_apply, lift_neg_apply, lift_apply_of, lift_neg, liftMonoid_symm_coe

FreeAddGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	11 math math: lift_mk, lift_apply_of, lift_unique, closure_eq_range, lift_of_eq_id, map_eq_lift, range_lift_le, lift_symm_apply, lift_eq_sum_map, lift_of_apply, range_lift_eq_closure

FreeAddGroup.Red.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	FreeAddGroup.Red.Step	FreeAddGroup.Lift.aux	—	AddSemigroup.to_isLawfulIdentity AddSemigroup.to_isAssociative neg_add_cancel_left add_neg_cancel_left

FreeAddMagma

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_comp_of, lift_comp_of', lift_symm_apply, lift_of

FreeAddMonoid

Definitions

Name	Category	Theorems
lift 📖	CompOp	13 math math: lift_symm_apply, lift_ofList, lift_apply, lift_comp_of, lift_eval_of, mrange_lift, lift_restrict, AddMonoid.Coprod.lift_apply_mk, comp_lift, lift_of_comp_eq_map, hom_map_lift, CharacterModule.homEquiv_apply_apply, AddSubmonoid.closure_eq_mrange

FreeAddSemigroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_comp_of, lift_symm_apply, lift_of, lift_of_add, lift_comp_of'

FreeAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	12 math math: lift_comp_ι, liftAux_eq, lift_ι_apply, Algebra.adjoin_range_eq_range_freeAlgebra_lift, MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, ι_comp_lift, lift_unique, lift_symm_apply, AlgCat.free_map, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, Algebra.adjoin_eq_range_freeAlgebra_lift, AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure

FreeCommRing

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: FirstOrder.Ring.lift_genericPolyMap, FirstOrder.Ring.realize_termOfFreeCommRing, FirstOrder.Field.lift_genericMonicPoly, lift_of, lift_comp_of

FreeGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	16 math math: lift_of_eq_id, lift_apply_of, FreeGroupBasis.lift_apply_apply, lift_unique, injective_lift_of_ping_pong, lift_symm_apply, range_lift_eq_closure, closure_eq_range, freeGroupEquivCoprodI_symm_apply, freeGroupEquivCoprodI_apply, FreeAbelianGroup.liftAddEquiv_apply_apply, lift_mk, lift_eq_prod_map, range_lift_le, map_eq_lift, lift_of_apply

FreeGroup.Red.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	FreeGroup.Red.Step	FreeGroup.Lift.aux	—	Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative inv_mul_cancel_left mul_inv_cancel_left

FreeGroupBasis

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_apply_apply, lift_symm_apply

FreeLieAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: of_comp_lift, lift_comp_of, lift_unique, universalEnvelopingEquivFreeAlgebra_apply, lift_symm_apply, lift_of_apply

FreeMagma

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_of, lift_symm_apply, lift_comp_of, lift_comp_of'

FreeMonoid

Definitions

Name	Category	Theorems
lift 📖	CompOp	12 math math: lift_restrict, lift_of_comp_eq_map, lift_ofList, lift_comp_of, comp_lift, lift_eval_of, mrange_lift, hom_map_lift, lift_symm_apply, lift_apply, Monoid.Coprod.lift_apply_mk, Submonoid.closure_eq_mrange

FreeNonUnitalNonAssocAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: of_comp_lift, lift_unique, lift_symm_apply, lift_of_apply, lift_comp_of

FreeRing

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp_of, lift_of

FreeSemigroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_symm_apply, lift_comp_of', lift_of_mul, lift_comp_of, lift_of

Function.Periodic

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: Real.fourierCoeff_tsum_comp_add, lift_coe

GradedTensorProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_tmul

HNNExtension

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_of, lift_t

Hausdorffification

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_eq, lift_comp_of, lift_of

Ideal.Quotient

Definitions

Name	Category	Theorems
lift 📖	CompOp	10 math math: lift_surjective_of_surjective, RingHom.lift_injective_of_ker_le_ideal, lift_mk, Ideal.ker_quotient_lift, Ideal.injective_lift_iff, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, liftₐ_apply, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, AlgebraicGeometry.Scheme.Hom.toImage_app, lift_comp_mk

Ideal.ResidueField

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_algebraMap

IntermediateField

Definitions

Name	Category	Theorems
lift 📖	CompOp	13 math math: lift_inj, lift_le, lift_adjoin_simple, lift_top, lift_inf, InfiniteGalois.restrict_fixedField, mem_lift, lift_injective, lift_bot, lift_adjoin, lift_sup, liftAlgEquiv_apply, lift_restrict

IsAdicComplete

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: mkQ_comp_lift, of_lift, of_comp_lift, eq_lift, mk_lift

IsAdicComplete.StrictMono

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: eq_lift, of_comp_lift, of_lift, mkQ_comp_lift, mk_lift

IsAdjoinRoot

Definitions

Name	Category	Theorems
lift 📖	CompOp	10 math math: eq_lift, lift_self, lift_root, lift_map, lift_algebraMap, lift_self_apply, lift_algEquiv, apply_eq_lift, coe_liftHom, lift_algebraMap_apply

IsAlgClosed

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

IsBaseChange

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp, lift_eq

IsFractionRing

Definitions

Name	Category	Theorems
lift 📖	CompOp	11 math math: FractionRing.algebraMap_liftAlgebra, coe_liftAlgHom, AlgebraicIndependent.lift_reprField, liftAlgHom_toRingHom, lift_fieldRange_eq_of_range_eq, AlgebraicIndependent.aevalEquivField_apply_coe, lift_unique, lift_fieldRange, lift_mk', lift_algebraMap, liftAlgHom_apply

IsFreeGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_of, lift_symm_apply

IsIntegralClosure

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, algebraMap_lift, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply

IsLocalRing.ResidueField

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp_residue, lift_residue_apply

IsLocalization

Definitions

Name	Category	Theorems
lift 📖	CompOp	16 math math: lift_algebraMap_eq_algebraMap, bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom, lift_mk'_spec, lift_comp, lift_eq, coe_liftAlgHom, liftAlgHom_apply, lift_mk', Localization.mapToFractionRing_apply, lift_of_comp, lift_id, liftAlgHom_toRingHom, lift_injective_iff, lift_unique, lift_eq_iff, lift_surjective_iff

IsLocalization.Away

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp, lift_eq

IsLocalizedModule

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_comp, lift_comp_iso, lift_apply, lift_unique, lift_iso

IsNormalClosure

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

IsSepClosed

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_def

IsSymmetricAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_eq, lift_unique, lift_comp_linearMap

IsTensorProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_eq

LinearAlgebra.FreeProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_unique, lift_algebraMap, lift_symm_apply, lift_apply, lift_comp_ι

LinearOrder

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

LocalizedModule

Definitions

Name	Category	Theorems
lift 📖	CompOp	8 math math: lift_unique, IsLocalizedModule.lift_comp_iso, lift_comp, lift_mk, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, lift_mk_one, IsLocalizedModule.lift_iso, Module.FinitePresentation.exists_basis_localizedModule_powers

LocallyConstant

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_comp_proj

Magma.AssocQuotient

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_comp_of', lift_comp_of, lift_of, lift_symm_apply

Mathlib.Tactic

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Mathlib.Tactic.BicategoryCoherence.LiftHom

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Mathlib.Tactic.BicategoryCoherence.LiftHom₂

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Mathlib.Tactic.Coherence.LiftHom

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Mathlib.Tactic.Coherence.LiftObj

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Mathlib.Tactic.Ring.CSLift

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: inj, Mathlib.Tactic.Ring.instCSLiftValLift, Mathlib.Tactic.Ring.CSLiftVal.eq

Module.DirectLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_injective, lift_of, ModuleCat.directLimitIsColimit_desc, lift_comp_of, lift_of'

Module.Presentation.CokernelData

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: Module.Presentation.cokernelRelations_relation, Module.Presentation.cokernel_relation, ofSection_lift, Module.Presentation.ofExact_relation, π_lift

ModuleCat.HasLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_hom_apply, productLimitCone_isLimit_lift

ModuleCat.image

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_fac

Monoid.Coprod

Definitions

Name	Category	Theorems
lift 📖	CompOp	13 math math: lift_apply_inr, lift_inr_inl, lift_apply_inl, mrange_lift, range_lift, lift_inl_inr, comp_lift, lift_comp_swap, lift_comp_inr, lift_swap, lift_comp_inl, lift_apply_mk, lift_unique

Monoid.CoprodI

Definitions

Name	Category	Theorems
lift 📖	CompOp	14 math math: lift_of, inv_def, mrange_eq_iSup, lift_mrange_le, range_eq_iSup, freeGroupEquivCoprodI_symm_apply, lift_of', lift_symm_apply, of_leftInverse, lift_word_ping_pong, lift_comp_of', lift_comp_of, lift_range_le, lift_injective_of_ping_pong

Monoid.PushoutI

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_base, homEquiv_symm_apply, lift_of

MonoidAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	10 math math: Rep.to_Module_monoidAlgebra_map_aux, Representation.asAlgebraHom_def, lift_symm_apply, lift_apply', lift_apply, lift_mapRangeRingHom_algebraMap, lift_def, lift_single, lift_of, lift_unique'

MulArchimedeanClass

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_mk

NormedAddGroupHom

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_mk, lift_normNoninc, lift_unique, lift_norm_le, norm_lift_le

NormedAddGroupHom.Equalizer

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: liftEquiv_apply, lift_normNoninc, ι_comp_lift, lift_apply_coe, norm_lift_le

NormedAddGroupHom.ker

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: incl_comp_lift, lift_apply_coe

NumberField.ComplexEmbedding

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_comp_algebraMap, NumberField.InfinitePlace.comap_mk_lift, lift_algebraMap_apply

OmegaCompletePartialOrder

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

OrderBot

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

OrderTop

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Ordinal

Definitions

Name	Category	Theorems
lift 📖	CompOp	45 math math: isSuccLimit_lift, lift_type_lt, sInf_compl_lt_lift_ord_succ, lift_one, type_uLift, liftInitialSeg_coe, lift_lt, lift_pred, lift_id, PSet.rank_eq_wfRank, lift_type_eq, liftPrincipalSeg_coe, mem_range_lift_of_card_le, lift_lift, lift_succ, Cardinal.lift_ord, Cardinal.lift_preBeth, RelIso.ordinal_lift_type_eq, lift_inj, lt_lift_iff, lift_uzero, lift_natCast, lift_cof, lift_add, lift_id', lift_zero, isSuccPrelimit_lift, lift_typein_top, typein_ordinal, type_lift_preimage, Cardinal.lift_aleph, lift_preOmega, lift_type_le, le_lift_iff, ZFSet.rank_eq_wfRank, Cardinal.lift_beth, lift_omega0, lift_omega, lift_ofNat, lift_card, lift_mul, lift_univ, lift_umax, lift_le, Cardinal.lift_preAleph

PFun

Definitions

Name	Category	Theorems
lift 📖	CompOp	19 math math: Nat.rfind_min', res_univ, coe_preimage, coe_val, lift_graph, Nat.Partrec.Code.computable_recOn, core_restrict, Computable₂.partrec₂, lift_injective, Nat.Partrec'.of_prim, Computable.partrec, Dioph.diophFn_iff_pFun, prodLift_fst_comp_snd_comp, Nat.Partrec.of_eq_tot, coe_id, coe_comp, Nat.Partrec'.head, dom_coe, Nat.Partrec.of_primrec

PadicInt

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_sub_val_mem_span, lift_unique, lift_spec, lift_self

PartialOrder

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: compare_of_injective_eq_compareOfLessAndEq

PerfectClosure

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

PerfectRing

Definitions

Name	Category	Theorems
lift 📖	CompOp	18 math math: lift_comp_lift_eq_id, lift_comp_lift, lift_lift, comp_lift_apply, lift_lift_apply, liftEquiv_apply, IsPerfectClosure.equiv_toRingHom, lift_comp_lift_apply, lift_id_apply, lift_self, lift_comp_lift_apply_eq_self, lift_apply, lift_comp, lift_comp_apply, comp_lift, IsPerfectClosure.equiv_symm_toRingHom, lift_id, lift_self_apply

Perfection

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_apply_apply_coe, lift_symm_apply, PerfectionMap.lift_apply, PerfectionMap.equiv_apply

PerfectionMap

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_symm_apply, lift_apply

PiTensorProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	17 math math: lift_reindex, lift.tprod, liftAlgHom_apply, lift_reindex_symm, toDualContinuousMultilinearMap_apply_apply, norm_eval_le_injectiveSeminorm, liftEquiv_symm_apply, liftEquiv_apply, lift_comp_reindex, lift_tprod, liftIsometry_apply_apply, norm_eval_le_projectiveSeminorm, lift_comp_map, lift.unique', lift_comp_reindex_symm, lift.unique, lift_symm

Polynomial.IsSplittingField

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Polynomial.SplittingField

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

PosSMulMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	PosSMulMono	—	smul_le_smul_of_nonneg_left

PosSMulReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	PosSMulReflectLE	—	le_of_smul_le_smul_left

PosSMulReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	PosSMulReflectLT	—	lt_iff_lt_of_le_iff_le' lt_of_smul_lt_smul_left

PosSMulStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	PosSMulStrictMono	—	lt_iff_lt_of_le_iff_le' smul_lt_smul_of_pos_left

PowerBasis

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: lift_aeval, AdjoinRoot.equiv'_symm_toAlgHom, liftEquiv_symm_apply, equivOfMinpoly_apply, AdjoinRoot.equiv'_symm_apply, equivOfRoot_apply, lift_gen

Preorder

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

PresentedAddMonoid

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: toMonoid.unique, lift_of

PresentedMonoid

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: toMonoid.unique, lift_of

Profinite

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_lifts_assoc, lift_lifts

ProfiniteGrp.ProfiniteCompletion

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_eta, lift_eta_assoc, ProfiniteGrp.profiniteCompletion_map

Projectivization

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_mk

QuadraticAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_apply_apply, lift_symm_apply_coe

QuaternionAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_apply, lift_symm_apply

QuaternionAlgebra.Basis

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_zero, lift_smul, lift_one, liftHom_apply, lift_mul, lift_add

Quiver.FreeGroupoid

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_unique, lift_spec

Quiver.Push

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_unique, lift_comp, lift_obj

Quiver.Symmetrify

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_spec, lift_reverse, lift_unique

QuotientAddGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	10 math math: AdjoinRoot.evalEval_apply, lift_mk', ker_lift, lift_comp_mk', lift_mk, norm_lift_apply_le, lift_surjective_of_surjective, lift_quot_mk, KaehlerDifferential.quotKerTotalEquiv_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply

QuotientGroup

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_mk, lift_comp_mk', lift_mk', ker_lift, lift_surjective_of_surjective, lift_quot_mk

Relation.ReflTransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	—	Relation.ReflTransGen	—	—	trans_induction_on single trans

Relation.TransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	—	—	—	—	—

Representation.Coinvariants

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_mk, lift_comp_mk, Rep.indResAdjunction_counit_app_hom_hom, Rep.indResHomEquiv_symm_apply_hom

Ring.DirectLimit

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: lift_comp_of, lift_of, lift_injective, lift_of'

RingCon

Definitions

Name	Category	Theorems
lift 📖	CompOp	14 math math: lift_comp_mk', lift_unique, lift_apply_mk', lift_surjective_iff, lift_bijective_iff, lift_surjective_of_surjective, lift_mk', range_lift, rangeS_lift, coe_liftₐ, map_apply, liftₐ_coe_toRingHom, lift_injective_iff, lift_coe

RingQuot

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: eq_lift_comp_mkRingHom, lift_unique, lift_mkRingHom_apply, lift_def

SMulPosMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	SMulPosMono	—	smul_le_smul_of_nonneg_right

SMulPosReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	SMulPosReflectLE	—	le_of_smul_le_smul_right lt_iff_lt_of_le_iff_le'

SMulPosReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	SMulPosReflectLT	—	lt_of_smul_lt_smul_right lt_iff_lt_of_le_iff_le'

SMulPosStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	Preorder.toLE	SMulPosStrictMono	—	lt_iff_lt_of_le_iff_le' smul_lt_smul_of_pos_right

SSet.StrictSegal.isPointwiseRightKanExtensionAt

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: fac_aux₂, fac_aux₃, fac_aux₁

SSet.Subcomplex

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_ι, lift_ι_assoc, lift_app_coe

SSet.Truncated.HomotopyCategory

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_obj_mk, lift_map_homMk

Sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	—	Sbtw	—	—	Wbtw.lift wbtw

SemiNormedGrp.completion

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp_incl, lift_unique

SemidirectProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_inr, lift_inl, lift_comp_inl, lift_comp_inr, lift_unique

SeparationQuotient

Definitions

Name	Category	Theorems
lift 📖	CompOp	10 math math: lift_comp_mk, tendsto_lift_nhds_mk, continuousAt_lift, continuous_lift, uniformContinuous_lift, continuousWithinAt_lift, continuousOn_lift, lift_mk, liftCLM_apply, tendsto_lift_nhdsWithin_mk

SimpleGraph.ComponentCompl

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

SimpleGraph.ConnectedComponent

Definitions

Name	Category	Theorems
lift 📖	CompOp	1 math math: lift_mk

SkewMonoidAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: lift_apply', lift_of, lift_single, lift_apply, lift_unique', lift_def, lift_symm_apply

StandardEtalePair

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: homEquiv_symm_apply, StandardEtalePresentation.toPresentation_algebra_smul, lift_X, StandardEtalePresentation.lift_bijective, StandardEtalePresentation.toPresentation_σ', StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, StandardEtalePresentation.toPresentation_val, lift_X_left, StandardEtalePresentation.toPresentation_relation

Submonoid.LocalizationMap

Definitions

Name	Category	Theorems
lift 📖	CompOp	24 math math: lift_comp_lift_eq, lift_spec, lift_eq_iff, mulEquivOfLocalizations_apply, lift_mul_right, lift_of_comp, IsLocalization.lift_spec_mul_add, lift_localizationMap_mk', lift_unique, lift_mk', lift_surjective_iff, lift_comp, mulEquivOfLocalizations_symm_apply, lift_apply, Localization.mulEquivOfQuotient_apply, lift_left_inverse, lift_spec_mul, lift_eq, lift_mk'_spec, lift_mul_left, lift_injective_iff, lift₀_def, lift_comp_lift, lift_id

Submonoid.LocalizationMap.AwayMap

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: lift_comp, lift_eq

Surreal

Definitions

Name	Category	Theorems
lift 📖	CompOp	—

Sym2

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_comp_map, coe_lift_symm_apply, lift_smul_lift, lift_mk, lift_map_apply

SymmetricAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_ι_apply, IsSymmetricAlgebra.equiv_apply, lift_comp_ι, lift_ι, IsSymmetricAlgebra.equiv_toAlgHom

T2Quotient

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: continuous_lift, lift_mk, unique_lift

TensorAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	7 math math: ι_comp_lift, lift_symm_apply, lift_ι_apply, lift_comp_ι, range_lift, LinearAlgebra.FreeProduct.lift_apply, lift_unique

TensorProduct

Definitions

Name	Category	Theorems
lift 📖	CompOp	27 math math: map₂_eq_range_lift_comp_mapIncl, ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply, Algebra.IsEpi.injective_lift_mul, lift.unique, lift.tmul', Rep.indResAdjunction_counit_app_hom_hom, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, IsTensorProduct.equiv_apply, lift_compr₂ₛₗ, lift.tmul, lift_comp_map, Coalgebra.lift_lsmul_comp_counit_comp_comul, groupHomology.H1AddEquivOfIsTrivial_symm_apply, LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul, lift_mk, AlgebraTensorModule.lift_apply, Module.Flat.iff_lift_lsmul_comp_subtype_injective, LinearMap.rid_comp_lTensor, Algebra.injective_lift_lsmul, lift_compr₂, LinearMap.lid_comp_rTensor, IsTensorProduct.equiv_toLinearMap, lift_mk_compr₂ₛₗ, lift_comp_comm_eq, lift_mk_compr₂, Rep.indResHomEquiv_symm_apply_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply

TensorProduct.AlgebraTensorModule

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: uncurry_apply, lift_apply, lift_tmul, Algebra.FormallyUnramified.comp_sec

TensorProduct.LieModule

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: coe_liftLie_eq_lift_coe, lift_apply

Topology.IsQuotientMap

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_apply, lift_comp, liftEquiv_apply

TrivSqZeroExt

Definitions

Name	Category	Theorems
lift 📖	CompOp	9 math math: lift_inlAlgHom_inrHom, lift_comp_inrHom, lift_apply_inr, liftEquiv_apply, liftEquivOfComm_apply, lift_def, lift_comp_inlHom, lift_apply_inl, range_liftAux

Trivialization

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: proj_lift, lift_self

Trunc

Definitions

Name	Category	Theorems
lift 📖	CompOp	2 math math: LinearMap.detAux_def, lift_mk

Unitization

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_symm_apply_apply, lift_range, lift_symm_apply, lift_range_le, lift_apply_apply, lift_apply

UniversalEnvelopingAlgebra

Definitions

Name	Category	Theorems
lift 📖	CompOp	6 math math: lift_unique, ι_comp_lift, lift_ι_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, lift_symm_apply, lift_ι_apply'

ValuativeRel.ValueGroupWithZero

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_mul, lift_mk, lift_zero, lift_valuation, lift_one

Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	—	Wbtw	—	—	affineSegment.lift

WithOne

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_coe, lift_one, lift_unique

WithZero

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_coe, lift_zero, lift_unique

WittVector

Definitions

Name	Category	Theorems
lift 📖	CompOp	4 math math: truncate_comp_lift, liftEquiv_apply, truncate_lift, lift_unique

ZMod

Definitions

Name	Category	Theorems
lift 📖	CompOp	5 math math: lift_castAddHom, lift_comp_coe, lift_comp_castAddHom, lift_coe, lift_injective

Zsqrtd

Definitions

Name	Category	Theorems
lift 📖	CompOp	3 math math: lift_symm_apply_coe, lift_apply_apply, lift_injective

affineSegment

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	—	Set Set.instHasSubset affineSegment	—	zero_smul smul_le_smul_of_nonneg_right zero_le_one one_smul smul_assoc

openSegment

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	—	Set Set.instHasSubset openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_lt_smul_of_pos_right zero_lt_one NeZero.one zero_smul add_smul one_smul smul_assoc

segment

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift 📖	mathematical	—	Set Set.instHasSubset segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_le_smul_of_nonneg_right zero_le_one zero_smul add_smul one_smul smul_assoc

---

← Back to Index