isUniformInducing_extension

Stream: Is there code for X?

[Yakov Pechersky]

Is it the case that the docs#UniformSpace.Completion.extension is uniform inducing if it is an extension of a uniform inducing (and dense inducing) function?

In proving that (WithVal v).Completion ≃ᵤ ℚ_[p] for v : Valuation ℚ ℤᵐ⁰, I have an existing (WithVal v).Completion ≃+* ℚ_[p] (#27696). A shortcut to proving this is docs#Equiv.toUniformEquivOfIsUniformInducing. To use it, I'd need to show that my ring equiv is uniform inducing.

The ring equiv is defined via Completion.extensionHom f hf where f : WithVal v →+* ℚ_[p]. I know that IsUniformInducing f and IsDenseInducing f. Having the IsUniformInducing (Completion.extension f hf) would golf the UniformEquiv construction.

Here's the underlying topology question

import Mathlib

variable {X Y : Type*} [UniformSpace X] [UniformSpace Y] [CompleteSpace Y] {f : X → Y}

open UniformSpace

lemma foo (h : IsUniformInducing f) (h' : IsDenseInducing f) :
    IsUniformInducing (Completion.extension f) := by
  sorry

[Aaron Liu]

I think you need [T0Space Y]

[Aaron Liu]

(this is equivalent to [T1Space Y], [T2Space Y], [T3Space Y], and [T35Space Y])

[Aaron Liu]

actually maybe you don't need it

[Yakov Pechersky]

T0Space gives access to induction over Completion X and using Completion.extension_coe h.uniformContinuous, yes.

[Aaron Liu]

I have a proof of this now

[Aaron Liu]

the signature is

theorem foo.{u_1, u_2} : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace.{u_1} X] [inst_1 : UniformSpace.{u_2} Y]
  [@CompleteSpace.{u_2} Y inst_1] {f : X → Y},
  @IsUniformInducing.{u_1, u_2} X Y inst inst_1 f →
    @IsDenseInducing.{u_1, u_2} X Y (@UniformSpace.toTopologicalSpace.{u_1} X inst)
        (@UniformSpace.toTopologicalSpace.{u_2} Y inst_1) f →
      @IsUniformInducing.{u_1, u_2} (@UniformSpace.Completion.{u_1} X inst) Y
        (@UniformSpace.Completion.uniformSpace.{u_1} X inst) inst_1
        (@UniformSpace.Completion.extension.{u_1, u_2} X inst Y inst_1 f)

[Aaron Liu]

unfortunately for the proof to work you'll have to checkout
commit c1d42b9167691c46d300e83a369aaa4d78ddfb06

[Aaron Liu]

import Mathlib.Topology.UniformSpace.Completion

open Filter

theorem IsDenseInducing.tendsto_extend {α β γ : Type*} [TopologicalSpace α] [TopologicalSpace β]
    {i : α → β} [TopologicalSpace γ] (di : IsDenseInducing i) {f : α → γ}
    (a : α) (hf : ContinuousAt f a) : Tendsto f (nhds a) (nhds (di.extend f (i a))) := by
  rw [IsDenseInducing.extend, ← di.nhds_eq_comap]
  exact @Classical.epsilon_spec γ (fun x => map f (nhds a) ≤ nhds x) ⟨f a, hf.tendsto⟩

theorem UniformSpace.Completion.inseparable_extension_coe {X Y : Type*}
    [UniformSpace X] [UniformSpace Y] {f : X → Y} (hf : UniformContinuous f) (x : X) :
    Inseparable (Completion.extension f x) (f x) := by
  rw [Completion.extension, AbstractCompletion.extend_def _ hf]
  refine tendsto_nhds_unique_inseparable ?_ (hf.continuous.tendsto x)
  apply @IsDenseInducing.tendsto_extend _ _ _ _ cPkg.uniformStruct.toTopologicalSpace
  exact hf.continuous.continuousAt

variable {X Y : Type*} [UniformSpace X] [UniformSpace Y] [CompleteSpace Y] {f : X → Y}

open UniformSpace

lemma foo (h : IsUniformInducing f) (h' : IsDenseInducing f) :
    IsUniformInducing (Completion.extension f) := by
  let k : AbstractCompletion X := {
    space := SeparationQuotient Y
    coe := SeparationQuotient.mk ∘ f
    uniformStruct := inferInstance
    complete := inferInstance
    dense := SeparationQuotient.surjective_mk.denseRange.comp
      h'.dense SeparationQuotient.continuous_mk
    separation := inferInstance
    isUniformInducing := SeparationQuotient.isUniformInducing_mk.comp h
  }
  let l : AbstractCompletion X := { UniformSpace.Completion.cPkg with space := Completion X}
  let equiv := k.compareEquiv l
  apply SeparationQuotient.isUniformInducing_mk.isUniformInducing_comp_iff.1
  apply equiv.isUniformInducing.isUniformInducing_comp_iff.1
  have he : SeparationQuotient.mk ∘ Completion.extension f = equiv.symm :=
    (Completion.extension_unique
      (SeparationQuotient.isUniformInducing_mk.uniformContinuous.comp h.uniformContinuous)
      (SeparationQuotient.isUniformInducing_mk.uniformContinuous.comp
        Completion.uniformContinuous_extension)
      (fun x => SeparationQuotient.mk_eq_mk.2 <|
        (Completion.inseparable_extension_coe h.uniformContinuous x).symm)).symm
  rw [he, equiv.self_comp_symm]
  exact IsUniformInducing.id

[Aaron Liu]

If you don't want to checkout
commit c1d42b9167691c46d300e83a369aaa4d78ddfb06
then you can modify it to be universe monomorphic and everything still works hopefully

[Yakov Pechersky]

Thanks! Generalized, and avoids the universe issues: #27790.

[Aaron Liu]

Yakov Pechersky said:

Thanks! Generalized, and avoids the universe issues: #27790.

It's actually not generalized since you added [T2Space β]

[Aaron Liu]

or maybe it is I can't really tell

[Aaron Liu]

oh it does turn out to be more general but you can also remove the [T2Space β] assumption to get a doubly-generalized theorem

[Aaron Liu]

for some reason people just really like to be evil

[Yakov Pechersky]

Will you please contribute how the T2Space removal works?

[Aaron Liu]

First observe that in a uniform space T2Space is equivalent to T0Space. Then observe that the statement is not evil. Conclude that T0Space as an assumption is not necessary.

[Aaron Liu]

Yakov Pechersky said:

Will you please contribute how the T2Space removal works?

I put a comment on the PR

[Aaron Liu]

I was able to remove (h' : DenseRange f)

theorem continuous_rangeFactoriztion_iff {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    {f : α → β} : Continuous (Set.rangeFactorization f) ↔ Continuous f :=
  Topology.IsInducing.subtypeVal.continuous_iff

theorem Continuous.rangeFactoriztion {α β : Type*} [UniformSpace α] [UniformSpace β]
    {f : α → β} (hf : Continuous f) : Continuous (Set.rangeFactorization f) :=
  continuous_rangeFactoriztion_iff.2 hf

theorem isUniformInducing_rangeFactoriztion_iff {α β : Type*} [UniformSpace α] [UniformSpace β]
    {f : α → β} : IsUniformInducing (Set.rangeFactorization f) ↔ IsUniformInducing f :=
  (isUniformInducing_val (range f)).isUniformInducing_comp_iff.symm

theorem IsUniformInducing.rangeFactoriztion {α β : Type*} [UniformSpace α] [UniformSpace β]
    {f : α → β} (hf : IsUniformInducing f) :
    IsUniformInducing (Set.rangeFactorization f) :=
  isUniformInducing_rangeFactoriztion_iff.2 hf

theorem isUniformInducing_inclusion {α : Type*} [UniformSpace α] {s t : Set α} (hst : s ⊆ t) :
    IsUniformInducing (Set.inclusion hst) :=
  (isUniformInducing_val t).isUniformInducing_comp_iff.1 (isUniformInducing_val s)

theorem isUniformEmbedding_inclusion {α : Type*} [UniformSpace α] {s t : Set α} (hst : s ⊆ t) :
    IsUniformEmbedding (Set.inclusion hst) :=
  ⟨isUniformInducing_inclusion hst, Set.inclusion_injective hst⟩

theorem denseRange_inclusion_iff {α : Type*} [TopologicalSpace α] {s t : Set α} (hst : s ⊆ t) :
    DenseRange (Set.inclusion hst) ↔ t ⊆ closure s := by
  rw [DenseRange, Subtype.dense_iff, ← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]

lemma IsDenseInducing.isUniformInducing_extend {α β γ : Type*}
    [UniformSpace α] [UniformSpace β] [UniformSpace γ]
    [CompleteSpace β] [CompleteSpace γ] {i : α → β} {f : α → γ}
    (hid : IsDenseInducing i) (hi : IsUniformInducing i) (h : IsUniformInducing f) :
    IsUniformInducing (hid.extend f) := by
  have : CompleteSpace (closure (range (SeparationQuotient.mk ∘ f))) :=
    isClosed_closure.isComplete.completeSpace_coe
  let ff : α → closure (range (SeparationQuotient.mk ∘ f)) :=
    Set.inclusion subset_closure ∘ Set.rangeFactorization (SeparationQuotient.mk ∘ f)
  have hgu : IsUniformInducing ff :=
    (isUniformInducing_inclusion subset_closure).comp
      (SeparationQuotient.isUniformInducing_mk.comp h).rangeFactoriztion
  have hgd : DenseRange ff :=
    ((denseRange_inclusion_iff subset_closure).2 subset_rfl).comp
      Set.surjective_onto_range.denseRange (continuous_inclusion subset_closure)
  have hg : IsDenseInducing ff := hgu.isDenseInducing hgd
  let fwd := hid.extend ff
  have hfwd : UniformContinuous fwd :=
    (uniformContinuous_uniformly_extend hi hid.dense hgu.uniformContinuous)
  have hg' : UniformContinuous (hg.extend i) :=
    uniformContinuous_uniformly_extend hgu hgd hi.uniformContinuous
  have key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk := by
    ext x
    induction x using isClosed_property hid.dense
    · exact isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous)
        SeparationQuotient.continuous_mk
    · simpa [fwd, hid.extend_eq hgu.uniformContinuous.continuous]
        using hg.inseparable_extend hi.uniformContinuous.continuous.continuousAt
  have hfu : IsUniformInducing fwd := by
    refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_
    rw [Function.comp_assoc, key]
    exact SeparationQuotient.isUniformInducing_mk
  have hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆
      closure (range (SeparationQuotient.mk ∘ f)) := by
    convert (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense
    rw [← Set.range_comp]
    apply congrArg range
    funext x
    simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt).symm
  suffices Subtype.val ∘ fwd = SeparationQuotient.mk ∘ hid.extend f by
    rw [← SeparationQuotient.isUniformInducing_mk.isUniformInducing_comp_iff, ← this]
    exact (isUniformInducing_val (closure (range (SeparationQuotient.mk ∘ f)))).comp hfu
  change Subtype.val ∘ fwd =
    Subtype.val ∘ Set.inclusion hrr ∘ Set.rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)
  apply congrArg (Function.comp Subtype.val)
  refine hid.extend_unique ?_ ?_
  · simp [ff, hid.inseparable_extend h.uniformContinuous.continuous.continuousAt]
  · exact (continuous_inclusion hrr).comp
      (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
        h.uniformContinuous).continuous).rangeFactoriztion

[Yakov Pechersky]

Makes sense! Would you like to commit it or should I?

[Aaron Liu]

you commit it since I don't have push access to your branch (the downside of PRs from forks)