Commit 2025-04-10 05:07 778fc9f5

View on Github →

chore: split Topology.Category.Profinite.Nobeling (#23898) The base file is now called Topology.Category.Profinite.Nobeling.Basic, which is separately imported by three new files:

.Span for the good products span
.ZeroLimit for the zero and limit cases of the ordinal induction
.Successor for the successor case of the ordinal induction Then .Induction ties up these files to prove Nöbeling's theorem proper.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Topology/Category/Profinite/Nobeling.lean

deleted theorem Profinite.Nobeling.isClosedEmbedding

deleted def Profinite.Nobeling.ι

deleted def Profinite.NobelingProof.C'

deleted def Profinite.NobelingProof.C0

deleted theorem Profinite.NobelingProof.C0_projOrd

deleted def Profinite.NobelingProof.C1

deleted theorem Profinite.NobelingProof.C1_projOrd

deleted def Profinite.NobelingProof.CC'₀

deleted def Profinite.NobelingProof.CC'₁

deleted theorem Profinite.NobelingProof.CC_comp_zero

deleted theorem Profinite.NobelingProof.CC_exact

deleted def Profinite.NobelingProof.GoodProducts.Basis

deleted def Profinite.NobelingProof.GoodProducts.MaxProducts

deleted def Profinite.NobelingProof.GoodProducts.MaxToGood

deleted theorem Profinite.NobelingProof.GoodProducts.P0

deleted theorem Profinite.NobelingProof.GoodProducts.Plimit

deleted def Profinite.NobelingProof.GoodProducts.SumEval

deleted theorem Profinite.NobelingProof.GoodProducts.chain'_cons_of_lt

deleted def Profinite.NobelingProof.GoodProducts.equiv_range

deleted theorem Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval

deleted def Profinite.NobelingProof.GoodProducts.eval

deleted theorem Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval

deleted theorem Profinite.NobelingProof.GoodProducts.good_lt_maxProducts

deleted theorem Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts

deleted theorem Profinite.NobelingProof.GoodProducts.injective

deleted theorem Profinite.NobelingProof.GoodProducts.injective_sum_to

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependent

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependentAux

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependentEmpty

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependentSingleton

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum

deleted theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller

deleted theorem Profinite.NobelingProof.GoodProducts.maxTail_isGood

deleted theorem Profinite.NobelingProof.GoodProducts.maxToGood_injective

deleted theorem Profinite.NobelingProof.GoodProducts.max_eq_eval

deleted theorem Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply

deleted theorem Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail

deleted def Profinite.NobelingProof.GoodProducts.range

deleted def Profinite.NobelingProof.GoodProducts.range_equiv

deleted theorem Profinite.NobelingProof.GoodProducts.range_equiv_factorization

deleted def Profinite.NobelingProof.GoodProducts.range_equiv_smaller

deleted def Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun

deleted theorem Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective

deleted def Profinite.NobelingProof.GoodProducts.smaller

deleted theorem Profinite.NobelingProof.GoodProducts.smaller_factorization

deleted theorem Profinite.NobelingProof.GoodProducts.smaller_mono

deleted theorem Profinite.NobelingProof.GoodProducts.span

deleted theorem Profinite.NobelingProof.GoodProducts.spanFin

deleted theorem Profinite.NobelingProof.GoodProducts.span_iff_products

deleted theorem Profinite.NobelingProof.GoodProducts.span_sum

deleted theorem Profinite.NobelingProof.GoodProducts.square_commutes

deleted def Profinite.NobelingProof.GoodProducts.sum_equiv

deleted theorem Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim

deleted def Profinite.NobelingProof.GoodProducts.sum_to

deleted theorem Profinite.NobelingProof.GoodProducts.sum_to_range

deleted theorem Profinite.NobelingProof.GoodProducts.union

deleted theorem Profinite.NobelingProof.GoodProducts.union_succ

deleted def Profinite.NobelingProof.GoodProducts

deleted def Profinite.NobelingProof.Linear_CC'

deleted def Profinite.NobelingProof.Linear_CC'₀

deleted def Profinite.NobelingProof.Linear_CC'₁

deleted theorem Profinite.NobelingProof.Nobeling_aux

deleted def Profinite.NobelingProof.P

deleted def Profinite.NobelingProof.Products.Tail

deleted def Profinite.NobelingProof.Products.eval

deleted theorem Profinite.NobelingProof.Products.evalCons

deleted theorem Profinite.NobelingProof.Products.evalFacProp

deleted theorem Profinite.NobelingProof.Products.evalFacProps

deleted theorem Profinite.NobelingProof.Products.eval_eq

deleted theorem Profinite.NobelingProof.Products.eval_πs'

deleted theorem Profinite.NobelingProof.Products.eval_πs

deleted theorem Profinite.NobelingProof.Products.eval_πs_image'

deleted theorem Profinite.NobelingProof.Products.eval_πs_image

deleted theorem Profinite.NobelingProof.Products.head!_le_of_lt

deleted theorem Profinite.NobelingProof.Products.head_lt_ord_of_isGood

deleted def Profinite.NobelingProof.Products.isGood

deleted theorem Profinite.NobelingProof.Products.isGood_mono

deleted theorem Profinite.NobelingProof.Products.isGood_nil

deleted theorem Profinite.NobelingProof.Products.limitOrdinal

deleted theorem Profinite.NobelingProof.Products.lt_iff_lex_lt

deleted theorem Profinite.NobelingProof.Products.lt_nil_empty

deleted theorem Profinite.NobelingProof.Products.lt_ord_of_lt

deleted theorem Profinite.NobelingProof.Products.max_eq_eval

deleted theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail'

deleted theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail

deleted def Profinite.NobelingProof.Products.nil

deleted theorem Profinite.NobelingProof.Products.prop_of_isGood

deleted theorem Profinite.NobelingProof.Products.prop_of_isGood_of_contained

deleted theorem Profinite.NobelingProof.Products.rel_head!_of_mem

deleted theorem Profinite.NobelingProof.Products.span_nil_eq_top

deleted def Profinite.NobelingProof.Products

deleted def Profinite.NobelingProof.Proj

deleted def Profinite.NobelingProof.ProjRestrict

deleted def Profinite.NobelingProof.ProjRestricts

deleted def Profinite.NobelingProof.SwapTrue

deleted theorem Profinite.NobelingProof.coe_πs'

deleted theorem Profinite.NobelingProof.coe_πs

deleted def Profinite.NobelingProof.contained

deleted theorem Profinite.NobelingProof.contained_C'

deleted theorem Profinite.NobelingProof.contained_C1

deleted theorem Profinite.NobelingProof.contained_eq_proj

deleted theorem Profinite.NobelingProof.contained_proj

deleted theorem Profinite.NobelingProof.continuous_CC'₀

deleted theorem Profinite.NobelingProof.continuous_CC'₁

deleted theorem Profinite.NobelingProof.continuous_proj

deleted theorem Profinite.NobelingProof.continuous_projRestrict

deleted theorem Profinite.NobelingProof.continuous_projRestricts

deleted theorem Profinite.NobelingProof.continuous_swapTrue

deleted def Profinite.NobelingProof.e

deleted theorem Profinite.NobelingProof.e_mem_of_eq_true

deleted theorem Profinite.NobelingProof.eval_eq_πJ

deleted def Profinite.NobelingProof.factors

deleted theorem Profinite.NobelingProof.factors_prod_eq_basis

deleted theorem Profinite.NobelingProof.factors_prod_eq_basis_of_eq

deleted theorem Profinite.NobelingProof.factors_prod_eq_basis_of_ne

deleted theorem Profinite.NobelingProof.fin_comap_jointlySurjective

deleted theorem Profinite.NobelingProof.injective_πs'

deleted theorem Profinite.NobelingProof.injective_πs

deleted theorem Profinite.NobelingProof.isClosed_C'

deleted theorem Profinite.NobelingProof.isClosed_C0

deleted theorem Profinite.NobelingProof.isClosed_C1

deleted theorem Profinite.NobelingProof.isClosed_proj

deleted def Profinite.NobelingProof.iso_map

deleted theorem Profinite.NobelingProof.iso_map_bijective

deleted theorem Profinite.NobelingProof.list_prod_apply

deleted theorem Profinite.NobelingProof.mem_C'_eq_false

deleted theorem Profinite.NobelingProof.one_sub_e_mem_of_false

deleted def Profinite.NobelingProof.ord

deleted theorem Profinite.NobelingProof.ord_term

deleted theorem Profinite.NobelingProof.ord_term_aux

deleted theorem Profinite.NobelingProof.projRestricts_comp_projRestrict

deleted theorem Profinite.NobelingProof.projRestricts_eq_comp

deleted theorem Profinite.NobelingProof.projRestricts_eq_id

deleted theorem Profinite.NobelingProof.proj_comp_of_subset

deleted theorem Profinite.NobelingProof.proj_eq_of_subset

deleted theorem Profinite.NobelingProof.proj_eq_self

deleted theorem Profinite.NobelingProof.proj_prop_eq_self

deleted def Profinite.NobelingProof.spanCone

deleted def Profinite.NobelingProof.spanCone_isLimit

deleted theorem Profinite.NobelingProof.spanFinBasis.span

deleted def Profinite.NobelingProof.spanFinBasis

deleted def Profinite.NobelingProof.spanFunctor

deleted theorem Profinite.NobelingProof.succ_exact

deleted theorem Profinite.NobelingProof.succ_mono

deleted theorem Profinite.NobelingProof.surjective_projRestricts

deleted theorem Profinite.NobelingProof.swapTrue_eq_true

deleted theorem Profinite.NobelingProof.swapTrue_mem_C1

deleted def Profinite.NobelingProof.term

deleted theorem Profinite.NobelingProof.term_ord_aux

deleted theorem Profinite.NobelingProof.union_C0C1_eq

deleted def Profinite.NobelingProof.π

deleted def Profinite.NobelingProof.πJ

deleted def Profinite.NobelingProof.πs'

deleted def Profinite.NobelingProof.πs

Created Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean

added def Profinite.NobelingProof.GoodProducts.equiv_range

added theorem Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval

added def Profinite.NobelingProof.GoodProducts.eval

added theorem Profinite.NobelingProof.GoodProducts.injective

added theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range

added def Profinite.NobelingProof.GoodProducts.range

added theorem Profinite.NobelingProof.GoodProducts.span_iff_products

added def Profinite.NobelingProof.GoodProducts

added def Profinite.NobelingProof.P

added def Profinite.NobelingProof.Products.eval

added theorem Profinite.NobelingProof.Products.evalFacProp

added theorem Profinite.NobelingProof.Products.evalFacProps

added theorem Profinite.NobelingProof.Products.eval_eq

added theorem Profinite.NobelingProof.Products.eval_πs'

added theorem Profinite.NobelingProof.Products.eval_πs

added theorem Profinite.NobelingProof.Products.eval_πs_image'

added theorem Profinite.NobelingProof.Products.eval_πs_image

added theorem Profinite.NobelingProof.Products.head!_le_of_lt

added theorem Profinite.NobelingProof.Products.head_lt_ord_of_isGood

added def Profinite.NobelingProof.Products.isGood

added theorem Profinite.NobelingProof.Products.isGood_mono

added theorem Profinite.NobelingProof.Products.lt_iff_lex_lt

added theorem Profinite.NobelingProof.Products.lt_ord_of_lt

added theorem Profinite.NobelingProof.Products.prop_of_isGood

added theorem Profinite.NobelingProof.Products.prop_of_isGood_of_contained

added theorem Profinite.NobelingProof.Products.rel_head!_of_mem

added def Profinite.NobelingProof.Products

added def Profinite.NobelingProof.Proj

added def Profinite.NobelingProof.ProjRestrict

added def Profinite.NobelingProof.ProjRestricts

added theorem Profinite.NobelingProof.coe_πs'

added theorem Profinite.NobelingProof.coe_πs

added def Profinite.NobelingProof.contained

added theorem Profinite.NobelingProof.contained_eq_proj

added theorem Profinite.NobelingProof.contained_proj

added theorem Profinite.NobelingProof.continuous_proj

added theorem Profinite.NobelingProof.continuous_projRestrict

added theorem Profinite.NobelingProof.continuous_projRestricts

added def Profinite.NobelingProof.e

added theorem Profinite.NobelingProof.injective_πs'

added theorem Profinite.NobelingProof.injective_πs

added theorem Profinite.NobelingProof.isClosed_proj

added def Profinite.NobelingProof.iso_map

added theorem Profinite.NobelingProof.iso_map_bijective

added def Profinite.NobelingProof.ord

added theorem Profinite.NobelingProof.ord_term

added theorem Profinite.NobelingProof.ord_term_aux

added theorem Profinite.NobelingProof.projRestricts_comp_projRestrict

added theorem Profinite.NobelingProof.projRestricts_eq_comp

added theorem Profinite.NobelingProof.projRestricts_eq_id

added theorem Profinite.NobelingProof.proj_comp_of_subset

added theorem Profinite.NobelingProof.proj_eq_of_subset

added theorem Profinite.NobelingProof.proj_eq_self

added theorem Profinite.NobelingProof.proj_prop_eq_self

added def Profinite.NobelingProof.spanCone

added def Profinite.NobelingProof.spanCone_isLimit

added def Profinite.NobelingProof.spanFunctor

added theorem Profinite.NobelingProof.surjective_projRestricts

added def Profinite.NobelingProof.term

added theorem Profinite.NobelingProof.term_ord_aux

added def Profinite.NobelingProof.π

added def Profinite.NobelingProof.πs'

added def Profinite.NobelingProof.πs

Created Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean

added theorem Profinite.Nobeling.isClosedEmbedding

added def Profinite.Nobeling.ι

added def Profinite.NobelingProof.GoodProducts.Basis

added theorem Profinite.NobelingProof.GoodProducts.P0

added theorem Profinite.NobelingProof.GoodProducts.Plimit

added theorem Profinite.NobelingProof.GoodProducts.linearIndependent

added theorem Profinite.NobelingProof.GoodProducts.linearIndependentAux

added theorem Profinite.NobelingProof.Nobeling_aux

Created Mathlib/Topology/Category/Profinite/Nobeling/Span.lean

added theorem Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval

added theorem Profinite.NobelingProof.GoodProducts.span

added theorem Profinite.NobelingProof.GoodProducts.spanFin

added theorem Profinite.NobelingProof.e_mem_of_eq_true

added theorem Profinite.NobelingProof.eval_eq_πJ

added def Profinite.NobelingProof.factors

added theorem Profinite.NobelingProof.factors_prod_eq_basis

added theorem Profinite.NobelingProof.factors_prod_eq_basis_of_eq

added theorem Profinite.NobelingProof.factors_prod_eq_basis_of_ne

added theorem Profinite.NobelingProof.fin_comap_jointlySurjective

added theorem Profinite.NobelingProof.list_prod_apply

added theorem Profinite.NobelingProof.one_sub_e_mem_of_false

added theorem Profinite.NobelingProof.spanFinBasis.span

added def Profinite.NobelingProof.spanFinBasis

added def Profinite.NobelingProof.πJ

Created Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean

added def Profinite.NobelingProof.C'

added def Profinite.NobelingProof.C0

added theorem Profinite.NobelingProof.C0_projOrd

added def Profinite.NobelingProof.C1

added theorem Profinite.NobelingProof.C1_projOrd

added def Profinite.NobelingProof.CC'₀

added def Profinite.NobelingProof.CC'₁

added theorem Profinite.NobelingProof.CC_comp_zero

added theorem Profinite.NobelingProof.CC_exact

added def Profinite.NobelingProof.GoodProducts.MaxProducts

added def Profinite.NobelingProof.GoodProducts.MaxToGood

added def Profinite.NobelingProof.GoodProducts.SumEval

added theorem Profinite.NobelingProof.GoodProducts.chain'_cons_of_lt

added theorem Profinite.NobelingProof.GoodProducts.good_lt_maxProducts

added theorem Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts

added theorem Profinite.NobelingProof.GoodProducts.injective_sum_to

added theorem Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval

added theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum

added theorem Profinite.NobelingProof.GoodProducts.maxTail_isGood

added theorem Profinite.NobelingProof.GoodProducts.maxToGood_injective

added theorem Profinite.NobelingProof.GoodProducts.max_eq_eval

added theorem Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply

added theorem Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail

added theorem Profinite.NobelingProof.GoodProducts.span_sum

added theorem Profinite.NobelingProof.GoodProducts.square_commutes

added def Profinite.NobelingProof.GoodProducts.sum_equiv

added theorem Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim

added def Profinite.NobelingProof.GoodProducts.sum_to

added theorem Profinite.NobelingProof.GoodProducts.sum_to_range

added theorem Profinite.NobelingProof.GoodProducts.union_succ

added def Profinite.NobelingProof.Linear_CC'

added def Profinite.NobelingProof.Linear_CC'₀

added def Profinite.NobelingProof.Linear_CC'₁

added def Profinite.NobelingProof.Products.Tail

added theorem Profinite.NobelingProof.Products.evalCons

added theorem Profinite.NobelingProof.Products.max_eq_eval

added theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail'

added theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail

added def Profinite.NobelingProof.SwapTrue

added theorem Profinite.NobelingProof.contained_C'

added theorem Profinite.NobelingProof.contained_C1

added theorem Profinite.NobelingProof.continuous_CC'₀

added theorem Profinite.NobelingProof.continuous_CC'₁

added theorem Profinite.NobelingProof.continuous_swapTrue

added theorem Profinite.NobelingProof.isClosed_C'

added theorem Profinite.NobelingProof.isClosed_C0

added theorem Profinite.NobelingProof.isClosed_C1

added theorem Profinite.NobelingProof.mem_C'_eq_false

added theorem Profinite.NobelingProof.succ_exact

added theorem Profinite.NobelingProof.succ_mono

added theorem Profinite.NobelingProof.swapTrue_eq_true

added theorem Profinite.NobelingProof.swapTrue_mem_C1

added theorem Profinite.NobelingProof.union_C0C1_eq

Created Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean

added theorem Profinite.NobelingProof.GoodProducts.linearIndependentEmpty

added theorem Profinite.NobelingProof.GoodProducts.linearIndependentSingleton

added theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller

added theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller

added def Profinite.NobelingProof.GoodProducts.range_equiv

added theorem Profinite.NobelingProof.GoodProducts.range_equiv_factorization

added def Profinite.NobelingProof.GoodProducts.range_equiv_smaller

added def Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun

added theorem Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective

added def Profinite.NobelingProof.GoodProducts.smaller

added theorem Profinite.NobelingProof.GoodProducts.smaller_factorization

added theorem Profinite.NobelingProof.GoodProducts.smaller_mono

added theorem Profinite.NobelingProof.GoodProducts.union

added theorem Profinite.NobelingProof.Products.isGood_nil

added theorem Profinite.NobelingProof.Products.limitOrdinal

added theorem Profinite.NobelingProof.Products.lt_nil_empty

added def Profinite.NobelingProof.Products.nil

added theorem Profinite.NobelingProof.Products.span_nil_eq_top