theorem EtaleAlgebra.pi_single_mul {ι : Type u_1} [DecidableEq ι] {F : ι → Type u_2} [(i : ι) → CommMonoidWithZero (F i)] (i : ι) (a : F i) (f : (j : ι) → F j) : Pi.single i a * f = Pi.single i (a * f i)

theorem EtaleAlgebra.pi_field_not_domain_of_two {ι : Type u_1} {F : ι → Type u_2} [(i : ι) → Field (F i)] [DecidableEq ι] {i j : ι} (hij : i ≠ j) : ¬NoZeroDivisors ((k : ι) → F k)

noncomputable def EtaleAlgebra.piSingletonAlgEquiv {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (j : ι) (hsing : ∀ (i : ι), i = j) : ((i : ι) → F i) ≃ₐ[K] F j

structure EtaleAlgebra.IsEtaleAlgebra (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [Algebra K L] : Prop

• exists_decomp : ∃ (ι : Type) (x : Fintype ι) (F : ι → Type) (x : (i : ι) → Field (F i)) (x_1 : (i : ι) → Algebra K (F i)) (_ : ∀ (i : ι), Algebra.IsSeparable K (F i)), Nonempty (L ≃ₐ[K] (i : ι) → F i)

def EtaleAlgebra.IsFiniteEtaleAlgebra (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [Algebra K L] : Prop

noncomputable def EtaleAlgebra.piRestr {K : Type u_1} [Field K] {ι : Type u_2} {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (S : Finset ι) : ((i : ι) → F i) →ₐ[K] (i : ↥S) → F ↑i

@[simp]

theorem EtaleAlgebra.piRestr_apply {K : Type u_1} [Field K] {ι : Type u_2} {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (S : Finset ι) (f : (i : ι) → F i) (j : ↥S) : (piRestr S) f j = f ↑j

theorem EtaleAlgebra.piRestr_surjective {K : Type u_1} [Field K] {ι : Type u_2} {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (S : Finset ι) : Function.Surjective ⇑(piRestr S)

theorem EtaleAlgebra.mem_ker_piRestr {K : Type u_1} [Field K] {ι : Type u_2} {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (S : Finset ι) (f : (i : ι) → F i) : f ∈ RingHom.ker (piRestr S) ↔ ∀ i ∈ S, f i = 0

theorem EtaleAlgebra.ker_phi_eq_ker_piRestr {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] {B : Type u_4} [CommRing B] [Algebra K B] (φ : ((i : ι) → F i) →ₐ[K] B) : have T := {i : ι | ∃ f ∈ RingHom.ker φ, f i ≠ 0}; RingHom.ker φ = RingHom.ker (piRestr (Finset.univ \ T))

noncomputable def EtaleAlgebra.algEquivOfSurjSameKer {R : Type u_4} {A : Type u_5} {B : Type u_6} {C : Type u_7} [CommSemiring R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) (hker : RingHom.ker f = RingHom.ker g) : B ≃ₐ[R] C

theorem EtaleAlgebra.surj_algHom_pi_fields_isSubproduct {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] {B : Type u_4} [CommRing B] [Algebra K B] (φ : ((i : ι) → F i) →ₐ[K] B) (hφ : Function.Surjective ⇑φ) : ∃ (S : Finset ι), Nonempty (B ≃ₐ[K] (i : ↥S) → F ↑i)

theorem EtaleAlgebra.algEquiv_field_of_pi_field {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] {E : Type u_4} [Field E] [Algebra K E] (e : E ≃ₐ[K] (i : ι) → F i) : ∃ (j : ι), Nonempty (E ≃ₐ[K] F j)

theorem EtaleAlgebra.surjection_to_field_factors {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {F : ι → Type u_3} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] {E : Type u_4} [Field E] [Algebra K E] (φ : ((i : ι) → F i) →ₐ[K] E) (hφ : Function.Surjective ⇑φ) : ∃ (j : ι), Nonempty (E ≃ₐ[K] F j)

theorem EtaleAlgebra.etale_decomposition_unique {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {κ : Type u_3} [Fintype κ] [DecidableEq κ] {F : ι → Type u_4} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] {G : κ → Type u_5} [(j : κ) → Field (G j)] [(j : κ) → Algebra K (G j)] (e : ((i : ι) → F i) ≃ₐ[K] (j : κ) → G j) : (∀ (i : ι), ∃ (j : κ), Nonempty (F i ≃ₐ[K] G j)) ∧ ∀ (j : κ), ∃ (i : ι), Nonempty (G j ≃ₐ[K] F i)

@[reducible, inline]

abbrev EtaleAlgebra.baseChange (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] (B : Type u_3) [CommRing B] [Algebra A B] : Type (max u_2 u_3)

@[implicit_reducible]

instance EtaleAlgebra.baseChange.instModule (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] (B : Type u_3) [CommRing B] [Algebra A B] : Module B (baseChange A M B)

@[implicit_reducible]

instance EtaleAlgebra.baseChange.instAlgebra (A : Type u_1) [CommRing A] (M : Type u_2) [CommRing M] [Algebra A M] (B : Type u_3) [CommRing B] [Algebra A B] : Algebra B (TensorProduct A B M)