Last active
September 14, 2022 12:29
-
-
Save riccardobrasca/9c421bbd9292cd82eb854abc3035f6e3 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| AddCommGroup.add_subgroup.equiv_top_symm_apply 1 | |
| AddCommGroup.colimit_comparison 1 | |
| AddCommGroup.hom_product_comparison 1 | |
| AddCommGroup.is_iso_hom_product_comparison 1 | |
| add_comm_group.limit_on_nat_torsion_free 1 | |
| AddCommGroup.tensor_functor_flip_additive 1 | |
| AddCommGroup.tensor_uncurry_curry 1 | |
| AddCommGroup.zmod_resolution_is_resolution 1 | |
| AddCommGroup.zmod_resolution_pi 1 | |
| add_equiv.mk_symm_apply 1 | |
| add_equiv.ulift_symm_apply 1 | |
| add_monoid_hom.comp_mem_filtration 1 | |
| add_monoid_hom.const_smul_hom_int_mem_filtration 1 | |
| add_monoid_hom.const_smul_hom_nat_mem_filtration 1 | |
| add_monoid_hom.eval_mem_filtration 1 | |
| add_monoid_hom.id_mem_filtration 1 | |
| add_monoid_hom.mk_from_pi_mem_filtration 1 | |
| aux_thm69.equiv.group_mul_apply 1 | |
| aux_thm69.equiv.group_mul_symm_apply 1 | |
| aux_thm69.equiv_Icc_bdd_nonneg_apply 1 | |
| aux_thm69.equiv.le_one_ge_one_eval 1 | |
| aux_thm69.equiv.le_one_ge_one_symm_eval 1 | |
| aux_thm69.equiv.lt_one_gt_one_eval 1 | |
| aux_thm69.equiv.lt_one_gt_one_symm_eval 1 | |
| aux_thm69.equiv.mul_inv_eval 1 | |
| aux_thm69.int.nonneg_equiv_nat 1 | |
| aux_thm69.mul_inv_fun_comp_id_apply 1 | |
| aux_thm69.my_summable_shift 1 | |
| aux_thm69.nat.le_equiv_nat 1 | |
| aux_thm69.sum_Icc_sum_tail 1 | |
| bicartesian.quatro_cone_acyclic 1 | |
| bicartesian.quatro_cone_d_12' 1 | |
| bicartesian.quatro_cone_d_23' 1 | |
| bicartesian.quatro_cone_d_34' 1 | |
| bicartesian.quatro_cone_X_1 1 | |
| bicartesian.quatro_cone_X_2 1 | |
| bicartesian.quatro_cone_X_3 1 | |
| bicartesian.quatro_cons_acyclic 1 | |
| bounded_derived_category.complete_distinguished_triangle_morphism 1 | |
| bounded_derived_category.rotate_distinguished_triangle 1 | |
| bounded_homotopy_category.hom_single_iso_naturality' 1 | |
| bounded_homotopy_category.val_as_bdd_above 1 | |
| breen_deligne.basic_universal_map.eval_FP2'_not_suitable 1 | |
| breen_deligne.basic_universal_map.eval_LCFP'_not_suitable 1 | |
| breen_deligne.basic_universal_map.eval_png₀_coe 1 | |
| breen_deligne.basic_universal_map.proj_aux_kronecker_proj_aux 1 | |
| breen_deligne.BD_map₂_app_f 1 | |
| breen_deligne.data.additive_whiskering_left 1 | |
| breen_deligne.data.additive_whiskering_right 1 | |
| breen_deligne.data.complex₂_obj_d 1 | |
| breen_deligne.data.complex_d_comp_d 1 | |
| breen_deligne.data.comp_suitable 1 | |
| breen_deligne.data.eval_functor_comp 1 | |
| breen_deligne.data.hom_pow'_proj' 1 | |
| breen_deligne.data.hom_pow'_suitable_strict 1 | |
| breen_deligne.data.hom_pow'_sum' 1 | |
| breen_deligne.data.suitable.of_basic 1 | |
| breen_deligne.FP2_def 1 | |
| breen_deligne.FreeMat.iso_mk'_hom 1 | |
| breen_deligne.FreeMat.to_FreeAbMat 1 | |
| breen_deligne.package.Biprod_iso_Pow_two_components_inv 1 | |
| breen_deligne.package.endo_T_obj_obj_e 1 | |
| breen_deligne.package.eval'_bounded_above 1 | |
| breen_deligne.package.eval'_obj_X_0 1 | |
| breen_deligne.package.eval'_obj_X_succ 1 | |
| breen_deligne.package.Pow_comp_Pow_components_inv 1 | |
| breen_deligne.universal_map.eval_CLCFPTinv₂_rescale 1 | |
| breen_deligne.universal_map.eval_CLCFPTinv_sub 1 | |
| breen_deligne.universal_map.eval_FP2_of 1 | |
| breen_deligne.universal_map.eval_FP2_sub 1 | |
| breen_deligne.universal_map.eval_Pow_functor_obj 1 | |
| breen_deligne.universal_map.factor_le_of_suitable 1 | |
| breen_deligne.universal_map.factor_sub 1 | |
| breen_deligne.universal_map.suitable_congr 1 | |
| breen_deligne.universal_map.suitable_smul_iff 1 | |
| breen_deligne.universal_map.suitable_sub 1 | |
| category_theory.additive_equivalence_inverse 1 | |
| category_theory.adjunction.whiskering_right_counit 1 | |
| category_theory.adjunction.whiskering_right_unit 1 | |
| category_theory.arrow.conerve_to_cocomplex_homology_is_zero 1 | |
| category_theory.colimit_homology_functor_iso 1 | |
| category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_sheafification_compatibility 1 | |
| category_theory.discrete.left_unitor_def 1 | |
| category_theory.endomorphisms.mk_bo_ho_ca 1 | |
| category_theory.endomorphisms.mk_bo_ho_ca' 1 | |
| category_theory.eval_functor_colimit_iso 1 | |
| category_theory.exact_inr_fst 1 | |
| category_theory.exact_seq.of_unop 1 | |
| category_theory.functor.d_from_map 1 | |
| category_theory.functor.finite_product_condition_iff_finite_product_condition' 1 | |
| category_theory.functor.flip_evaluation_comp_whiskering_right 1 | |
| category_theory.functor.is_proetale_sheaf_of_empty_of_product_of_equalizer 1 | |
| category_theory.functor.is_proetale_sheaf_of_types_projective 1 | |
| category_theory.functor.is_singleton_iff_exists_bijective_to_punit 1 | |
| category_theory.functor.is_singleton_iff_forall_bijective_to_is_singleton 1 | |
| category_theory.functor.map_commsq 1 | |
| category_theory.functor.map_next_iso_inv 1 | |
| category_theory.functor.map_prev_iso_hom 1 | |
| category_theory.functor.obj_biprod_iso 1 | |
| category_theory.functor.obj_X_next_hom_eq 1 | |
| category_theory.functor.obj_X_prev_hom_eq 1 | |
| category_theory.functor.preserves_finite_colimits_of_exact 1 | |
| category_theory.functor.whiskering_right_obj_comp 1 | |
| category_theory.grothendieck_topology.eq_zero_of_forall 1 | |
| category_theory.grothendieck_topology.is_iso_sheafify_lift_of_is_iso 1 | |
| category_theory.homology_functor_preserves_filtered_colimits 1 | |
| category_theory.homology_iso_inv_homology_functor_map 1 | |
| category_theory.is_iso_of_is_iso_preadditive_yoneda_map_app 1 | |
| category_theory.is_iso_sheafification_types_adjunction_counit_app 1 | |
| category_theory.is_snake_input.cokernel_to'_mono 1 | |
| category_theory.is_snake_input.eq_δ_of_spec 1 | |
| category_theory.is_snake_input.hom_eq_zero₁ 1 | |
| category_theory.limits.concrete.equalizer_equiv_apply 1 | |
| category_theory.limits.concrete.equalizer_ext 1 | |
| category_theory.limits.is_limit_op_fan 1 | |
| category_theory.limits.is_zero_iff_exact_zero_zero 1 | |
| category_theory.limits.is_zero_unop 1 | |
| category_theory.limits.preserves_zero_of_preserves_initial 1 | |
| category_theory.limits.zero_of_epi_comp_zero 1 | |
| category_theory.monoidal_functor.map_associator_hom 1 | |
| category_theory.nat_trans.kernel_fork_X_map 1 | |
| category_theory.presheaf_to_SheafOfTypes_iso 1 | |
| category_theory.projective.epi_homology_map_of_pseudoelement 1 | |
| category_theory.projective.homology.π_iso_cokernel_lift_hom 1 | |
| category_theory.projective.mono_homology_functor_of_pseudoelement 1 | |
| category_theory.projective.pullback_comp_mono_iso_fst 1 | |
| category_theory.Sheaf.hom.comp_val_assoc 1 | |
| category_theory.sheafification_adjunction_types_counit_app 1 | |
| category_theory.sheafification_adjunction_types_hom_equiv_apply 1 | |
| category_theory.sheafification_adjunction_types_hom_equiv_symm_apply 1 | |
| category_theory.sheafification_adjunction_types_unit_app 1 | |
| category_theory.sheafification_types_reflective 1 | |
| category_theory.Sheaf.iso.mk_hom_val 1 | |
| category_theory.Sheaf.iso.mk_inv_val 1 | |
| category_theory.short_exact_sequence.comp_snd_assoc 1 | |
| category_theory.short_exact_sequence.Fst_additive 1 | |
| category_theory.short_exact_sequence.id_fst 1 | |
| category_theory.short_exact_sequence.id_snd 1 | |
| category_theory.short_exact_sequence.id_trd 1 | |
| category_theory.short_exact_sequence.is_iso_of_fst_of_trd 1 | |
| category_theory.short_exact_sequence.mk_of_split' 1 | |
| category_theory.short_exact_sequence.mk_split_split 1 | |
| category_theory.short_exact_sequence.Snd_additive 1 | |
| category_theory.short_exact_sequence.tfae_split 1 | |
| category_theory.short_exact_sequence.Trd_additive 1 | |
| category_theory.sigma_functor_preserves_epi 1 | |
| category_theory.sigma_functor_preserves_mono 1 | |
| category_theory.sites.pullback_sheafification_compatibility_hom_apply_val 1 | |
| category_theory.snake_diagram.mk_functor'' 1 | |
| category_theory.snake.mk_of_homology 1 | |
| category_theory.splitting.splittings_comm 1 | |
| category_theory.triangulated.triangle_morphism_is_iso_iff 1 | |
| category_theory.triangulated.triangle.nonneg_rotate_neg₃ 1 | |
| category_theory.triangulated.triangle.obj₁_functor 1 | |
| category_theory.triangulated.triangle.obj₂_functor 1 | |
| category_theory.triangulated.triangle.obj₃_functor 1 | |
| category_theory.triangulated.triangle.shift_comm_eq_eq_to_hom 1 | |
| category_theory.triangulated.triangle.shift_hom₁ 1 | |
| category_theory.triangulated.triangle.shift_hom₂ 1 | |
| category_theory.triangulated.triangle.shift_hom₃ 1 | |
| category_theory.triangulated.triangle.shift_mor₁ 1 | |
| category_theory.triangulated.triangle.shift_mor₂ 1 | |
| category_theory.triangulated.triangle.shift_mor₃ 1 | |
| category_theory.triangulated.triangle.shift_obj₁ 1 | |
| category_theory.triangulated.triangle.shift_obj₂ 1 | |
| category_theory.triangulated.triangle.shift_obj₃ 1 | |
| chain_complex.exact_zero_fst_iff_mono 1 | |
| chain_complex.exact_zero_snd_iff_epi 1 | |
| chain_complex_nat_has_homology 1 | |
| CLCFP_def 1 | |
| CLCFP.Tinv_def' 1 | |
| CLCTinv.map_nat_iso 1 | |
| cochain_complex.cons_d_01 1 | |
| cochain_complex.cons_d_succ 1 | |
| cochain_complex.cons_X_0 1 | |
| cochain_complex.cons_X_succ 1 | |
| cochain_complex.hom.cons_f_0 1 | |
| cochain_complex.hom.cons_f_succ 1 | |
| cochain_complex.imker.cokernel.desc_comp_left 1 | |
| cochain_complex.imker.cokernel.desc_is_iso 1 | |
| cochain_complex.imker.homology_zero_zero' 1 | |
| cochain_complex.imker.image_to_kernel_eq_image_to_kernel_of_eq_fst 1 | |
| cochain_complex.imker.image_to_kernel_eq_image_to_kernel_of_eq_snd 1 | |
| cochain_complex.imker.image_to_kernel_zero_left' 1 | |
| cochain_complex.imker.is_iso_cokernel_pi_image_to_kernel_of_zero_of_zero 1 | |
| cochain_complex.imker.kernel_subobject_map_epi_of_epi 1 | |
| cochain_complex.imker.sq_from_epi_of_epi 1 | |
| cochain_complex.imker.X_iso_image_inv 1 | |
| cochain_complex_int_has_homology 1 | |
| commsq.ι_iso_inv 1 | |
| CompHaus.coe_id_apply 1 | |
| CompHaus.diagram_of_pt_obj 1 | |
| comphaus_filtered_pseudo_normed_group_hom.strict.to_schfpsng_hom 1 | |
| comphaus_filtered_pseudo_normed_group_hom.to_add_monoid_hom_hom_injective 1 | |
| CompHausFiltPseuNormGrp₁.exact_with_constant.extend_aux' 1 | |
| CompHausFiltPseuNormGrp₁.mem_filtration_iff_of_is_limit 1 | |
| CompHausFiltPseuNormGrp₁.rescale_to_Condensed_iso 1 | |
| CompHausFiltPseuNormGrp.rescale₁ 1 | |
| complex_shape.symm_next 1 | |
| complex_shape.symm_prev 1 | |
| Condensed_Ab_CondensedSet_adjunction'_hom_equiv_apply 1 | |
| Condensed_Ab_CondensedSet_adjunction_hom_equiv_apply 1 | |
| Condensed_Ab_CondensedSet_adjunction'_hom_equiv_symm_apply 1 | |
| Condensed_Ab_CondensedSet_adjunction_hom_equiv_symm_apply 1 | |
| Condensed_Ab_to_CondensedSet_preserves_limits_of_shape_of_filtered 1 | |
| Condensed_Ab_to_presheaf_obj 1 | |
| Condensed.coproduct_to_colimit_short_exact_sequence 1 | |
| Condensed.eval_freeAb_iso_component_neg 1 | |
| Condensed.eval_freeAb_iso_component_zero 1 | |
| Condensed.evaluation_exact 1 | |
| Condensed.exactness_in_the_middle_part_one 1 | |
| Condensed_ExtrSheaf_equiv_inverse_val 1 | |
| Condensed.half_internal_hom_eval_iso 1 | |
| Condensed.homology_evaluation_iso 1 | |
| Condensed.homology_functor_evaluation_iso 1 | |
| Condensed.is_iso_iff_ExtrDisc 1 | |
| Condensed.of_top_ab_map_val 1 | |
| Condensed_product_iso_product_spec' 1 | |
| CondensedSet.coe_val_obj_sigma_equiv_symm 1 | |
| CondensedSet.is_colimit_sigma_cone 1 | |
| CondensedSet_presheaf_adjunction_counit_app 1 | |
| CondensedSet_presheaf_adjunction_hom_equiv_apply 1 | |
| CondensedSet_presheaf_adjunction_hom_equiv_symm_apply 1 | |
| CondensedSet_presheaf_adjunction_unit_app 1 | |
| Condensed.tensor_uncurry_eq 1 | |
| condensify_def 1 | |
| condensify_map_zero 1 | |
| condensify_nonstrict_map_add 1 | |
| condensify_nonstrict_map_neg 1 | |
| dual_finset_antimono 1 | |
| embedding.locally_constant_extend_of_empty 1 | |
| ennreal.mul_inv_eq_iff_eq_mul 1 | |
| ennreal.summable_of_coe_sum_eq 1 | |
| ennreal.top_zpow_of_pos 1 | |
| eventually_constant 1 | |
| exact_notation 1 | |
| Ext_coproduct_iso_naturality_inv 1 | |
| ExtQprime_iso_aux_system_comm_setup.add_equiv.to_AddCommGroup_iso_apply 1 | |
| ExtQprime_iso_aux_system_comm_setup.preadditive_yoneda_obj_obj_CondensedSet_to_Condensed_Ab_apply 1 | |
| ExtrDisc_to_Profinite_obj 1 | |
| ExtrSheaf.half_internal_hom_val_obj 1 | |
| ExtrSheafProd.half_internal_hom_val_obj 1 | |
| ExtrSheafProd.hom_has_add 1 | |
| ExtrSheafProd.hom_has_neg 1 | |
| ExtrSheafProd.hom_has_sub 1 | |
| ExtrSheafProd.tensor_functor_flip_additive 1 | |
| ExtrSheafProd.tensor_functor_map_app 1 | |
| ExtrSheafProd.tensor_functor_obj_map 1 | |
| ExtrSheafProd.tensor_presheaf_map 1 | |
| ExtrSheafProd.tensor_uncurry_curry 1 | |
| ExtrSheaf.tensor_functor_map_app 1 | |
| ExtrSheaf.tensor_functor_obj_map 1 | |
| ExtrSheaf.tensor_val_obj 1 | |
| fact_le_of_add_one_le 1 | |
| FiltrationPow.cast_le_vcomp_Tinv 1 | |
| filtration_pow_iso_aux'₀_spec' 1 | |
| filtration_pow_iso_aux'_spec' 1 | |
| filtration_pow_iso_aux_spec' 1 | |
| filtration_pow_iso_spec' 1 | |
| FiltrationPow_map 1 | |
| FiltrationPow.mul_iso_hom 1 | |
| Filtration_rescale 1 | |
| Filtration.Tinv₀_comp_res 1 | |
| finset.mem_span_iff 1 | |
| finset.prod_attach' 1 | |
| finset.prod_comap 1 | |
| finset.sum_nat_abs_le 1 | |
| free_abelian_group.free_predicate.smul_nat_iff 1 | |
| free_abelian_group.lift_id_map 1 | |
| functor.map_map' 1 | |
| generates_norm_of_generates_nnnorm 1 | |
| has_homology.desc_π 1 | |
| has_homology.eq_map_of_π_map_ι 1 | |
| has_homology.fst_eq_zero 1 | |
| has_homology.map_ι_assoc 1 | |
| has_homology.π_comp_desc_assoc 1 | |
| hom_equiv_evaluation_apply_eq_app_id 1 | |
| homological_complex.biprod.lift_map_assoc 1 | |
| homological_complex.cone.desc_of_null_homotopic 1 | |
| homological_complex.cone.lift_of_null_homotopic 1 | |
| homological_complex.cone_to_termwise_split_comp_homotopy 1 | |
| homological_complex.cone.triangle_functorial 1 | |
| homological_complex.embed.d_to_none 1 | |
| homological_complex.embed_eval_is_zero_of_none 1 | |
| homological_complex.embed_homotopy_hom_eq_zero_of_of_none 1 | |
| homological_complex.embed_homotopy_hom_eq_zero_of_to_none 1 | |
| homological_complex.embed_homotopy_hom_some 1 | |
| homological_complex.embed_nat_obj_down_up_pos 1 | |
| homological_complex.embed_nat_obj_down_up_succ_f 1 | |
| homological_complex.embed_nat_obj_down_up_zero_pos 1 | |
| homological_complex.embed.X_some 1 | |
| homological_complex.epi_iff_eval 1 | |
| homological_complex.epi_prev' 1 | |
| homological_complex.eval.category_theory.limits.preserves_colimits_of_size 1 | |
| homological_complex.eval_functor_homology_iso 1 | |
| homological_complex.functor_eval_homology_nat_iso 1 | |
| homological_complex.homological_complex.embed.subsingleton_to_none 1 | |
| homological_complex.homology.desc'_ι 1 | |
| homological_complex.homology.π'_lift 1 | |
| homological_complex.homotopy_category.quotient_obj_shift 1 | |
| homological_complex.homotopy_category.shift_functor_obj_as 1 | |
| homological_complex.homotopy.comp_X_eq_to_iso 1 | |
| homological_complex.homotopy.X_eq_to_iso_comp 1 | |
| homological_complex.hom_single_iso_symm_apply_f 1 | |
| homological_complex.mono_iff_eval 1 | |
| homological_complex.mono_next' 1 | |
| homological_complex.section_X_eq_to_hom 1 | |
| homological_complex.shift_functor_eq 1 | |
| homological_complex.single_obj_iso_zero 1 | |
| homological_complex.termwise_split_epi_lift_retraction 1 | |
| homological_complex.triangleₕ_map_splittings_iso 1 | |
| homological_complex.triangleₕ_of_termwise_split_mor₃ 1 | |
| homological_complex.unop_functor_additive 1 | |
| homology.has_ι 1 | |
| homology.has_π 1 | |
| homology_iso_datum.change.fac₂_assoc 1 | |
| homology_iso_datum.change.fac₃_assoc 1 | |
| homology_iso_datum.tautological'_iso₁ 1 | |
| homology_iso_datum.tautological_iso_hom 1 | |
| homology_iso_predatum.fork_X 1 | |
| homology_map_datum.of_g_are_zeros 1 | |
| homotopy_category.quotient_map_sub 1 | |
| homotopy_category.quotient_op_functor 1 | |
| homotopy_category.quotient_unop_functor 1 | |
| homotopy_category.single_map 1 | |
| homotopy_category.triangleₕ_of_termwise_split_mem_distinguished_triangles 1 | |
| index_up_one_eq_set_up_one_range 1 | |
| int.neg_one_pow_bit0 1 | |
| int.neg_one_pow_bit1 1 | |
| int.neg_one_pow_eq_neg_one_npow 1 | |
| int.neg_one_pow_eq_pow_abs 1 | |
| int.neg_one_pow_sub 1 | |
| int.tsum_eq_nat_tsum_of_bdd_below 1 | |
| invpoly.Tinv_coeff 1 | |
| invpoly.Tinv_hom_to_fun 1 | |
| is_clopen.is_clopen_sUnion 1 | |
| is_locally_constant_iff_clopen_fibers 1 | |
| iso_of_zero_of_bicartesian 1 | |
| laurent_measures.condensedCH 1 | |
| laurent_measures.profinite_comp_PFPNGT₁_to_CHFPNG₁ₑₗ 1 | |
| laurent_measures_ses.Φ_natural 1 | |
| laurent_measures.to_Lbar_surjective 1 | |
| Lbar_bdd.transition_cast_le 1 | |
| Lbar_bdd.transition_transition 1 | |
| Lbar_le.coe_hom_of_normed_group_hom_apply 1 | |
| Lbar_le.truncate_mk_seq 1 | |
| Lbar.Tinv_aux_ne_zero 1 | |
| Lbar.Tinv_ne_zero 1 | |
| lem98.hom_Lbar_cone_X 1 | |
| linear_equiv.to_add_equiv_symm_apply 1 | |
| list.extract_cons_succ_left 1 | |
| list.extract_zero_right 1 | |
| locally_constant.density.mem_finset_clopen_unique' 1 | |
| locally_constant.edist_apply_le 1 | |
| locally_constant.edist_def 1 | |
| locally_constant.norm_const_zero 1 | |
| locally_constant.norm_eq_iff' 1 | |
| lt_of_lt_of_le_unbundled 1 | |
| mk_pullback_fst 1 | |
| nat_abs_lt_nat_abs_of_nonneg_of_lt 1 | |
| nat.injective_pow 1 | |
| nnrat.le_inv_iff_mul_le 1 | |
| nnrat.le_of_forall_lt_one_mul_le 1 | |
| nnrat.mul_finset_sup 1 | |
| nnrat.mul_lt_of_lt_div 1 | |
| nnreal.fact_inv_mul_le 1 | |
| nnreal.fact_le_inv_mul_self 1 | |
| nnreal.fact_le_subst_left' 1 | |
| nnreal.fact_le_subst_right' 1 | |
| nnreal.fact_nat_cast_inv_le_one 1 | |
| nnreal.fact_one_le_add_one 1 | |
| nnreal.fact_two_pow_inv_le_one 1 | |
| nnreal.nat.binary.fund_thm' 1 | |
| nnreal.nat.digit.r_sub_sum_small 1 | |
| nonstrict_extend_mono 1 | |
| NSH_δ_res_f 1 | |
| of_epi_g.to_homology_iso_predatum_π 1 | |
| one_lt_two_r 1 | |
| option.eq_none_or_eq_some 1 | |
| pfpng_ctu_smul_int 1 | |
| pi_induced_induced 1 | |
| PolyhedralLattice.augmentation_map_equalizes 1 | |
| PolyhedralLattice.Cech_conerve.finsupp_fin_one_iso_hom 1 | |
| polyhedral_lattice.filtration_fintype 1 | |
| polyhedral_lattice_hom.coe_inj_iff 1 | |
| polyhedral_lattice_hom.coe_mk_polyhedral_lattice_hom' 1 | |
| polyhedral_lattice_hom.mk_to_add_monoid_hom 1 | |
| PolyhedralLattice.Hom_obj 1 | |
| PolyhedralLattice.Hom_rescale_hom_symm_apply 1 | |
| polyhedral_lattice_hom.to_add_monoid_hom_injective 1 | |
| polyhedral_lattice_hom.to_normed_group_hom 1 | |
| PolyhedralLattice.to_SemiNormedGroup 1 | |
| pow_d_le_z 1 | |
| pow_equiv 1 | |
| pow_filtration_hom_ext 1 | |
| Pow_mul_hom 1 | |
| Pow_mul_inv 1 | |
| pow_pow 1 | |
| Pow_Pow_X_hom_apply 1 | |
| preserves_finite_biproducts_Condensed_evaluation 1 | |
| presheaf_to_Condensed_Ab_preserves_colimits 1 | |
| ProFiltPseuNormGrp₁.mem_filtration_iff_of_is_limit 1 | |
| ProFiltPseuNormGrpWithTinv₁.gadget_cone_π_app 1 | |
| ProFiltPseuNormGrpWithTinv₁.rescale_out 1 | |
| ProFiltPseuNormGrpWithTinv.iso_of_equiv_of_strict'_inv_apply 1 | |
| ProFiltPseuNormGrpWithTinv.of_coe 1 | |
| ProFiltPseuNormGrpWithTinv.Pow_mul_inv 1 | |
| ProFiltPseuNormGrpWithTinv.Pow_rescale_aux_apply 1 | |
| Profinite.compact_space_Radon_LC_of_discrete_quotient 1 | |
| Profinite.discrete_topology_pmz 1 | |
| Profinite.extend_nat_trans_id 1 | |
| Profinite.free'_lift_val_eq_sheafification_lift 1 | |
| profinitely_filtered_pseudo_normed_group_with_Tinv.pi_proj_to_fun 1 | |
| Profinite.normed_free_pfpng_π_w 1 | |
| profinite_pow_filtration_iso_component_spec' 1 | |
| profinite_pow_filtration_iso_spec' 1 | |
| Profinite.Radon_iso_real_measures 1 | |
| Profinite.t2_space_fun_to_R 1 | |
| Profinite.t2_space_Radon_LC 1 | |
| Profinite.t2_space_weak_dual 1 | |
| Profinite.topological_space_bdd_weak_dual_filtration 1 | |
| Profinite.why_do_I_need_this 1 | |
| pseudo_normed_group.cast_le'_eq_cast_le 1 | |
| pseudo_normed_group.coe_sum' 1 | |
| pseudo_normed_group.filtration_prod_equiv 1 | |
| pseudo_normed_group.mem_filtration_prod 1 | |
| pseudo_normed_group.neg_mem_filtration_iff 1 | |
| pseudo_normed_group.pow_incl_apply 1 | |
| pseudo_normed_group.pow_incl_injective 1 | |
| PseuNormGrp₁.level_map' 1 | |
| PseuNormGrp₁.mem_filtration_iff_of_is_limit 1 | |
| PseuNormGrp₁.neg_nat_trans 1 | |
| QprimeFP_map 1 | |
| QprimeFP_sigma_proj_eq_0 1 | |
| real_measures.homeo_filtration_ϖ_ball_preimage 1 | |
| real.Sup_eq' 1 | |
| SemiNormedGroup.iso_rescale_hom 1 | |
| SemiNormedGroup.LocallyConstant_obj_obj 1 | |
| SemiNormedGroup.normed_with_aut_LCC 1 | |
| SemiNormedGroup.T_hom_eq 1 | |
| SemiNormedGroup.truncate.obj_d_add_one 1 | |
| set_up_one_def 1 | |
| set_up_one_span 1 | |
| short_complex.functor_homological_complex_π₁_iso_eval 1 | |
| short_complex.functor_homological_complex_π₃_iso_eval 1 | |
| short_complex.mk_id_τ₁ 1 | |
| short_complex.mk_id_τ₂ 1 | |
| short_complex.mk_id_τ₃ 1 | |
| short_complex.zero_preserves_colimits_of_shape 1 | |
| short_complex.ι_middle_π₁_is_zero 1 | |
| short_complex.π₁_preserves_colimit 1 | |
| short_complex.π₂_preserves_colimit 1 | |
| short_complex.π₃_preserves_colimit 1 | |
| sign_vectors_inhabited 1 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.level_neg 1 | |
| sum_str.op_fst 1 | |
| sum_str.symm_inl 1 | |
| sum_str.unop_fst 1 | |
| system_of_complexes.inv_apply_hom_apply 1 | |
| system_of_complexes.shift_sub_id_is_iso 1 | |
| system_of_complexes.truncate_obj_d_succ_succ 1 | |
| system_of_double_complexes.col_obj_X 1 | |
| system_of_double_complexes.col_res 1 | |
| system_of_double_complexes.col_X 1 | |
| system_of_double_complexes.d'_d' 1 | |
| system_of_double_complexes.row_map_app_f 1 | |
| system_of_double_complexes.row_X 1 | |
| theta.eventually_le_one 1 | |
| theta.ϑ_eq_ϑ' 1 | |
| thm95.Cech_nerve_level_hom_right 1 | |
| thm95.Cech_nerve_level_inv'_left 1 | |
| thm95.Cech_nerve_level_map 1 | |
| thm95.col_complex_level_map 1 | |
| thm95.col_complex_level_obj 1 | |
| thm95.col_complex_level_obj_d 1 | |
| thm95.col_complex_obj_d 1 | |
| thm95.col_complex_obj_iso_X_zero 1 | |
| thm95.double_complex.col'_aux_obj 1 | |
| thm95.double_complex.col_iso_hom_app_f 1 | |
| thm95.double_complex.col_obj_X_zero 1 | |
| thm95.FLC_complex_map 1 | |
| thm95.rescale_nat_trans' 1 | |
| tsum_abs_eq_coe_tsum_nnabs 1 | |
| two_mul_lt_two 1 | |
| two_step_resolution_ab_projective 1 | |
| two_step_resolution_projective_pid 1 | |
| up_down_up_eq 1 | |
| up_two_set_down_one 1 | |
| ϕ_apply 1 | |
| ϕ_natural 1 | |
| AddCommGroup.add_subgroup.equiv_top 2 | |
| AddCommGroup.eq_of_is_zero 2 | |
| AddCommGroup.tensor_curry_equiv_apply 2 | |
| add_equiv.quotient_congr 2 | |
| add_equiv.symm_mk_apply 2 | |
| add_monoid_hom.coe_mk_from_pi 2 | |
| add_monoid_hom.pow_eval 2 | |
| aux_thm69.equiv_compl_R_bdd_apply 2 | |
| aux_thm69.equiv_Icc_R_apply 2 | |
| aux_thm69.int_tsum_shift 2 | |
| aux_thm69.mul_inv_fun_comp_id 2 | |
| aux_thm69.prod_nat_summable_aux 2 | |
| aux_thm69.summable_shift 2 | |
| aux_thm69.sum_range_sum_Icc' 2 | |
| aux_thm69.sum_reverse 2 | |
| bicartesian.quatro_cons_hom_quasi_iso 2 | |
| bounded_homotopy_category.hom_val 2 | |
| breen_deligne.basic_universal_map.suitable_mul_left_le_one 2 | |
| breen_deligne.basic_universal_map.suitable_mul_left_one_le 2 | |
| breen_deligne.basic_universal_map.suitable_mul_right_le_one 2 | |
| breen_deligne.basic_universal_map.suitable_mul_right_one_le 2 | |
| breen_deligne.basic_universal_map.suitable_of_le 2 | |
| breen_deligne.BD_system_map_app_app 2 | |
| breen_deligne.data.complex₂_map_f 2 | |
| breen_deligne.data.complex₂_obj_X 2 | |
| breen_deligne.data.eval_functor'_comp 2 | |
| breen_deligne.data.eval_functor_obj_obj_d 2 | |
| breen_deligne.data.mul_obj_d 2 | |
| breen_deligne.data.proj_f 2 | |
| breen_deligne.data.system_obj_d 2 | |
| breen_deligne.data.system_res_def 2 | |
| breen_deligne.eval_Pow_functor_nat_trans_compatibility 2 | |
| breen_deligne.Mat.comm_semiring 2 | |
| breen_deligne.package.eval_functor_obj_X 2 | |
| breen_deligne.package.main_lemma' 2 | |
| breen_deligne.universal_map.congr_eval_Pow' 2 | |
| breen_deligne.universal_map.eval_CLCFP_sub 2 | |
| breen_deligne.universal_map.eval_CLCFPTinv₂_sub 2 | |
| breen_deligne.universal_map.eval_CLCFPTinv_zero 2 | |
| breen_deligne.universal_map.eval_FP2_add 2 | |
| breen_deligne.universal_map.eval_FP2_neg 2 | |
| breen_deligne.universal_map.eval_LCFP_neg 2 | |
| breen_deligne.universal_map.eval_LCFP_sub 2 | |
| breen_deligne.universal_map.eval_Pow_comp_app 2 | |
| breen_deligne.universal_map.eval_Pow'_hcomp 2 | |
| breen_deligne.universal_map.factor_add 2 | |
| breen_deligne.universal_map.factor_neg 2 | |
| breen_deligne.universal_map.map_eval_Pow' 2 | |
| breen_deligne.universal_map.suitable_mul_left_le_one 2 | |
| breen_deligne.universal_map.suitable_mul_left_one_le 2 | |
| breen_deligne.universal_map.suitable_mul_right_le_one 2 | |
| breen_deligne.universal_map.suitable_mul_right_one_le 2 | |
| breen_deligne.universal_map.suitable_of_le 2 | |
| category_theory.AB5.colim_exact 2 | |
| category_theory.arrow.op_comp_unop 2 | |
| category_theory.arrow.unop_comp_op 2 | |
| category_theory.arrow.unop_hom 2 | |
| category_theory.composable_morphisms.hom.id_τ₁ 2 | |
| category_theory.composable_morphisms.id_τ₁ 2 | |
| category_theory.cosimplicial_object.augmented.cocomplex_map 2 | |
| category_theory.endomorphisms.sub_f 2 | |
| category_theory.eq_to_iso_inv 2 | |
| category_theory.exact.epi_of_exact_zero_right 2 | |
| category_theory.functor.epi_of_epi_of_exact 2 | |
| category_theory.functor.forget₂_additive 2 | |
| category_theory.functor.is_iso_cokernel_comparison_of_exact 2 | |
| category_theory.functor.is_singleton_iff_exists_bijective_to_is_singleton 2 | |
| category_theory.functor.is_singleton_iff_forall_bijective_to_punit 2 | |
| category_theory.functor.map_d_to 2 | |
| category_theory.functor.map_is_biprod 2 | |
| category_theory.functor.preserves_coequalizers_of_exact 2 | |
| category_theory.is_snake_input.hom_eq_zero₂ 2 | |
| category_theory.is_snake_input.δ_spec 2 | |
| category_theory.limits.cokernel.map_desc_assoc 2 | |
| category_theory.limits.epi_of_epi_of_comp_epi_of_mono 2 | |
| category_theory.nat_trans.conj_by 2 | |
| category_theory.preadditive.apply_Pow_hom_app 2 | |
| category_theory.preadditive.apply_Pow_inv_app 2 | |
| category_theory.preadditive.apply_Pow_naturality 2 | |
| category_theory.preadditive.eval_Pow_functor_comp 2 | |
| category_theory.preadditive.Pow_obj 2 | |
| category_theory.preserves_colimits_of_shape_const_zero_aux 2 | |
| category_theory.projective.homology.π_ι_assoc 2 | |
| category_theory.projective.π_cokernel_iso_of_eq 2 | |
| category_theory.short_exact_sequence.Functor 2 | |
| category_theory.short_exact_sequence.functor_map_naturality 2 | |
| category_theory.short_exact_sequence.hom_inj_injective 2 | |
| category_theory.short_exact_sequence.hom_zero_fst 2 | |
| category_theory.short_exact_sequence.hom_zero_snd 2 | |
| category_theory.short_exact_sequence.hom_zero_trd 2 | |
| category_theory.sites.to_sheafify_pullback_sheafification_compatibility 2 | |
| category_theory.snake_diagram.exact_kernel_ι_self 2 | |
| category_theory.snake.row_exact₁_aux 2 | |
| category_theory.snake.row_exact₂_aux 2 | |
| category_theory.triangulated.neg_iso_inv 2 | |
| category_theory.triangulated.triangle.iso.of_components_hom_hom₁ 2 | |
| category_theory.triangulated.triangle.iso.of_components_hom_hom₂ 2 | |
| category_theory.triangulated.triangle.iso.of_components_hom_hom₃ 2 | |
| category_theory.triangulated.triangle.triangle_shift_functor_map 2 | |
| category_theory.triangulated.triangle.triangle_shift_map_hom₁ 2 | |
| category_theory.triangulated.triangle.triangle_shift_map_hom₂ 2 | |
| category_theory.triangulated.triangle.triangle_shift_map_hom₃ 2 | |
| ceil_add_le 2 | |
| CLCTinv.F_def 2 | |
| cochain_complex.imker.cokernel.desc_spec 2 | |
| cochain_complex.imker.image_to_kernel_epi_of_epi 2 | |
| commsq.neg_iso_inv 2 | |
| commsq.ι_iso_hom 2 | |
| CompHaus.continuous_of_is_limit 2 | |
| CompHausFiltPseuNormGrp₁.create_hom_from_level_to_fun 2 | |
| CompHausFiltPseuNormGrp₁.create_iso_from_level_add_aux_aux 2 | |
| CompHausFiltPseuNormGrp₁.create_iso_from_level_zero_aux 2 | |
| CompHausFiltPseuNormGrp₁.level_create_iso_from_level 2 | |
| CompHausFiltPseuNormGrp₁.level_jointly_faithful 2 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.lift_fun_map_add 2 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.lift_fun_map_zero 2 | |
| CompHausFiltPseuNormGrp.rescale_obj 2 | |
| CompHausFiltPseuNormGrp.rescale_preserves_limits_of_shape_discrete_quotient 2 | |
| CompHausFiltPseuNormGrpWithTinv.large_category 2 | |
| complex_shape.embedding.nat_down_int_up_c_iff 2 | |
| Condensed_Ab.to_free_free_lift 2 | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_finite_colimits 2 | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_finite_limits 2 | |
| Condensed.category_theory.Sheaf_to_presheaf.category_theory.is_right_adjoint 2 | |
| Condensed.eval_freeCond'_iso_aux_neg 2 | |
| Condensed.eval_freeCond'_iso_aux_zero 2 | |
| Condensed.forget_to_CondensedType 2 | |
| Condensed.forget_to_CondensedType.category_theory.is_right_adjoint 2 | |
| condensed.Profinite_to_presheaf_Ab 2 | |
| CondensedSet.coe_val_obj_sigma_equiv 2 | |
| CondensedSet.val_obj_sigma_equiv_symm_apply' 2 | |
| Condensed.short_exact_iff_ExtrDisc 2 | |
| condensed.unsheafified_free_Cech' 2 | |
| discrete_quotient.comap_equiv 2 | |
| discrete_quotient.comap_mem_fibre_iff 2 | |
| discrete_quotient.mem_fibre_iff' 2 | |
| ExtrSheafProd.hom_has_zero 2 | |
| ExtrSheafProd.map_tensor_val_app 2 | |
| Filtration.cast_le_apply 2 | |
| FiltrationPow.cast_le_app 2 | |
| floor_add_floor_le 2 | |
| has_homology.map_desc_assoc 2 | |
| has_homology.ι_eq_desc 2 | |
| has_homology.π_eq_lift 2 | |
| homological_complex.biprod.map_desc_assoc 2 | |
| homological_complex.biproduct_bicone_is_coprod 2 | |
| homological_complex.biproduct_bicone_is_prod 2 | |
| homological_complex.biproduct_is_biprod 2 | |
| homological_complex.cokernel_complex_d 2 | |
| homological_complex.cone_from_zero 2 | |
| homological_complex.cone_to_zero 2 | |
| homological_complex.cone.triangle_map_id 2 | |
| homological_complex.congr_next_functor 2 | |
| homological_complex.embed_nat_obj_down_up_succ 2 | |
| homological_complex.epi_of_eval 2 | |
| homological_complex.epi_prev 2 | |
| homological_complex.eval.category_theory.limits.preserves_limits_of_size 2 | |
| homological_complex.eval_functor_equiv 2 | |
| homological_complex.functor_eval.obj_obj_d 2 | |
| homological_complex.homotopy_connecting_hom_of_splittings 2 | |
| homological_complex.kernel_complex_d 2 | |
| homological_complex.mono_next 2 | |
| homological_complex.op_functor_additive 2 | |
| homological_complex.shift_X 2 | |
| homological_complex.termwise_split_epi_desc_split_epi 2 | |
| homological_complex.termwise_split_epi_retraction_lift_aux 2 | |
| homology_iso_datum.of_homological_complex 2 | |
| int.neg_one_pow_even 2 | |
| int.neg_one_pow_neg_one 2 | |
| int.neg_one_pow_odd 2 | |
| invpoly.map_bound' 2 | |
| invpoly.nonneg_of_norm_mul_zpow 2 | |
| invpoly.to_laurent_measures_of_laurent_measures 2 | |
| invpoly.zsmul_apply 2 | |
| is_clopen.is_closed_sUnion 2 | |
| is_lub_iff 2 | |
| iso_on_the_right_neg_spec' 2 | |
| iso_on_the_right_zero_spec' 2 | |
| laurent_measures.map_bound' 2 | |
| laurent_measures.nonneg_of_norm_mul_zpow 2 | |
| laurent_measures_ses.cfpng_hom_add 2 | |
| laurent_measures_ses.cfpng_hom_neg 2 | |
| laurent_measures.zsmul_apply 2 | |
| Lbar_le.cast_le_apply 2 | |
| Lbar.mk_aux' 2 | |
| Lbar.mk_aux_mem_filtration 2 | |
| Lbar.nnnorm_nsmul 2 | |
| LCFP_def 2 | |
| le_unbundled 2 | |
| locally_constant.dist_def 2 | |
| locally_constant.eq_sum_of_fintype 2 | |
| locally_constant.norm_const 2 | |
| maps_comm 2 | |
| Module.coe_of'' 2 | |
| Module.projective_of_of_projective 2 | |
| mul_equiv.quotient_congr 2 | |
| nat.strict_mono_pow 2 | |
| natural_fork 2 | |
| nnrat.bot_eq_zero 2 | |
| nnrat.inv_le_of_le_mul 2 | |
| nnrat.lt_inv_iff_mul_lt 2 | |
| nnrat.mul_sup 2 | |
| nnrat.sum_div 2 | |
| nnreal.fact_le_subst_right 2 | |
| nnreal.nat.binary.zero_fst_le 2 | |
| nnreal.zpow_le_iff_log 2 | |
| nonstrict_extend_map_add 2 | |
| nonstrict_extend_map_neg 2 | |
| normed_add_group_hom.coe_range 2 | |
| normed_free_pfpng_functor_map 2 | |
| normed_snake_dual 2 | |
| pBanach.has_continuous_smul_δ_aux₁ 2 | |
| pBanach.has_continuous_smul_δ_aux₂ 2 | |
| pBanach.has_continuous_smul_δ_aux₃ 2 | |
| pBanach.norm_le_of_forall_sum_le 2 | |
| pBanach.norm_le_of_tendsto 2 | |
| pBanach.sum_rpow_le_norm 2 | |
| pBanach.uniform_continuous_coe 2 | |
| pfpng_ctu_const 2 | |
| pfpng_ctu_id 2 | |
| polyhedral_lattice.add_monoid_hom.coe_incl_apply 2 | |
| PolyhedralLattice.Cech_conerve.map_succ_zero_aux 2 | |
| PolyhedralLattice.Cech_conerve.π_hom 2 | |
| polyhedral_lattice_hom.coe_mk_polyhedral_lattice_hom 2 | |
| PolyhedralLattice.Hom_cosimplicial_zero_iso_aux_rfl 2 | |
| PolyhedralLattice.Hom_map_to_fun 2 | |
| PolyhedralLattice.rescale_obj 2 | |
| Pow_obj 2 | |
| preserves_limits_of_shape_of_filtered_aux 2 | |
| preserves_limits_of_shape_pempty_of_preserves_terminal 2 | |
| ProFiltPseuNormGrp.large_category 2 | |
| ProFiltPseuNormGrpWithTinv.Pow_obj 2 | |
| ProFiltPseuNormGrpWithTinv.rescale_obj 2 | |
| Profinite.compact_space_Radon_LC 2 | |
| Profinite.continuous_Radon_equiv_Radon_LC_symm 2 | |
| Profinite.continuous_weak_dual_LC_to_fun 2 | |
| Profinite.dense_range_coe₂ 2 | |
| Profinite.is_limit_Radon_png_cone_map_level 2 | |
| Profinite.normed_free_pfpng_level_iso 2 | |
| Profinite.Radon_closed_embedding_range_bdd 2 | |
| Profinite.Radon_homeomorph_Radon_LC 2 | |
| Profinite.Radon_iso_limit 2 | |
| Profinite.Radon_iso_Radon_LC 2 | |
| Profinite.Radon_LC_closed_embedding 2 | |
| Profinite.Radon_LC_comparison_naturality_aux 2 | |
| Profinite.Radon_LC_CompHaus_comparison 2 | |
| Profinite.Radon_LC_to_fun_continuous 2 | |
| Profinite.Radon_LC_to_fun_injective 2 | |
| Profinite.Radon_LC_to_Radon 2 | |
| Profinite.Radon_png_iso 2 | |
| Profinite.Radon_to_fun_continuous 2 | |
| Profinite.Radon_to_fun_injective 2 | |
| Profinite.Radon_to_Radon_LC 2 | |
| Profinite.sigma_iso_empty 2 | |
| Profinite.t2_space_Radon 2 | |
| SemiNormedGroup.Completion_T_inv_eq 2 | |
| SemiNormedGroup.forget₂_Ab_obj 2 | |
| SemiNormedGroup.normed_with_aut_Completion 2 | |
| SemiNormedGroup.rescale_obj 2 | |
| SemiNormedGroup.T_hom_incl 2 | |
| set_up_one_antitone 2 | |
| short_complex.functor_nat_iso_mk 2 | |
| short_complex.hom_mk_τ₁ 2 | |
| short_complex.hom_mk_τ₂ 2 | |
| short_complex.hom_mk_τ₃ 2 | |
| system_of_complexes.hom_apply_comp_inv_apply 2 | |
| system_of_complexes.rescale_obj 2 | |
| system_of_complexes.ScaleIndexLeft_apply 2 | |
| system_of_complexes.ScaleIndexLeft_obj_map 2 | |
| system_of_complexes.ScaleIndexRight_apply 2 | |
| system_of_complexes.ScaleIndexRight_obj_map 2 | |
| system_of_complexes.ScaleIndexRight_obj_obj 2 | |
| system_of_double_complexes.d'_comp_d' 2 | |
| system_of_double_complexes.d'_d 2 | |
| tactic.prove_goal_asyncI 2 | |
| theta.bdd_floor 2 | |
| theta.eventually_antitone 2 | |
| theta.finite_sum' 2 | |
| theta.limit_neg_geometric 2 | |
| theta.summable_ϑ_section 2 | |
| theta.ϑ_surjective 2 | |
| thm95.col_complex_obj 2 | |
| thm95.col_complex_rescaled_map 2 | |
| thm95.col_complex_rescaled_obj 2 | |
| thm95.double_complex.col'_map 2 | |
| thm95.scale'_app 2 | |
| thm95.scale_factorial_obj 2 | |
| thm95.to_rescale' 2 | |
| topological_space.clopens.indicator_continuous 2 | |
| topological_space.clopens.indicator_one_inverse_image 2 | |
| up_two_index_down_one 2 | |
| AddCommGroup.projective_of_Z_Module_projective 3 | |
| AddCommGroup.zmod.nsmul_eq_zero 3 | |
| add_equiv.mk_symm 3 | |
| add_monoid_hom.mk_from_pi_apply 3 | |
| add_submonoid.injective_subtype 3 | |
| aux_thm69.equiv_Icc_bdd_nonneg 3 | |
| aux_thm69.equiv_nat_diag 3 | |
| aux_thm69.mul_inv_fun_comp 3 | |
| aux_thm69.range_equiv_Icc 3 | |
| aux_thm69.sum_range_sum_Icc 3 | |
| bounded_derived_category.category_theory.category_comp_val 3 | |
| bounded_derived_category.category_theory.category_hom 3 | |
| bounded_homotopy_category.preserves_coproducts_single 3 | |
| breen_deligne.basic_universal_map.eval_FP2_comp 3 | |
| breen_deligne.basic_universal_map.eval_LCFP_comp 3 | |
| breen_deligne.BD_map_app_f 3 | |
| breen_deligne.FP2.res_comp_Tinv 3 | |
| breen_deligne.package.eval_homotopy 3 | |
| breen_deligne.package.eval'_obj_d_0 3 | |
| breen_deligne.package.eval'_obj_X 3 | |
| breen_deligne.package.hH0_endo₂ 3 | |
| breen_deligne.universal_map.eval_Pow_zero_app 3 | |
| category_theory.composable_morphisms.apply_functor 3 | |
| category_theory.functor.finite_product_condition' 3 | |
| category_theory.functor.is_zero_of_comp 3 | |
| category_theory.functor.map_next 3 | |
| category_theory.functor.map_prev 3 | |
| category_theory.functor.obj_X_next 3 | |
| category_theory.functor.obj_X_prev 3 | |
| category_theory.limits.cofork_of_cokernel_is_colimit 3 | |
| category_theory.nat_trans.map_next 3 | |
| category_theory.nat_trans.map_prev 3 | |
| category_theory.nat_trans.unflip_comp 3 | |
| category_theory.nat_trans.unflip_id 3 | |
| category_theory.preserves_colimits_of_shape_const_zero 3 | |
| category_theory.prod_induction 3 | |
| category_theory.projective.homology.π'_ι_assoc 3 | |
| category_theory.short_exact_sequence.hom.sq1_assoc 3 | |
| category_theory.short_exact_sequence.hom.sq2_assoc 3 | |
| category_theory.short_exact_sequence.iso_of_components' 3 | |
| category_theory.short_exact_sequence.mk_of_split 3 | |
| category_theory.short_exact_sequence.snd_is_iso 3 | |
| category_theory.snake_diagram.mk_functor' 3 | |
| category_theory.snake_lemma.exact_δ 3 | |
| category_theory.snake_lemma.δ_exact 3 | |
| category_theory.triangulated.neg_iso_hom 3 | |
| chain_complex.is_zero_homology_of_exact 3 | |
| CLCFP.res_comp_Tinv 3 | |
| cochain_complex.truncation.image_comp_is_iso_left_comp_ι 3 | |
| commsq.ι_fst_assoc 3 | |
| commsq.ι_snd_assoc 3 | |
| CompHaus.coe_comp_apply 3 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.comp_to_fun 3 | |
| CompHausFiltPseuNormGrp₁.as_lvl_add 3 | |
| CompHausFiltPseuNormGrp₁.product.lift_to_fun 3 | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_coproducts_of_shape 3 | |
| Condensed.coproduct_presentation_eq 3 | |
| Condensed.eval_freeCond'_iso_component_hom_neg 3 | |
| Condensed.eval_freeCond'_iso_component_hom_zero 3 | |
| eq.lhs_def 3 | |
| eq.rhs_def 3 | |
| ExtrDisc.category_theory.category_hom 3 | |
| ExtrSheafProd.category_theory.category_hom 3 | |
| ExtrSheafProd.tensor_functor_additive 3 | |
| ExtrSheaf.tensor_functor_additive 3 | |
| Fintype.normed_free_pfpng_unit 3 | |
| has_homology.π_map_ι 3 | |
| homological_complex.exact_next 3 | |
| homological_complex.exact_prev 3 | |
| homological_complex.functor_eval_map_app_f 3 | |
| homological_complex_has_homology 3 | |
| homological_complex.homotopy_category.shift_as 3 | |
| homological_complex.modify_d 3 | |
| homological_complex.shift_functor_additive 3 | |
| homological_complex.termwise_split_epi_retraction_lift 3 | |
| homological_complex.triangleₕ_map_splittings_hom 3 | |
| homological_complex.X_eq_to_iso_shift 3 | |
| iso_on_the_right_neg_spec 3 | |
| iso_on_the_right_zero_spec 3 | |
| laurent_measures.profiniteCH 3 | |
| laurent_measures_ses.Φ_eq_ϕ 3 | |
| Lbar_le.eq_iff_truncate_eq 3 | |
| LCFP.res_comp_Tinv 3 | |
| LCFP.Tinv_norm_noninc 3 | |
| locally_constant.linear_eval 3 | |
| nat.monotone_pow 3 | |
| nnrat.div_lt_iff 3 | |
| nnrat.div_lt_one_of_lt 3 | |
| nnrat.lt_div_iff 3 | |
| nnreal.le_self_rpow 3 | |
| of_epi_g 3 | |
| os.monotone_pow 3 | |
| pBanach.sum_rpow_le_of_tendsto 3 | |
| PolyhedralLattice.Cech_conerve.map_succ_zero 3 | |
| polyhedral_lattice.conerve.π_is_quotient 3 | |
| PolyhedralLattice.rescale_proj_bound_by 3 | |
| polyhedral_lattice.π_is_quotient 3 | |
| ProFiltPseuNormGrp.bundled_hom 3 | |
| ProFiltPseuNormGrp.coe_comp_apply 3 | |
| ProFiltPseuNormGrpWithTinv₁.coe_comp_apply 3 | |
| ProFiltPseuNormGrpWithTinv₁.product.lift_to_fun 3 | |
| Profinite.bdd_add 3 | |
| Profinite.bdd_LC_iff_comparison 3 | |
| Profinite.bdd_neg 3 | |
| Profinite.bdd_zero 3 | |
| Profinite.compact_space_Radon 3 | |
| Profinite.continuous_Radon_LC_comparison_component_equiv_symm 3 | |
| profinitely_filtered_pseudo_normed_group_with_Tinv.pi_lift_to_fun 3 | |
| Profinite.map_Radon_png 3 | |
| Profinite.prod_cone 3 | |
| Profinite.Radon_functor_iso_Radon_LC_functor 3 | |
| Profinite.Radon_LC_comparison_component_homeo 3 | |
| Profinite.Radon_LC_comparison_component_iso 3 | |
| Profinite.Radon_LC_to_weak_dual 3 | |
| Profinite.Radon_png_comparison_component 3 | |
| Profinite.Radon_png_functor_level_iso_component 3 | |
| Profinite.sigma_sum_iso 3 | |
| Profinite_to_Condensed_map_val 3 | |
| SemiNormedGroup.equalizer.map_nat_id 3 | |
| short_complex.homology_functor_iso_hom_app 3 | |
| short_complex.nat_trans_hom_mk_app_τ₂ 3 | |
| short_complex.nat_trans_hom_mk_comp 3 | |
| short_complex.nat_trans_hom_mk_id 3 | |
| sigma_ι_coproduct_eval_iso 3 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.comp_to_fun 3 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.level_zero 3 | |
| subgroup.comap_eq_iff 3 | |
| sum_str.unop_symm 3 | |
| system_of_complexes.truncate_obj_d_zero_one 3 | |
| theta.eventually_pos_floor 3 | |
| theta.has_sum_x 3 | |
| theta.ϑ' 3 | |
| thm94 3 | |
| thm95.Cech_nerve_level_left_map 3 | |
| thm95.CLCFP'_map_app 3 | |
| thm95.CLCFP'_obj_map 3 | |
| thm95.col_complex_map 3 | |
| thm95.double_complex.col'_obj 3 | |
| topological_space.clopens.indicator_apply 3 | |
| two_step_resolution_hom_ab 3 | |
| weak_dual.bdd_LC_comap 3 | |
| θ_ϕ_exact 3 | |
| AddCommGroup.coe_of' 4 | |
| AddCommGroup.zmod_resolution 4 | |
| add_monoid_hom.mk_polyhedral_lattice_hom' 4 | |
| add_monoid_hom.pow_hom 4 | |
| aux_thm69.aux_ineq_mul 4 | |
| aux_thm69.equiv_bdd_integer_nat 4 | |
| aux_thm69.mul_inv_fun_def 4 | |
| bounded_derived_category.isomorphic_distinguished 4 | |
| bounded_homotopy_category.Ext_coproduct_iso_naturality 4 | |
| breen_deligne.basic_universal_map.pre_eval_apply 4 | |
| breen_deligne.data.eval_functor'_obj_X_map 4 | |
| breen_deligne.universal_map.eval_Pow'_of 4 | |
| breen_deligne.universal_map.map_eval_Pow 4 | |
| breen_deligne.universal_map.suitable_neg 4 | |
| category_theory.composable_morphisms.comp_τ₁ 4 | |
| category_theory.composable_morphisms.comp_τ₃ 4 | |
| category_theory.composable_morphisms.hom.comp_τ₁ 4 | |
| category_theory.composable_morphisms.hom.comp_τ₃ 4 | |
| category_theory.composable_morphisms.hom.id_τ₃ 4 | |
| category_theory.endomorphisms.forget_obj 4 | |
| category_theory.is_snake_input.map_eq_id 4 | |
| category_theory.is_snake_input.to_kernel_epi 4 | |
| category_theory.limits.op_fan 4 | |
| category_theory.projective.category_theory.limits.factor_thru_image.category_theory.strong_epi 4 | |
| category_theory.projective.pullback_comp_mono_iso 4 | |
| category_theory.short_exact_sequence.aux_tac 4 | |
| category_theory.snake.col_exact_aux 4 | |
| category_theory.snake_diagram.hom_tac 4 | |
| category_theory.snake_input.kernel_sequence 4 | |
| chain_complex.exact_iff_is_zero_homology 4 | |
| chain_complex.exact_of_is_zero_homology 4 | |
| chain_complex.is_projective_resolution.mk_ProjectiveResolution 4 | |
| CLCFPTinv₂_def 4 | |
| CLCTinv.map_nat_def 4 | |
| commsq.iso_inv_π 4 | |
| comphaus_filtered_pseudo_normed_group_hom.coe_mk' 4 | |
| comphaus_filtered_pseudo_normed_group_hom.mk_to_monoid_hom 4 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.mk_to_monoid_hom 4 | |
| CompHausFiltPseuNormGrp₁.create_iso_from_level_add_aux 4 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.lift_continuous 4 | |
| CompHausFiltPseuNormGrp₁.lvl_spec 4 | |
| CompHaus.injective_of_is_iso 4 | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_products_of_shape 4 | |
| Condensed.presentation_point_isomorphism 4 | |
| CondensedSet.val_obj_sigma_equiv_symm_apply 4 | |
| embed_unop 4 | |
| has_homology.fst_snd_eq_zero 4 | |
| homological_complex.congr_prev_functor 4 | |
| homological_complex.embed_iso 4 | |
| homological_complex.functor_eval_homology_iso 4 | |
| homological_complex.modify_functor_map_f 4 | |
| homological_complex.next_functor_iso_eval 4 | |
| homological_complex.prev_functor_iso_eval 4 | |
| homology.desc_zero 4 | |
| homotopy.congr_hom 4 | |
| invpoly.zpow_strict_anti 4 | |
| iso_on_the_left_neg₀_spec 4 | |
| iso_on_the_left_zero₀_spec 4 | |
| Lbar_bdd.coeff_bound 4 | |
| Lbar_le.injective_cast_le 4 | |
| map_homological_complex_embed 4 | |
| mul_equiv.surjective_congr 4 | |
| pfpng_ctu_smul_nat 4 | |
| PolyhedralLattice.unrescale 4 | |
| preserves_limits_aux_1 4 | |
| Profinite.bdd_weak_dual_filtration_homeo 4 | |
| Profinite.continuous_Radon_equiv_Radon_LC 4 | |
| Profinite.is_limit_Radon_png_cone 4 | |
| Profinite.normed_free_pfpng_π 4 | |
| Profinite.Radon_CompHaus_comparison 4 | |
| Profinite.Radon_CompHaus_functor_iso_Radon_LC_CompHaus_functor 4 | |
| Profinite.Radon_LC_CompHaus_diagram 4 | |
| Profinite.weak_dual_C_equiv_LC 4 | |
| Profinite.weak_dual_LC_to_fun 4 | |
| PseuNormGrp₁.level_map 4 | |
| real.pow_nnnorm_sum_le 4 | |
| rel.decidable_rel 4 | |
| SemiNormedGroup.truncate_obj 4 | |
| short_complex.functor_homological_complex_π₁_iso_prev_functor 4 | |
| short_complex.functor_homological_complex_π₃_iso_next_functor 4 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.mk_to_monoid_hom 4 | |
| strict_pseudo_normed_group_hom.mk_to_monoid_hom 4 | |
| system_of_complexes.is_weak_bounded_exact.iff_of_iso 4 | |
| system_of_double_complexes.truncate.d_π 4 | |
| theta.eventually_pos_y 4 | |
| theta.summable_floor 4 | |
| theta.ϑ₀ 4 | |
| thm95.Cech_nerve_level_obj 4 | |
| weak_dual.bdd_comap 4 | |
| weak_dual.bdd_iff_indexed_parition 4 | |
| aux_thm69.equiv_compl_R_bdd 5 | |
| aux_thm69.equiv_Icc_R 5 | |
| aux_thm69.equiv.le_one_ge_one 5 | |
| aux_thm69.equiv.lt_one_gt_one 5 | |
| aux_thm69.prod_nat_summable 5 | |
| breen_deligne.package.hH0_endo 5 | |
| category_theory.composable_morphisms.hom.id_τ₂ 5 | |
| category_theory.functor.map_endomorphisms_map_f 5 | |
| category_theory.has_snake_lemma 5 | |
| category_theory.limits.cofork_of_cokernel 5 | |
| category_theory.presheaf_to_SheafOfTypes 5 | |
| category_theory.short_exact_sequence.comp_trd 5 | |
| category_theory.short_exact_sequence.f_comp_g 5 | |
| category_theory.short_exact_sequence.has_nsmul 5 | |
| category_theory.short_exact_sequence.has_zsmul 5 | |
| category_theory.short_exact_sequence.mk_split 5 | |
| cochain_complex.imker.X_iso_kernel 5 | |
| commsq.bicartesian_iff 5 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.level_coe 5 | |
| CompHausFiltPseuNormGrp₁.level_cone_compatible 5 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.fac_aux 5 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.lift_strict 5 | |
| complex_shape.embedding.nat_up_int_up 5 | |
| Condensed.evaluation_additive 5 | |
| Condensed.exact_colim_of_exact_of_is_filtered 5 | |
| down_two_up 5 | |
| ExtrSheafProd.evaluation_additive 5 | |
| ExtrSheafProd.tensor_curry_uncurry 5 | |
| ExtrSheafProd.tensor_val 5 | |
| free_abelian_group.free_predicate.smul_iff 5 | |
| homological_complex.cone.triangle_map 5 | |
| homological_complex.cone_X 5 | |
| homological_complex.embed_nat_obj_down_up_zero 5 | |
| homological_complex.termwise_split_epi_desc 5 | |
| locally_constant.nnnorm_apply_le_nnnorm 5 | |
| nnrat.half_lt_self 5 | |
| nnreal.inv_mul_le_iff 5 | |
| PolyhedralLattice.coe_id 5 | |
| ProFiltPseuNormGrp.coe_id 5 | |
| Profinite.is_limit_Radon_LC_CompHaus_cone 5 | |
| Profinite.is_limit_Radon_LC_cone.continuous_Radon_LC 5 | |
| Profinite.Radon_closed_embedding 5 | |
| Profinite.Radon_png_comparison 5 | |
| Sheaf.hom_equiv_apply 5 | |
| short_complex.functor_category_equivalence.functor_unit_iso_comp 5 | |
| short_complex.functor_homological_complex_π₂_iso_eval 5 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.level_add 5 | |
| strict_pseudo_normed_group_hom.level_coe 5 | |
| tactic.interactive.asyncI 5 | |
| theta.exists_limit_y 5 | |
| thm95.rescale_functor' 5 | |
| aux_thm69.equiv.group_mul 6 | |
| bicartesian.quatro_cons_hom 6 | |
| breen_deligne.data.proj_suitable 6 | |
| breen_deligne.package.eval'_obj_d 6 | |
| breen_deligne.package.Pow_X_hom 6 | |
| breen_deligne.universal_map.eval_Pow_zero 6 | |
| category_theory.composable_morphisms.comp_τ₂ 6 | |
| category_theory.composable_morphisms.hom.comp_τ₂ 6 | |
| category_theory.snake_diagram.o_snd 6 | |
| CLCFP_rescale 6 | |
| CLCTinv.map_nat_app 6 | |
| CompHausFiltPseuNormGrp₁.create_hom_from_level 6 | |
| CompHausFiltPseuNormGrp₁.to_Condensed_obj 6 | |
| CompHausFiltPseuNormGrp.to_Condensed_obj 6 | |
| condensify_map_comp 6 | |
| continuous_map.comap_LC_linear_map 6 | |
| Filtration_obj_map_apply 6 | |
| homological_complex.embed.d_of_none 6 | |
| homological_complex.termwise_split_epi_lift 6 | |
| homological_complex.termwise_split_epi_retraction 6 | |
| homology.lift_desc' 6 | |
| int.neg_one_pow_ite 6 | |
| locally_constant.has_edist 6 | |
| nat_up_int_down_c_iff 6 | |
| nnreal.nat.digit.zero_def 6 | |
| ProFiltPseuNormGrp.CompHausFiltPseuNormGrp.category_theory.has_forget₂ 6 | |
| Profinite.is_limit_Radon_CompHaus_cone 6 | |
| Profinite.Radon_png_cone 6 | |
| Profinite.Radon_png_functor_level_iso 6 | |
| Profinite.Radon_to_weak_dual 6 | |
| Profinite.weak_dual_LC_to_C 6 | |
| pseudo_normed_group.pow_incl 6 | |
| SemiNormedGroup.equalizer.map_nat_app 6 | |
| theta.eventually_le 6 | |
| theta.summable_nnnorm 6 | |
| theta.ϑ_section 6 | |
| thm95.scale' 6 | |
| topological_space.clopens.indicator_LC_apply 6 | |
| AddCommGroup.Ab.category_theory.limits.has_colimits_of_size 7 | |
| bounded_derived_category.pretriangulated 7 | |
| breen_deligne.FP2.Tinv_def 7 | |
| category_theory.short_exact_sequence.exact_of_split 7 | |
| category_theory.triangulated.is_iso_of_is_iso_of_is_iso 7 | |
| CompHausFiltPseuNormGrp.level_obj 7 | |
| Condensed.half_internal_hom_iso 7 | |
| Condensed_product_iso_biproduct_spec 7 | |
| CondensedSet.evaluation_map 7 | |
| coproduct_eval_iso 7 | |
| discrete_quotient.mem_fibre_iff 7 | |
| free_pfpng.discrete_quotient_separates_points 7 | |
| has_homology.desc_comp 7 | |
| homological_complex.category_theory.limits.has_colimits_of_size 7 | |
| homological_complex.category_theory.limits.has_limits_of_size 7 | |
| homological_complex.functor_eval.obj_map_f 7 | |
| homology_iso_datum.change.η_iso 7 | |
| int.neg_one_pow_neg 7 | |
| LCFP.Tinv_def 7 | |
| lc_to_c 7 | |
| liquid_tensor_experiment.sections 7 | |
| nat.eq_zero_or_exists_eq_add_of_ne_one 7 | |
| nnrat.two_inv_lt_one 7 | |
| pBanach.has_p_norm 7 | |
| pBanach.lp.nontrivial 7 | |
| Profinite.Radon_LC_to_fun 7 | |
| Profinite.Radon_to_fun 7 | |
| sum_str.op_symm 7 | |
| theta.limit_y 7 | |
| two_step_resolution_ab_X 7 | |
| two_step_resolution_X 7 | |
| AddCommGroup.to_direct_sum 8 | |
| aux_thm69.equiv.mul_inv_rev 8 | |
| breen_deligne.package.Pow_X_inv 8 | |
| category_theory.endomorphisms.neg_f 8 | |
| category_theory.is_snake_input.cokernel_to' 8 | |
| category_theory.short_exact_sequence.g_nat 8 | |
| CompHausFiltPseuNormGrp₁.create_iso_from_level_compat_aux 8 | |
| CompHausFiltPseuNormGrp₁.is_limit_ext 8 | |
| has_homology.snd_eq_zero 8 | |
| homological_complex.biproduct_bicone 8 | |
| Lbar_le.coe_cast_le 8 | |
| locally_constant.continuous_eval 8 | |
| pBanach.has_continuous_smul_δ_aux 8 | |
| product_iso_biproduct_spec' 8 | |
| ProFiltPseuNormGrp₁.is_limit_ext 8 | |
| ProFiltPseuNormGrpWithTinv₁.is_limit_ext 8 | |
| Profinite.extend_map 8 | |
| Profinite.Radon_equiv_Radon_LC 8 | |
| Profinite.Radon_LC_CompHaus_cone 8 | |
| two_step_resolution_ab_d 8 | |
| two_step_resolution_d 8 | |
| two_step_resolution_hom 8 | |
| bounded_derived_category 9 | |
| bounded_derived_category.val.homotopy_category.is_K_projective 9 | |
| breen_deligne.basic_universal_map.eval_of 9 | |
| breen_deligne.basic_universal_map.pre_eval 9 | |
| breen_deligne.data.complex_X 9 | |
| breen_deligne.universal_map.eval_of 9 | |
| category_theory.endomorphisms.single_e 9 | |
| category_theory.exact_seq.of_op 9 | |
| category_theory.is_snake_input.aux_simp 9 | |
| CompHausFiltPseuNormGrp₁.rescale_map 9 | |
| CompHausFiltPseuNormGrp.rescale_map 9 | |
| CompHausFiltPseuNormGrpWithTinv.has_coe_to_sort 9 | |
| ennreal.sub_pos 9 | |
| has_homology.comp_lift 9 | |
| homological_complex.biproduct.fst_f 9 | |
| invpoly.nsmul_apply 9 | |
| Lbar_le.Tinv_apply 9 | |
| PolyhedralLattice.rescale_proj 9 | |
| polyhedral_lattice.Tinv_apply 9 | |
| ProFiltPseuNormGrp.has_coe_to_sort 9 | |
| ProFiltPseuNormGrpWithTinv₁.rescale_map 9 | |
| Profinite.Radon_CompHaus_cone 9 | |
| Profinite.Radon_LC_comparison_component_equiv_aux 9 | |
| Profinite.Radon_LC_CompHaus_functor 9 | |
| Profinite.weak_dual_C_to_LC 9 | |
| summable.prod_nat 9 | |
| category_theory.short_exact_sequence.exact_inl_snd 10 | |
| category_theory.short_exact_sequence.hom_inj 10 | |
| CLCTinv.ι_range 10 | |
| Condensed.tensor_eval_iso 10 | |
| Condensed.tensor_iso 10 | |
| functor.map_unop 10 | |
| homological_complex.biprod.map_desc 10 | |
| homological_complex.category_theory.limits.has_binary_biproducts 10 | |
| product_iso_biproduct_spec 10 | |
| Profinite.Radon_functor 10 | |
| Profinite.to_normed_free_pfpng 10 | |
| reorder 10 | |
| SemiNormedGroup.LCC_obj_map 10 | |
| theta.aux_y 10 | |
| bicartesian.quatro_cons 11 | |
| bounded_derived_category.mk_iso 11 | |
| category_theory.functor.finite_product_aux.obj_equiv 11 | |
| category_theory.sheafification_adjunction_types 11 | |
| category_theory.short_exact_sequence.comp_fst 11 | |
| CLCFP.T_inv_eq 11 | |
| finset.le_ceil 11 | |
| Fintype.LaurentMeasure 11 | |
| has_homology.iso_ι 11 | |
| LCFP_rescale 11 | |
| LCFP.T_inv_eq 11 | |
| LC.T_inv_eq 11 | |
| nnrat.mul_le_iff_le_inv 11 | |
| Profinite.map_Radon_LC 11 | |
| Profinite.Radon_CompHaus_functor 11 | |
| short_complex.homology_functor_obj 11 | |
| add_monoid_hom.mk_from_pi 12 | |
| breen_deligne.FP2.Tinv_app 12 | |
| breen_deligne.package.main_lemma 12 | |
| category_theory.exact.mono_desc 12 | |
| category_theory.right_split 12 | |
| category_theory.short_exact_sequence.right_split 12 | |
| category_theory.split.right_split 12 | |
| ennreal.le_zero_iff 12 | |
| FiltrationPow.Tinv_app 12 | |
| pBanach.p_banach 12 | |
| Profinite.is_limit_Radon_LC_cone 12 | |
| theta.finite_sum 12 | |
| AddCommGroup.pi_π 13 | |
| breen_deligne.FP2.res_refl 13 | |
| category_theory.snake_diagram.o_le_o 13 | |
| chain_complex.exact_of_mono 13 | |
| CLCFP.res_refl 13 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits 13 | |
| CondensedSet.sigma_cone 13 | |
| Condensed.tensor_curry_eq 13 | |
| Filtration.pi_iso 13 | |
| Filtration.res_refl 13 | |
| laurent_measures.nnreal.has_continuous_smul 13 | |
| laurent_measures_ses.Φ 13 | |
| LCFP.res_refl 13 | |
| pBanach.has_continuous_smul 13 | |
| pBanach.lp_type.has_continuous_smul 13 | |
| Pow_Pow_X 13 | |
| Profinite.Radon_png_functor 13 | |
| sum_str.symm_symm 13 | |
| breen_deligne.FP2.res_app 14 | |
| category_theory.endomorphisms.add_f 14 | |
| category_theory.is_snake_input.mk_of_short_exact_sequence_hom 14 | |
| category_theory.snake_diagram.mk_of_short_exact_sequence_hom 14 | |
| category_theory.snake_input.mk_of_short_exact_sequence_hom 14 | |
| CLCFP.res_app 14 | |
| homological_complex.eval_functor_obj 14 | |
| Profinite.prod_iso 14 | |
| weak_dual.bdd_LC 14 | |
| bicartesian.quatro_cone 15 | |
| breen_deligne.FP2.res_comp_res 15 | |
| category_theory.exact_seq.arrow_congr 15 | |
| category_theory.nat_iso.unflip 15 | |
| category_theory.nat_trans.unflip 15 | |
| Condensed.AB5 15 | |
| LCFP.res_comp_res 15 | |
| Profinite.bdd_weak_dual 15 | |
| theta.summable_norm 15 | |
| category_theory.functor.pbool 16 | |
| category_theory.short_exact_sequence.quiver.hom.has_sub 16 | |
| category_theory.snake_diagram.o_fst 16 | |
| pBanach.lp_type.pseudo_metric_space 16 | |
| Pow_map 16 | |
| AddCommGroup.pi_lift 17 | |
| bounded_derived_category.lift_unique 17 | |
| category_theory.arrow.op_left 17 | |
| category_theory.biprod.is_biprod 17 | |
| category_theory.is_biprod 17 | |
| CompHausFiltPseuNormGrp₁.product.lift_unique 17 | |
| CompHausFiltPseuNormGrp.to_Condensed_map 17 | |
| Condensed.evaluation_obj 17 | |
| CondensedSet.evaluation_obj 17 | |
| finset.floor_le 17 | |
| homological_complex.category_theory.limits.has_colimits_of_shape 17 | |
| polyhedral_lattice_hom.coe_injective 17 | |
| ProFiltPseuNormGrpWithTinv₁.product.lift_unique 17 | |
| Profinite.map_Radon 17 | |
| Profinite.Radon_LC_comparison_component_equiv 17 | |
| category_theory.projective.homology.π'_ι 18 | |
| category_theory.short_exact_sequence.left_split 18 | |
| category_theory.snake_diagram.map_tac 18 | |
| category_theory.split.left_split 18 | |
| Condensed.coproduct_presentation 18 | |
| locally_constant.normed_space 18 | |
| pBanach.lp_type.has_coe_to_fun 18 | |
| Profinite.Radon_LC_cone 18 | |
| bounded_derived_category.int.category_theory.has_shift 19 | |
| category_theory.short_exact_sequence.quiver.hom.has_add 19 | |
| polyhedral_lattice_hom.to_fun_eq_coe 19 | |
| product_iso_biproduct 19 | |
| aux_thm69.int.summable_iff_on_nat 20 | |
| category_theory.functor.subsingleton.map_equiv 20 | |
| category_theory.short_exact_sequence.comp_snd 20 | |
| CompHausFiltPseuNormGrp₁.create_iso_from_level 20 | |
| continuous_map.comap_LC 20 | |
| pBanach.lp_type.has_nnnorm 20 | |
| ProFiltPseuNormGrpWithTinv₁.coe_sum 20 | |
| rescale.add_comm_monoid 20 | |
| as_normed_space'.has_norm 21 | |
| aux_thm69.mul_inv_fun 21 | |
| commsq.iso_hom_π 21 | |
| CompHausFiltPseuNormGrpWithTinv.concrete_category 21 | |
| invpoly.has_norm 21 | |
| pBanach.lp_type.has_norm 21 | |
| ProFiltPseuNormGrp.concrete_category 21 | |
| Condensed.category_theory.endomorphisms.category_theory.limits.has_finite_biproducts 22 | |
| locally_constant.metric_space 22 | |
| PolyhedralLattice.coe_of 22 | |
| ProFiltPseuNormGrp.coe_of 22 | |
| ProFiltPseuNormGrpWithTinv.coe_of 22 | |
| bounded_derived_category.forget.category_theory.faithful 23 | |
| category_theory.arrow.op_hom 23 | |
| category_theory.is_biprod.iso_biprod 23 | |
| category_theory.snake_diagram.decidable_eq 23 | |
| CompHausFiltPseuNormGrp₁.to_PNG₁.category_theory.faithful 23 | |
| ExtrDisc.sum.inl_desc 23 | |
| ExtrDisc.sum.inr_desc 23 | |
| homological_complex.next_functor 23 | |
| ProFiltPseuNormGrp₁.to_PNG₁.category_theory.faithful 23 | |
| breen_deligne.universal_map.eval_Pow' 24 | |
| has_homology.π_iso 24 | |
| homology_iso_predatum.fac_assoc 24 | |
| breen_deligne.basic_universal_map.eval_comp 25 | |
| breen_deligne.universal_map.eval_comp 25 | |
| homological_complex.prev_functor 25 | |
| category_theory.short_exact_sequence.Fst 26 | |
| category_theory.short_exact_sequence.Trd 26 | |
| CompHausFiltPseuNormGrp₁.product.lift_π_assoc 26 | |
| has_homology.lift_π_assoc 26 | |
| nnrat.inv_le 26 | |
| ProFiltPseuNormGrp₁.product.lift_π_assoc 26 | |
| ProFiltPseuNormGrp.coe_comp 26 | |
| ProFiltPseuNormGrpWithTinv₁.product.lift_π_assoc 26 | |
| ProFiltPseuNormGrpWithTinv.coe_comp 26 | |
| category_theory.simplicial_object.to_complex 27 | |
| Condensed.half_internal_hom 27 | |
| Condensed.tensor_uncurry 27 | |
| ExtrSheaf.half_internal_hom 27 | |
| ExtrSheafProd.half_internal_hom 27 | |
| ExtrSheafProd.tensor_uncurry 27 | |
| ExtrSheaf.tensor_uncurry 27 | |
| homological_complex.obj.category_theory.limits.preserves_finite_colimits 27 | |
| pBanach.lp_type.complete_space 27 | |
| two_step_resolution_ab 27 | |
| as_normed_space'.inhabited 28 | |
| bounded_homotopy_category.lift_comp 28 | |
| category_theory.composable_morphisms.hom.inhabited 28 | |
| category_theory.composable_morphisms.inhabited 28 | |
| combinatorial_lemma.recursion_data.inhabited 28 | |
| comphaus_filtered_pseudo_normed_group_hom.inhabited 28 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.inhabited 28 | |
| Lbar_bdd.inhabited 28 | |
| Lbar.inhabited 28 | |
| Lbar_le.inhabited 28 | |
| ProFiltPseuNormGrp.inhabited 28 | |
| ProFiltPseuNormGrpWithTinv.inhabited 28 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.inhabited 28 | |
| category_theory.arrow.op_right 29 | |
| category_theory.arrow.op_unop 29 | |
| category_theory.projective.homology.π_ι 29 | |
| Pow_mul 29 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.coe_inj 29 | |
| sum_str.op_unop 29 | |
| category_theory.short_exact_sequence.quiver.hom.has_neg 30 | |
| commsq.ι_eq 30 | |
| homological_complex.kernel_d 30 | |
| locally_constant.map_hom_comp 30 | |
| Profinite.Radon_LC_comparison 30 | |
| Profinite.Radon_LC_functor 30 | |
| Condensed.tensor_curry 31 | |
| ExtrSheafProd.tensor_curry 31 | |
| ExtrSheaf.tensor_curry 31 | |
| ExtrDisc.totally_disconnected_space 32 | |
| ProFiltPseuNormGrp.Top.of.totally_disconnected_space 32 | |
| ProFiltPseuNormGrpWithTinv₁.limit_cone_is_limit 32 | |
| ProFiltPseuNormGrpWithTinv.Top.of.totally_disconnected_space 32 | |
| topological_space.clopens.indicator_LC 32 | |
| breen_deligne.Mat 33 | |
| invpoly.sub_apply 33 | |
| category_theory.cosimplicial_object.to_cocomplex 34 | |
| CLCTinv.map_iso_inv 34 | |
| homological_complex.biprod.map_iso_inv 34 | |
| homology.lift_desc 35 | |
| bounded_derived_category.has_zero_object 36 | |
| category_theory.is_snake_input.to_kernel' 36 | |
| real_measures.neg_apply 36 | |
| bounded_derived_category_hom.ext_iff 37 | |
| category_theory.composable_morphisms.hom.ext_iff 37 | |
| category_theory.endomorphisms.hom.ext_iff 37 | |
| category_theory.short_exact_sequence.ext_iff 37 | |
| category_theory.short_exact_sequence.hom.ext_iff 37 | |
| category_theory.short_exact_sequence.Snd 37 | |
| commsq.ext_iff 37 | |
| Condensed.category_theory.endomorphisms.category_theory.enough_projectives 37 | |
| ExtrDisc.hom.ext_iff 37 | |
| ExtrSheafProd.hom.ext_iff 37 | |
| invpoly.invpoly.norm_nonneg 37 | |
| polyhedral_lattice_hom.ext_iff 37 | |
| short_complex.functor_category_equivalence 37 | |
| breen_deligne.data.sum_f 38 | |
| name_set.partition 39 | |
| discrete_quotient.equiv_bot 40 | |
| locally_constant.eq_sum 40 | |
| pBanach.lp_type 40 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.coe_to_add_monoid_hom 41 | |
| strict_pseudo_normed_group_hom.coe_to_add_monoid_hom 41 | |
| CLCFP.map_norm_noninc 42 | |
| ExtrDisc.t2_space 42 | |
| LCFP.map_norm_noninc 42 | |
| ProFiltPseuNormGrp.Top.of.t2_space 42 | |
| ProFiltPseuNormGrpWithTinv.Top.of.t2_space 42 | |
| bounded_derived_category.lift_map 43 | |
| Profinite.equalizer.lift_ι_assoc 43 | |
| category_theory.endomorphisms.has_limits 45 | |
| category_theory.is_snake_input.row_exact 45 | |
| Condensed.category_theory.limits.has_limits 45 | |
| discrete_quotient.fibre 45 | |
| PseuNormGrp₁.category_theory.limits.has_limits 45 | |
| Condensed.preserves_finite_limits 46 | |
| homological_complex.obj.category_theory.limits.preserves_finite_limits 46 | |
| invpoly.coe_nnnorm 46 | |
| category_theory.cosimplicial_object.cocomplex 48 | |
| comphaus_filtered_pseudo_normed_group_hom.map_sub 48 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.map_sub 48 | |
| polyhedral_lattice_hom.map_sub 48 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.map_sub 48 | |
| breen_deligne.data.complex_d 49 | |
| Condensed.eval_freeAb_iso 51 | |
| Filtration.res_comp 51 | |
| homological_complex.biproduct.inr_f 51 | |
| breen_deligne.data.system_obj 52 | |
| category_theory.short_exact_sequence.iso_of_components 52 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.mk'_apply 52 | |
| Condensed.eval_freeCond'_iso 52 | |
| homological_complex.biproduct.inl_f 53 | |
| homological_complex.kernel.ι_f 53 | |
| category_theory.endomorphisms.has_colimits 54 | |
| category_theory.limits.eq_to_hom_comp_image.ι_assoc 54 | |
| category_theory.limits.eq_to_hom_comp_kernel.ι_assoc 54 | |
| Condensed.category_theory.limits.has_colimits 54 | |
| CLCTinv.map_iso_hom 56 | |
| homological_complex.biprod.map_iso_hom 56 | |
| homotopy_category.unop_functor 56 | |
| nnrat.abs_eq 56 | |
| category_theory.projective.pseudoelement.id_apply 57 | |
| CompHausFiltPseuNormGrp₁.id_apply 57 | |
| CompHaus.id_apply 57 | |
| locally_constant.sum_apply 57 | |
| ProFiltPseuNormGrp₁.id_apply 57 | |
| PseuNormGrp₁.id_apply 57 | |
| strict_pseudo_normed_group_hom.id_apply 57 | |
| comphaus_filtered_pseudo_normed_group_hom.map_neg 58 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.map_neg 58 | |
| homological_complex.eval_functor.obj_X 58 | |
| SemiNormedGroup.truncate.obj_X 58 | |
| strict_pseudo_normed_group_hom.map_neg 58 | |
| Profinite.Radon_png 60 | |
| two_step_resolution 62 | |
| ExtrSheafProd.tensor_functor 64 | |
| Fintype.normed_free_pfpng 64 | |
| locally_constant.norm_zero 64 | |
| Profinite.normed_free_pfpng 64 | |
| thm95 64 | |
| short_complex.homology_functor.category_theory.limits.preserves_colimits_of_shape 66 | |
| CompHausFiltPseuNormGrp₁.as_lvl 67 | |
| locally_constant.uniform_space 68 | |
| short_complex.functor_category_equivalence.unit_iso 68 | |
| complex_shape.embedding.c_iff 69 | |
| ExtrDisc.compact_space 69 | |
| laurent_measures_bdd.map_apply 69 | |
| ProFiltPseuNormGrp.Top.of.compact_space 69 | |
| ProFiltPseuNormGrpWithTinv.Top.of.compact_space 69 | |
| category_theory.adjunction.whiskering_right 70 | |
| homological_complex.eval_functor.obj_d 70 | |
| punit.profinitely_filtered_pseudo_normed_group_with_Tinv 70 | |
| SemiNormedGroup.truncate.obj_d 70 | |
| invpoly.norm_add 72 | |
| laurent_measures.norm_add 72 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.lift_fun 74 | |
| breen_deligne.Mat.category_theory.small_category 75 | |
| has_homology.ι_desc_assoc 75 | |
| topological_space.clopens.indicator 77 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.map_zsmul 79 | |
| bounded_derived_category.forget.category_theory.full 81 | |
| category_theory.short_exact_sequence.category_theory.limits.has_zero_morphisms 81 | |
| PolyhedralLattice.category_theory.limits.has_zero_morphisms 81 | |
| oof 82 | |
| strict_comphaus_filtered_pseudo_normed_group_hom.map_sum 84 | |
| breen_deligne.universal_map.very_suitable.mul_right 85 | |
| category_theory.short_exact_sequence.quiver 85 | |
| comphaus_filtered_pseudo_normed_group_hom.zero_apply 85 | |
| category_theory.arrow.unop_op 91 | |
| sum_str.unop_op 91 | |
| category_theory.endomorphisms.preserves_limits 93 | |
| category_theory.snake_input 93 | |
| category_theory.snake.snake_input 93 | |
| CompHaus.category_theory.forget.category_theory.limits.preserves_limits 93 | |
| CompHausFiltPseuNormGrp₁.to_PNG₁.category_theory.limits.preserves_limits 93 | |
| CondensedSet.evaluation.category_theory.limits.preserves_limits 93 | |
| ProFiltPseuNormGrpWithTinv₁.obj.category_theory.limits.preserves_limits 93 | |
| pBanach.lp 97 | |
| Profinite.is_limit_Radon_LC_cone.linear_map 99 | |
| as_normed_space'.norm_def 100 | |
| cochain_complex.cons.d_comp_d 100 | |
| invpoly.norm_def 100 | |
| system_of_double_complexes.d_comp_d 100 | |
| category_theory.short_exact_sequence.left_split.splitting 106 | |
| category_theory.short_exact_sequence.right_split.splitting 106 | |
| category_theory.short_exact_sequence.splitting 106 | |
| bounded_derived_category.is_zero_zero 107 | |
| as_normed_space'.normed_add_comm_group 108 | |
| locally_constant.normed_add_comm_group 108 | |
| pBanach.lp_type.normed_add_comm_group 108 | |
| homological_complex.eval_functor 109 | |
| has_homology.iso_inv 119 | |
| sum_str.iso_inv 119 | |
| category_theory.endomorphisms.preserves_colimits 123 | |
| category_theory.preadditive.Pow.category_theory.limits.preserves_colimits 123 | |
| CompHausFiltPseuNormGrp₁.product.lift_π 124 | |
| has_homology.lift_π 124 | |
| ProFiltPseuNormGrpWithTinv₁.product.lift_π 124 | |
| short_complex.category_theory.limits.has_colimit 128 | |
| category_theory.short_exact_sequence.hom.sq2 129 | |
| homological_complex.biproduct.lift_f 131 | |
| aux_thm69.equiv.mul_inv 136 | |
| category_theory.short_exact_sequence.hom.sq1 136 | |
| category_theory.short_exact_sequence 137 | |
| main 140 | |
| ExtrDisc.empty.elim 141 | |
| system_of_complexes.completion 144 | |
| Profinite.is_limit_Radon_LC_cone.weak_dual 145 | |
| has_homology.lift_ι 146 | |
| Profinite.equalizer.lift_ι 146 | |
| polyhedral_lattice.profinitely_filtered_pseudo_normed_group 152 | |
| ProFiltPseuNormGrp.profinitely_filtered_pseudo_normed_group 152 | |
| punit.profinitely_filtered_pseudo_normed_group 152 | |
| system_of_double_complexes.d_d 152 | |
| category_theory.short_exact_sequence.functor_map 158 | |
| real_measures.functor_map 158 | |
| comphaus_filtered_pseudo_normed_group_hom.coe_mk 159 | |
| Lbar_le.coe_mk 159 | |
| strict_pseudo_normed_group_hom.coe_mk 159 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.has_zero 160 | |
| Lbar_bdd.has_zero 160 | |
| Lbar_le.has_zero 160 | |
| polyhedral_lattice_hom.has_zero 160 | |
| ProFiltPseuNormGrp.has_zero 160 | |
| ProFiltPseuNormGrpWithTinv.has_zero 160 | |
| real_measures.metric.closed_ball.has_zero 160 | |
| ProFiltPseuNormGrpWithTinv₁.product.fan 166 | |
| topological_space.clopens.singleton 170 | |
| ExtrDisc.topological_space 174 | |
| Profinite.Radon_LC.topological_space 174 | |
| Profinite.Radon.topological_space 174 | |
| type_pow_topology.topological_space 174 | |
| Profinite.is_limit_Radon_LC_cone.Radon_LC 177 | |
| Profinite.Radon_LC 177 | |
| aux_thm69.T.zero_le 182 | |
| ennreal.zero_le 182 | |
| nnreal.nat.digit.zero_le 182 | |
| category_theory.functor.homology_iso 184 | |
| continuous_map.comap 201 | |
| has_homology.ι_desc 201 | |
| weak_dual.comap 201 | |
| LCFP.obj.normed_with_aut 202 | |
| sum_str.iso_hom 206 | |
| category_theory.short_exact_sequence.f_nat 209 | |
| commsq.of_iso 209 | |
| AddCommGroup.of.category_theory.projective 215 | |
| CompHausFiltPseuNormGrp₁.lvl 216 | |
| laurent_measures.condensed 223 | |
| locally_constant.map_zero 228 | |
| as_normed_space'.add_comm_group 233 | |
| laurent_measures_ses.comphaus_filtered_pseudo_normed_group_hom.add_comm_group 233 | |
| Profinite.epi_free'_to_condensed_setup.obj.add_comm_group 233 | |
| bicartesian.biprod.matrix 235 | |
| system_of_complexes.is_quotient.surjective 238 | |
| bounded_homotopy_category.hom_ext 256 | |
| CompHausFiltPseuNormGrp₁.product.hom_ext 256 | |
| ExtrDisc.empty.hom_ext 256 | |
| ExtrDisc.sum.hom_ext 256 | |
| ProFiltPseuNormGrpWithTinv₁.product.hom_ext 256 | |
| Profinite.equalizer.hom_ext 256 | |
| Profinite.punit.hom_ext 256 | |
| homological_complex.cone.map_id 260 | |
| laurent_measures_bdd.map_id 260 | |
| SemiNormedGroup.equalizer.map_id 260 | |
| as_normed_space'.module 264 | |
| pBanach.lp_type.module 264 | |
| ExtrDisc.sum.inr 280 | |
| homological_complex.biproduct.inr 280 | |
| category_theory.snake_lemma.δ 292 | |
| system_of_complexes.is_bounded_exact.of_le 293 | |
| ExtrDisc.sum.inl 294 | |
| category_theory.right_split.short_exact 298 | |
| category_theory.split.short_exact 298 | |
| comphaus_filtered_pseudo_normed_group_hom.bound_by.zsmul 310 | |
| pBanach.lp_type.triangle 312 | |
| homology_iso_datum.map_iso 322 | |
| homology_iso_predatum.map_iso 322 | |
| ExtrSheafProd.evaluation 328 | |
| laurent_measures.profinite 328 | |
| thm95''.profinite 328 | |
| category_theory.functor.pbool.fintype 344 | |
| ProFiltPseuNormGrp 346 | |
| weak_dual.bdd 349 | |
| bounded_derived_category.forget 354 | |
| Profinite.Radon 357 | |
| ExtrDisc.empty 388 | |
| CompHaus.comp_apply 422 | |
| CompHausFiltPseuNormGrp₁.comp_apply 422 | |
| ProFiltPseuNormGrp₁.comp_apply 422 | |
| PseuNormGrp₁.comp_apply 422 | |
| strict_pseudo_normed_group_hom.comp_apply 422 | |
| Profinite.bdd_weak_dual.comphaus_filtered_pseudo_normed_group 429 | |
| as_normed_space'.down 471 | |
| category_theory.snake_input.proj 471 | |
| Pow 495 | |
| ProFiltPseuNormGrpWithTinv₁.product.is_limit 502 | |
| homological_complex.biproduct.snd 511 | |
| bounded_derived_category.preadditive 605 | |
| breen_deligne.data.preadditive 605 | |
| category_theory.short_exact_sequence.category_theory.preadditive 605 | |
| ExtrSheafProd.preadditive 605 | |
| invpoly.summable 640 | |
| pBanach.lp_type.summable 640 | |
| comphaus_filtered_pseudo_normed_group_hom.bound_by.strict 657 | |
| PolyhedralLattice.rescale 666 | |
| ProFiltPseuNormGrpWithTinv₁.rescale 666 | |
| laurent_measures_bdd.map_comp 681 | |
| sum_str.unop 681 | |
| category_theory.functor.single 696 | |
| category_theory.short_exact_sequence.split 725 | |
| category_theory.short_exact_sequence.splitting.split 725 | |
| homology_iso_datum.change.η.category_theory.is_iso 775 | |
| cochain_complex.cons.shape 777 | |
| aux_thm69.R 800 | |
| cochain_complex.imker.is_iso_cokernel.desc 833 | |
| ExtrDisc.sum.desc 833 | |
| homological_complex.biproduct.desc 833 | |
| bounded_derived_category.Ext 836 | |
| category_theory.exact_seq.congr 872 | |
| commsq.bicartesian.congr 872 | |
| system_of_complexes.congr 872 | |
| system_of_double_complexes.congr 872 | |
| bounded_derived_category.additive 879 | |
| thm95.rescale_functor'.additive 879 | |
| category_theory.projective.f.category_theory.epi 939 | |
| category_theory.projective.snd.category_theory.epi 939 | |
| category_theory.splitting.retraction.category_theory.epi 939 | |
| homological_complex.boundaries_map.category_theory.epi 939 | |
| homological_complex.f.category_theory.epi 939 | |
| PolyhedralLattice.Cech_conerve.π_hom.category_theory.epi 939 | |
| add_monoid_hom.pow 1059 | |
| ProFiltPseuNormGrpWithTinv₁.product 1071 | |
| cochain_complex.cons 1074 | |
| cochain_complex.hom.cons 1074 | |
| Profinite.bdd_weak_dual.pseudo_normed_group 1095 | |
| category_theory.endomorphisms.functor.free 1311 | |
| cochain_complex.hom.cons.comm 1372 | |
| bounded_derived_category.cone 1622 | |
| has_lt.lt.fact 1674 | |
| comphaus_filtered_pseudo_normed_group_hom.bound_by.neg 1788 | |
| bounded_derived_category.lift 1836 | |
| CompHausFiltPseuNormGrp₁.level_jointly_reflects_limits.lift 1836 | |
| ProFiltPseuNormGrpWithTinv₁.product.lift 1836 | |
| Profinite.equalizer.lift 1836 | |
| pseudo_normed_group.prod 1854 | |
| pfpng_ctu.sub 1997 | |
| breen_deligne.basic_universal_map.eval 2040 | |
| breen_deligne.universal_map.eval 2040 | |
| category_theory.projective.homology.ι.category_theory.mono 2065 | |
| category_theory.splitting.section.category_theory.mono 2065 | |
| homology_iso_datum.ι.category_theory.mono 2065 | |
| homological_complex.kernel_subobject_cokernel.π 2100 | |
| ProFiltPseuNormGrpWithTinv₁.product.π 2100 | |
| homological_complex.kernel 2324 | |
| bounded_derived_category_hom.ext 2753 | |
| category_theory.short_exact_sequence.ext 2753 | |
| category_theory.short_exact_sequence.hom.ext 2753 | |
| commsq.ext 2753 | |
| ExtrDisc.sum 3002 | |
| real_measures.continuous.sum 3002 | |
| Filtration.res 3154 | |
| homological_complex.kernel.ι 3188 | |
| category_theory.simplicial_object.augmented.complex 3368 | |
| category_theory.simplicial_object.complex 3368 | |
| category_theory.short_exact_sequence.functor 3467 | |
| category_theory.short_exact_sequence.id 3648 | |
| comphaus_filtered_pseudo_normed_group_hom.bound_by.id 3648 | |
| rescale_constants.one 3835 | |
| category_theory.split.exact 4357 | |
| homological_complex.eval_functor.obj 4414 | |
| short_complex.functor_category_equivalence.unit_iso.obj 4414 | |
| bounded_derived_category.category_theory.category 4541 | |
| category_theory.short_exact_sequence.category_theory.category 4541 | |
| category_theory.snake_input.category_theory.category 4541 | |
| bounded_derived_category.zero 4593 | |
| aux_thm69.T 4915 | |
| CLCFP.T 4915 | |
| LCFP.T 4915 | |
| as_normed_space'.up 5219 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.inv_of_equiv_of_strict.apply 5497 | |
| comphaus_filtered_pseudo_normed_group_with_Tinv_hom.inv_of_equiv_of_strict_symm.apply 5497 | |
| ProFiltPseuNormGrpWithTinv.iso_of_equiv_of_strict.apply 5497 | |
| ProFiltPseuNormGrpWithTinv.iso_of_equiv_of_strict_symm.apply 5497 | |
| cochain_complex.cons.X 5708 | |
| category_theory.arrow.op 6278 | |
| category_theory.exact_seq.op 6278 | |
| sum_str.op 6278 | |
| bounded_derived_category.of 8489 | |
| ExtrDisc.of 8489 | |
| ProFiltPseuNormGrp.of 8489 | |
| category_theory.endomorphisms.free.map 8513 | |
| category_theory.split.map 8513 | |
| category_theory.short_exact_sequence.hom 9984 | |
| category_theory.short_exact_sequence.comp 11642 | |
| theta.y 31403 | |
| cochain_complex.cons.d 52655 | |
| cochain_complex.hom.cons.f 56608 | |
| bounded_homotopy_category.e 157236 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment