R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ↑f
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f
      (Algebra.adjoin R
        ↑(Finset.preimage s ↑f
            (_ : ∀ (x : A), x ∈ ↑f ⁻¹' ↑s → ∀ (x_2 : A), x_2 ∈ ↑f ⁻¹' ↑s → ↑f x = ↑f x_2 → x = x_2))) =
    map f S
rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ↑f
rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤
exact map_mono le_top