internlm/Lean-Github huggingface dataset:
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ S₁ ⧸ comap e P →ₗ[R ⧸ p] S₂ ⧸ P
Tactic:
apply (config := {allowSynthFailures := true }) LinearMap.mk
Proof state after:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), ?toAddHom.toFun (m • x) = (RingHom.id (R ⧸ p)) m • ?toAddHom.toFun x

case toAddHom
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), ?toAddHom.toFun (m • x) = (RingHom.id (R ⧸ p)) m • ?toAddHom.toFun x

case toAddHom
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)
Tactic:
swap
Proof state after:
case toAddHom
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)

case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), ?toAddHom.toFun (m • x) = (RingHom.id (R ⧸ p)) m • ?toAddHom.toFun x
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
case toAddHom
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)
Tactic:
exact E.toLinearMap.toAddHom
Proof state after:
no goals
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), E.toLinearMap.toFun (m • x) = (RingHom.id (R ⧸ p)) m • E.toLinearMap.toFun x
Tactic:
intro r x
Proof state after:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E.toLinearMap.toFun (r • x) = (RingHom.id (R ⧸ p)) r • E.toLinearMap.toFun x
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E.toLinearMap.toFun (r • x) = (RingHom.id (R ⧸ p)) r • E.toLinearMap.toFun x
Tactic:
show E (_ * _) = _ * (E x)
Proof state after:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) r * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) r) * E x
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
case map_smul'
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) r * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) r) * E x
Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
Proof state after:
case map_smul'.intro
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
x : S₁ ⧸ comap e P
r : R
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) ((Quotient.mk p) r) * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) ((Quotient.mk p) r)) * E x
Theorem: Ideal.inertiaDeg_comap_eq
Proof state before:
case map_smul'.intro
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
x : S₁ ⧸ comap e P
r : R
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) ((Quotient.mk p) r) * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) ((Quotient.mk p) r)) * E x
Tactic:
simp only [Quotient.mk_comp_algebraMap, Quotient.lift_mk, _root_.map_mul, AlgEquiv.commutes,
  RingHomCompTriple.comp_apply]
Proof state after:
no goals
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ IsIntegrallyClosed S
Tactic:
let K := FractionRing R
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
⊢ IsIntegrallyClosed S
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
⊢ IsIntegrallyClosed S
Tactic:
let g : S →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ IsIntegrallyClosed S
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ IsIntegrallyClosed S
Tactic:
letI := g.toAlgebra
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S
Tactic:
have : IsScalarTower R S K := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S
Tactic:
have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S
Tactic:
refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
  ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
⊢ IsIntegral S x → ∃ y, (algebraMap S K) y = x
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
⊢ IsIntegral S x → ∃ y, (algebraMap S K) y = x
Tactic:
intro hx
Proof state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
⊢ ∃ y, (algebraMap S K) y = x
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
⊢ ∃ y, (algebraMap S K) y = x
Tactic:
obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
Proof state after:
case intro.mk
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap S K) y = x
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
case intro.mk
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap S K) y = x
Tactic:
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy
Proof state after:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap S K) y = x
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap S K) y = x
Tactic:
refine' ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr _⟩
Proof state after:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x
Tactic:
rw [RingHom.comp_id, hz, ← Algebra.smul_def]
Proof state after:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x
Tactic:
rfl
Proof state after:
no goals
Theorem: isIntegrallyClosed_of_isLocalization
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = (algebraMap S K).comp (algebraMap R S)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
Proof state after:
no goals
Theorem: IsIntegral_of_isLocalization
Proof state before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
⊢ Algebra.IsIntegral Rₚ Sₚ
Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
  (algebraMap R S) (Submonoid.le_comap_map M) := by
  apply IsLocalization.ringHom_ext M
  simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
Proof state after:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ Algebra.IsIntegral Rₚ Sₚ
Theorem: IsIntegral_of_isLocalization
Proof state before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ Algebra.IsIntegral Rₚ Sₚ
Tactic:
constructor
Proof state after:
case isIntegral
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Sₚ), IsIntegral Rₚ x
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Sₚ), IsIntegral Rₚ x
Tactic:
intros x
Proof state after:
case isIntegral
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Sₚ
⊢ IsIntegral Rₚ x