case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (map f g) ≤ AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)

case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g) ≤ AlgHom.range (map f g)
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (map f g) = AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)
apply le_antisymm
case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ ↑(map f g) '' {t | ∃ a b, a ⊗ₜ[R] b = t} ⊆
    ↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g))
case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (map f g) ≤ AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g)
rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]
case a.intro.intro.intro.intro
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
a : A
b : C
⊢ ↑(map f g) (a ⊗ₜ[R] b) ∈ ↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g))
case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ ↑(map f g) '' {t | ∃ a b, a ⊗ₜ[R] b = t} ⊆
    ↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g))
rintro _ ⟨_, ⟨a, b, rfl⟩, rfl⟩
case a.intro.intro.intro.intro
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
a : A
b : C
⊢ ↑f a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑g b ∈ ↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g))
case a.intro.intro.intro.intro
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
a : A
b : C
⊢ ↑(map f g) (a ⊗ₜ[R] b) ∈ ↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g))
rw [map_tmul, ← _root_.mul_one (f a), ← _root_.one_mul (g b), ← tmul_mul_tmul]
no goals
case a.intro.intro.intro.intro
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
a : A
b : C
⊢ ↑f a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑g b ∈ ↑(AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g))
exact mul_mem_sup (AlgHom.mem_range_self _ a) (AlgHom.mem_range_self _ b)
case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (AlgHom.comp (map f g) includeLeft) ⊔ AlgHom.range (AlgHom.comp (map f g) includeRight) ≤
    AlgHom.range (map f g)
case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (AlgHom.comp includeLeft f) ⊔ AlgHom.range (AlgHom.comp includeRight g) ≤ AlgHom.range (map f g)
rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]
no goals
case a
R : Type u
inst✝⁸ : CommSemiring R
A : Type v₁
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type v₂
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
C : Type v₃
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type v₄
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
⊢ AlgHom.range (AlgHom.comp (map f g) includeLeft) ⊔ AlgHom.range (AlgHom.comp (map f g) includeRight) ≤
    AlgHom.range (map f g)
exact sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)