equiv_of_functor

Stream: general

[Kevin Buzzard]

What am I rediscovering here:

import data.equiv.basic

variables {α β : Type} {P : α → β} {T : α → Type}

def f {x y : α} (h : P x = P y) : T x → T y := sorry

lemma f.id {x : α} (r : T x) : f (rfl : P x = P x) r = r := sorry

lemma f.comp {x y z : α} (hxy : P x = P y) (hyz : P y = P z)
  (r : T x) : f hyz (f hxy r) = f (hyz ▸ hxy : P x = P z) r := sorry

def T.equiv {x y : α} (h : P x = P y) : T x ≃ T y :=
{ to_fun := f h,
  inv_fun := f h.symm,
  left_inv := λ r, by rw f.comp h h.symm; exact f.id r,
  right_inv := λ r, by rw f.comp h.symm h; exact f.id r
}

and is T.equiv in mathlib in some form? Any way of making alpha into a groupoid such that f becomes a functor makes f send isomorphisms to equivs. Or something.

[Kevin Buzzard]

Oh I've just found another one, in localization.lean

[Kevin Buzzard]

def map (hf : injective f) : fraction_ring A → fraction_ring B :=
localization.map f $ λ s h,
  by rw [mem_non_zero_divisors_iff_ne_zero, ← map_zero f, ne.def, hf.eq_iff];
    exact mem_non_zero_divisors_iff_ne_zero.1 h

An injective ring map f : A -> B gives us a map fraction_ring A → fraction_ring B. I need that if f is an equiv then so is map f _. The natural way of proving it is to prove map.id and map.comp

[Kevin Buzzard]

and then invoke some general fact about equivs

[Kevin Buzzard]

@[simp] lemma map_id : map id (λ s (hs : s ∈ S), hs) = id :=
localization.funext _ _ $ map_coe _ _

lemma map_comp_map {γ : Type*} [comm_ring γ]  (hf : ∀ s ∈ S, f s ∈ T) (U : set γ)
  [is_submonoid U] (g : β → γ) [is_ring_hom g] (hg : ∀ t ∈ T, g t ∈ U) :
  map g hg ∘ map f hf = map (λ x, g (f x)) (λ s hs, hg _ (hf _ hs)) :=
localization.funext _ _ $ by simp

lemma map_map {γ : Type*} [comm_ring γ]  (hf : ∀ s ∈ S, f s ∈ T) (U : set γ)
  [is_submonoid U] (g : β → γ) [is_ring_hom g] (hg : ∀ t ∈ T, g t ∈ U) (x) :
  map g hg (map f hf x) = map (λ x, g (f x)) (λ s hs, hg _ (hf _ hs)) x :=
congr_fun (map_comp_map _ _ _ _ _) x

def equiv_of_equiv (h₁ : α ≃r β) (h₂ : h₁.to_equiv '' S = T) :
  localization α S ≃r localization β T :=
{ to_fun := map h₁.to_equiv $ λ s hs, by {rw ← h₂, simp [hs]},
  inv_fun := map h₁.symm.to_equiv $ λ t ht,
    by simp [equiv.image_eq_preimage, set.preimage, set.ext_iff, *] at *,
  left_inv := λ _, by simp only [map_map, ring_equiv.to_equiv_symm_apply,
    equiv.symm_apply_apply]; erw map_id; refl,
  right_inv := λ _, by simp only [map_map, ring_equiv.to_equiv_symm_apply,
    equiv.apply_symm_apply]; erw map_id; refl,
  hom := map.is_ring_hom _ _ }

All of that from localization.lean. It's somehow the same argument as mine above.