Theorems · Definition · commutative algebra

galLiftEquiv

{A : Type u_1} →
  (K : Type u_2) →
    (L : Type u_3) →
      (L₂ : Type u_4) →
        {B : Type u_6} →
          {B₂ : Type u_7} →
            [inst : CommRing A] →
              [inst_1 : CommRing B] →
                [inst_2 : CommRing B₂] →
                  [inst_3 : Algebra A B] →
                    [inst_4 : Algebra A B₂] →
                      [inst_5 : Field K] →
                        [inst_6 : Field L] →
                          [inst_7 : Field L₂] →
                            [inst_8 : Algebra A K] →
                              [IsFractionRing A K] →
                                [inst_10 : Algebra K L] →
                                  [inst_11 : Algebra A L] →
                                    [IsScalarTower A K L] →
                                      [inst_13 : Algebra K L₂] →
                                        [inst_14 : Algebra A L₂] →
                                          [IsScalarTower A K L₂] →
                                            [inst_16 : Algebra B L] →
                                              [IsScalarTower A B L] →
                                                [IsIntegralClosure B A L] →
                                                  [inst_19 : Algebra B₂ L₂] →
                                                    [IsScalarTower A B₂ L₂] →
                                                      [IsIntegralClosure B₂ A L₂] →
                                                        [Algebra.IsAlgebraic K L] →
                                                          [Algebra.IsAlgebraic K L₂] → (B ≃ₐ[A] B₂) → L ≃ₐ[K] L₂

A version of galLift for AlgEquiv.

Defined in

Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Cited by

4 results in Mathlib

Foundations

Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraAlgebraFieldFieldFieldAlgebraIsFractionRingAlgebraAlgebraIsScalarTowerAlgebraAlgebraIsScalarTowerAlgebraIsScalarTowerIsIntegralClosureAlgebraIsScalarTowerIsIntegralClosureAlgebra.IsAlgebraicAlgebra.IsAlgebraic