Commit 2025-12-22 22:40 e4039565

View on Github →

feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

added theorem Set.pairwise_disjoint_smul_iff

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added theorem Set.nonempty_image_mulLeft_inv_inter_iff

added theorem Set.nonempty_image_mulRight_inv_inter_iff

Modified Mathlib/Algebra/Group/Submonoid/MulAction.lean

Modified Mathlib/Algebra/Regular/SMul.lean

added theorem IsSMulRegular.natAbs_iff

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

added theorem Circle.isAddQuotientCoveringMap_exp

added theorem Circle.isCoveringMap_exp

modified theorem isLocalHomeomorph_circleExp

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/Tactic/Translate/ToAdditive.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem IsUnit.isQuotientMap_nsmul

added theorem IsUnit.isQuotientMap_smul

added theorem IsUnit.isQuotientMap_zsmul

added theorem ProperlyDiscontinuousSMul.exists_nhds_disjoint_image

added theorem ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self

added theorem ProperlyDiscontinuousSMul.finite_stabilizer'

added theorem ProperlyDiscontinuousSMul.finite_stabilizer

added theorem isHomeomorph_smul

added theorem isHomeomorph_smul₀

Modified Mathlib/Topology/Algebra/Group/Pointwise.lean

added theorem IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty

added theorem IsDiscrete.exists_nhds_eq_one_of_image_mulRight_inter_nonempty

Created Mathlib/Topology/Covering/AddCircle.lean

added theorem AddCircle.isAddQuotientCoveringMap_coe

added theorem AddCircle.isAddQuotientCoveringMap_nsmul

added theorem AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero

added theorem AddCircle.isAddQuotientCoveringMap_zsmul

added theorem AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero

added theorem AddCircle.isCoveringMap_coe

added theorem AddCircle.isLocalHomeomorph_coe

Modified Mathlib/Topology/Covering/Basic.lean

Created Mathlib/Topology/Covering/Quotient.lean

added structure IsAddQuotientCoveringMap

added theorem IsQuotientCoveringMap.homeomorph_comp

added theorem IsQuotientCoveringMap.homeomorph_comp_iff

added theorem IsQuotientCoveringMap.isCancelSMul

added theorem IsQuotientCoveringMap.isCoveringMap

added structure IsQuotientCoveringMap

added theorem Subgroup.isQuotientCoveringMap

added theorem Subgroup.isQuotientCoveringMap_of_comm

added theorem Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul

added theorem Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint

added theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom

added theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_properlyDiscontinuousSMul

added theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup

added theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp

added theorem isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul

added theorem isQuotientCoveringMap_iff_isCoveringMap_and

added theorem isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean

added theorem AddCircle.card_torsion_le_of_isSMulRegular

added theorem AddCircle.card_torsion_le_of_isSMulRegular_int

modified theorem AddCircle.finite_torsion

added theorem AddCircle.finite_torsion_of_isSMulRegular

added theorem AddCircle.finite_torsion_of_isSMulRegular_int

deleted theorem AddCircle.isLocalHomeomorph_coe

deleted theorem AddCircle.nsmul_eq_zero_iff

Modified Mathlib/Topology/Maps/Basic.lean

added theorem Topology.IsInducing.IsQuotientMap.of_comp_isQuotientMap

added theorem Topology.IsInducing.IsQuotientMap.of_comp_of_eq_coinduced