RootsOfUnityCharacterCriterion.lean

theorem bijective_compLeft_of_coefficient_equiv
    {G H A B : Type*} [Group G] [Group H] [CommGroup A] [CommGroup B]
    [TopologicalSpace G] [TopologicalSpace H]
    [TopologicalSpace A] [TopologicalSpace B]
    [IsTopologicalGroup A] [IsTopologicalGroup B]
    (f : G →ₜ* H) (e : A ≃ₜ* B)
    (h : Function.Bijective (f.compLeft A)) : Function.Bijective (f.compLeft B)

def equivOfBijectiveRootsOfUnityPullback
    (K : Type*) [Field K] [IsSepClosed K] [CharZero K]
    {G H : Type*} [CommGroup G] [CommGroup H]
    [TopologicalSpace G] [TopologicalSpace H]
    [IsTopologicalGroup G] [IsTopologicalGroup H]
    [CompactSpace G] [CompactSpace H]
    [TotallyDisconnectedSpace G] [TotallyDisconnectedSpace H]
    (f : G →ₜ* H)
    (hf : ∀ n : ℕ+, let _ : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥;
      let _ : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩;
      Function.Bijective (f.compLeft (rootsOfUnity (n : ℕ) K))) : G ≃ₜ* H := by
  apply equivOfBijectiveFiniteCharacterPullback f
  intro A hA
  have : IsCyclic A := isCyclic_of_injective_ringHom (Circle.coeHom.comp A.subtype)
    (Circle.coe_injective.comp Subtype.val_injective)
  let n : ℕ+ := ⟨Nat.card A, Nat.card_pos⟩
  let _ : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  let _ : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  let e : rootsOfUnity (n : ℕ) K ≃* A :=
    mulEquivOfCyclicCardEq (HasEnoughRootsOfUnity.natCard_rootsOfUnity K (n : ℕ))
  let eTop : rootsOfUnity (n : ℕ) K ≃ₜ* A :=
    { toMulEquiv := e
      continuous_toFun := continuous_of_discreteTopology
      continuous_invFun := continuous_of_discreteTopology }
  exact bijective_compLeft_of_coefficient_equiv f eTop (hf n)