R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
⊢ IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S → IsLocalization M S
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
refine' ⟨fun _ => isLocalization_of_base_ringEquiv M S h, _⟩
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ IsLocalization M S
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
⊢ IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S → IsLocalization M S
intro H
case h.e'_3
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ M = Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.symm h)) (Submonoid.map (RingEquiv.toMonoidHom h) M)

case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ inst✝¹ = RingHom.toAlgebra (RingHom.comp (algebraMap P S) (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.symm h))))
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ IsLocalization M S
convert isLocalization_of_base_ringEquiv (Submonoid.map (RingEquiv.toMonoidHom h) M) S h.symm
case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ inst✝¹ =
    RingHom.toAlgebra
      (RingHom.comp (algebraMap R S)
        (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm h))
          (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.symm h)))))
case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ inst✝¹ = RingHom.toAlgebra (RingHom.comp (algebraMap P S) (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.symm h))))
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc]
case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ inst✝¹ = RingHom.toAlgebra (algebraMap R S)
case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ inst✝¹ =
    RingHom.toAlgebra
      (RingHom.comp (algebraMap R S)
        (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm h))
          (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.symm h)))))
simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom]
case h.e'_6.h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ ∀ (r : R), ↑(algebraMap R S) r = ↑(algebraMap R S) r
case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ inst✝¹ = RingHom.toAlgebra (algebraMap R S)
apply Algebra.algebra_ext
case h.e'_6.h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
r : R
⊢ ↑(algebraMap R S) r = ↑(algebraMap R S) r
case h.e'_6.h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ ∀ (r : R), ↑(algebraMap R S) r = ↑(algebraMap R S) r
intro r
no goals
case h.e'_6.h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
r : R
⊢ ↑(algebraMap R S) r = ↑(algebraMap R S) r
rw [RingHom.algebraMap_toAlgebra]
case h.e'_3.hf
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ Injective ↑(MulEquiv.toMonoidHom (MulEquiv.symm (RingEquiv.toMulEquiv (RingEquiv.symm h))))
case h.e'_3
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ M = Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.symm h)) (Submonoid.map (RingEquiv.toMonoidHom h) M)
erw [Submonoid.map_equiv_eq_comap_symm, Submonoid.comap_map_eq_of_injective]
no goals
case h.e'_3.hf
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_2
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) (RingEquiv.toRingHom (RingEquiv.symm h)))
H : IsLocalization (Submonoid.map (RingEquiv.toMonoidHom h) M) S
⊢ Injective ↑(MulEquiv.toMonoidHom (MulEquiv.symm (RingEquiv.toMulEquiv (RingEquiv.symm h))))
exact h.toEquiv.injective